src/HOL/Probability/Independent_Family.thy
 author hoelzl Wed Oct 10 12:12:21 2012 +0200 (2012-10-10) changeset 49781 59b219ca3513 parent 49776 199d1d5bb17e child 49784 5e5b2da42a69 permissions -rw-r--r--
simplified assumptions for kolmogorov_0_1_law
 hoelzl@42861 ` 1` ```(* Title: HOL/Probability/Independent_Family.thy ``` hoelzl@42861 ` 2` ``` Author: Johannes Hölzl, TU München ``` hoelzl@42861 ` 3` ```*) ``` hoelzl@42861 ` 4` hoelzl@42861 ` 5` ```header {* Independent families of events, event sets, and random variables *} ``` hoelzl@42861 ` 6` hoelzl@42861 ` 7` ```theory Independent_Family ``` hoelzl@47694 ` 8` ``` imports Probability_Measure Infinite_Product_Measure ``` hoelzl@42861 ` 9` ```begin ``` hoelzl@42861 ` 10` hoelzl@42985 ` 11` ```lemma INT_decseq_offset: ``` hoelzl@42985 ` 12` ``` assumes "decseq F" ``` hoelzl@42985 ` 13` ``` shows "(\i. F i) = (\i\{n..}. F i)" ``` hoelzl@42985 ` 14` ```proof safe ``` hoelzl@42985 ` 15` ``` fix x i assume x: "x \ (\i\{n..}. F i)" ``` hoelzl@42985 ` 16` ``` show "x \ F i" ``` hoelzl@42985 ` 17` ``` proof cases ``` hoelzl@42985 ` 18` ``` from x have "x \ F n" by auto ``` hoelzl@42985 ` 19` ``` also assume "i \ n" with `decseq F` have "F n \ F i" ``` hoelzl@42985 ` 20` ``` unfolding decseq_def by simp ``` hoelzl@42985 ` 21` ``` finally show ?thesis . ``` hoelzl@42985 ` 22` ``` qed (insert x, simp) ``` hoelzl@42985 ` 23` ```qed auto ``` hoelzl@42985 ` 24` hoelzl@42861 ` 25` ```definition (in prob_space) ``` hoelzl@42983 ` 26` ``` "indep_events A I \ (A`I \ events) \ ``` hoelzl@42981 ` 27` ``` (\J\I. J \ {} \ finite J \ prob (\j\J. A j) = (\j\J. prob (A j)))" ``` hoelzl@42861 ` 28` hoelzl@42861 ` 29` ```definition (in prob_space) ``` hoelzl@42981 ` 30` ``` "indep_event A B \ indep_events (bool_case A B) UNIV" ``` hoelzl@42861 ` 31` hoelzl@42861 ` 32` ```definition (in prob_space) ``` hoelzl@42983 ` 33` ``` "indep_sets F I \ (\i\I. F i \ events) \ ``` hoelzl@42981 ` 34` ``` (\J\I. J \ {} \ finite J \ (\A\Pi J F. prob (\j\J. A j) = (\j\J. prob (A j))))" ``` hoelzl@42981 ` 35` hoelzl@42981 ` 36` ```definition (in prob_space) ``` hoelzl@42981 ` 37` ``` "indep_set A B \ indep_sets (bool_case A B) UNIV" ``` hoelzl@42861 ` 38` hoelzl@42861 ` 39` ```definition (in prob_space) ``` hoelzl@42989 ` 40` ``` "indep_vars M' X I \ ``` hoelzl@42861 ` 41` ``` (\i\I. random_variable (M' i) (X i)) \ ``` hoelzl@42861 ` 42` ``` indep_sets (\i. sigma_sets (space M) { X i -` A \ space M | A. A \ sets (M' i)}) I" ``` hoelzl@42861 ` 43` hoelzl@42989 ` 44` ```definition (in prob_space) ``` hoelzl@42989 ` 45` ``` "indep_var Ma A Mb B \ indep_vars (bool_case Ma Mb) (bool_case A B) UNIV" ``` hoelzl@42989 ` 46` hoelzl@47694 ` 47` ```lemma (in prob_space) indep_sets_cong: ``` hoelzl@42981 ` 48` ``` "I = J \ (\i. i \ I \ F i = G i) \ indep_sets F I \ indep_sets G J" ``` hoelzl@42981 ` 49` ``` by (simp add: indep_sets_def, intro conj_cong all_cong imp_cong ball_cong) blast+ ``` hoelzl@42981 ` 50` hoelzl@42985 ` 51` ```lemma (in prob_space) indep_sets_singleton_iff_indep_events: ``` hoelzl@42985 ` 52` ``` "indep_sets (\i. {F i}) I \ indep_events F I" ``` hoelzl@42985 ` 53` ``` unfolding indep_sets_def indep_events_def ``` hoelzl@42985 ` 54` ``` by (simp, intro conj_cong ball_cong all_cong imp_cong) (auto simp: Pi_iff) ``` hoelzl@42985 ` 55` hoelzl@42981 ` 56` ```lemma (in prob_space) indep_events_finite_index_events: ``` hoelzl@42981 ` 57` ``` "indep_events F I \ (\J\I. J \ {} \ finite J \ indep_events F J)" ``` hoelzl@42981 ` 58` ``` by (auto simp: indep_events_def) ``` hoelzl@42981 ` 59` hoelzl@42861 ` 60` ```lemma (in prob_space) indep_sets_finite_index_sets: ``` hoelzl@42861 ` 61` ``` "indep_sets F I \ (\J\I. J \ {} \ finite J \ indep_sets F J)" ``` hoelzl@42861 ` 62` ```proof (intro iffI allI impI) ``` hoelzl@42861 ` 63` ``` assume *: "\J\I. J \ {} \ finite J \ indep_sets F J" ``` hoelzl@42861 ` 64` ``` show "indep_sets F I" unfolding indep_sets_def ``` hoelzl@42861 ` 65` ``` proof (intro conjI ballI allI impI) ``` hoelzl@42861 ` 66` ``` fix i assume "i \ I" ``` hoelzl@42861 ` 67` ``` with *[THEN spec, of "{i}"] show "F i \ events" ``` hoelzl@42861 ` 68` ``` by (auto simp: indep_sets_def) ``` hoelzl@42861 ` 69` ``` qed (insert *, auto simp: indep_sets_def) ``` hoelzl@42861 ` 70` ```qed (auto simp: indep_sets_def) ``` hoelzl@42861 ` 71` hoelzl@42861 ` 72` ```lemma (in prob_space) indep_sets_mono_index: ``` hoelzl@42861 ` 73` ``` "J \ I \ indep_sets F I \ indep_sets F J" ``` hoelzl@42861 ` 74` ``` unfolding indep_sets_def by auto ``` hoelzl@42861 ` 75` hoelzl@42861 ` 76` ```lemma (in prob_space) indep_sets_mono_sets: ``` hoelzl@42861 ` 77` ``` assumes indep: "indep_sets F I" ``` hoelzl@42861 ` 78` ``` assumes mono: "\i. i\I \ G i \ F i" ``` hoelzl@42861 ` 79` ``` shows "indep_sets G I" ``` hoelzl@42861 ` 80` ```proof - ``` hoelzl@42861 ` 81` ``` have "(\i\I. F i \ events) \ (\i\I. G i \ events)" ``` hoelzl@42861 ` 82` ``` using mono by auto ``` hoelzl@42861 ` 83` ``` moreover have "\A J. J \ I \ A \ (\ j\J. G j) \ A \ (\ j\J. F j)" ``` hoelzl@42861 ` 84` ``` using mono by (auto simp: Pi_iff) ``` hoelzl@42861 ` 85` ``` ultimately show ?thesis ``` hoelzl@42861 ` 86` ``` using indep by (auto simp: indep_sets_def) ``` hoelzl@42861 ` 87` ```qed ``` hoelzl@42861 ` 88` hoelzl@49772 ` 89` ```lemma (in prob_space) indep_sets_mono: ``` hoelzl@49772 ` 90` ``` assumes indep: "indep_sets F I" ``` hoelzl@49772 ` 91` ``` assumes mono: "J \ I" "\i. i\J \ G i \ F i" ``` hoelzl@49772 ` 92` ``` shows "indep_sets G J" ``` hoelzl@49772 ` 93` ``` apply (rule indep_sets_mono_sets) ``` hoelzl@49772 ` 94` ``` apply (rule indep_sets_mono_index) ``` hoelzl@49772 ` 95` ``` apply (fact +) ``` hoelzl@49772 ` 96` ``` done ``` hoelzl@49772 ` 97` hoelzl@42861 ` 98` ```lemma (in prob_space) indep_setsI: ``` hoelzl@42861 ` 99` ``` assumes "\i. i \ I \ F i \ events" ``` hoelzl@42861 ` 100` ``` and "\A J. J \ {} \ J \ I \ finite J \ (\j\J. A j \ F j) \ prob (\j\J. A j) = (\j\J. prob (A j))" ``` hoelzl@42861 ` 101` ``` shows "indep_sets F I" ``` hoelzl@42861 ` 102` ``` using assms unfolding indep_sets_def by (auto simp: Pi_iff) ``` hoelzl@42861 ` 103` hoelzl@42861 ` 104` ```lemma (in prob_space) indep_setsD: ``` hoelzl@42861 ` 105` ``` assumes "indep_sets F I" and "J \ I" "J \ {}" "finite J" "\j\J. A j \ F j" ``` hoelzl@42861 ` 106` ``` shows "prob (\j\J. A j) = (\j\J. prob (A j))" ``` hoelzl@42861 ` 107` ``` using assms unfolding indep_sets_def by auto ``` hoelzl@42861 ` 108` hoelzl@42982 ` 109` ```lemma (in prob_space) indep_setI: ``` hoelzl@42982 ` 110` ``` assumes ev: "A \ events" "B \ events" ``` hoelzl@42982 ` 111` ``` and indep: "\a b. a \ A \ b \ B \ prob (a \ b) = prob a * prob b" ``` hoelzl@42982 ` 112` ``` shows "indep_set A B" ``` hoelzl@42982 ` 113` ``` unfolding indep_set_def ``` hoelzl@42982 ` 114` ```proof (rule indep_setsI) ``` hoelzl@42982 ` 115` ``` fix F J assume "J \ {}" "J \ UNIV" ``` hoelzl@42982 ` 116` ``` and F: "\j\J. F j \ (case j of True \ A | False \ B)" ``` hoelzl@42982 ` 117` ``` have "J \ Pow UNIV" by auto ``` hoelzl@42982 ` 118` ``` with F `J \ {}` indep[of "F True" "F False"] ``` hoelzl@42982 ` 119` ``` show "prob (\j\J. F j) = (\j\J. prob (F j))" ``` hoelzl@42982 ` 120` ``` unfolding UNIV_bool Pow_insert by (auto simp: ac_simps) ``` hoelzl@42982 ` 121` ```qed (auto split: bool.split simp: ev) ``` hoelzl@42982 ` 122` hoelzl@42982 ` 123` ```lemma (in prob_space) indep_setD: ``` hoelzl@42982 ` 124` ``` assumes indep: "indep_set A B" and ev: "a \ A" "b \ B" ``` hoelzl@42982 ` 125` ``` shows "prob (a \ b) = prob a * prob b" ``` hoelzl@42982 ` 126` ``` using indep[unfolded indep_set_def, THEN indep_setsD, of UNIV "bool_case a b"] ev ``` hoelzl@42982 ` 127` ``` by (simp add: ac_simps UNIV_bool) ``` hoelzl@42982 ` 128` hoelzl@43340 ` 129` ```lemma (in prob_space) indep_var_eq: ``` hoelzl@43340 ` 130` ``` "indep_var S X T Y \ ``` hoelzl@43340 ` 131` ``` (random_variable S X \ random_variable T Y) \ ``` hoelzl@43340 ` 132` ``` indep_set ``` hoelzl@43340 ` 133` ``` (sigma_sets (space M) { X -` A \ space M | A. A \ sets S}) ``` hoelzl@43340 ` 134` ``` (sigma_sets (space M) { Y -` A \ space M | A. A \ sets T})" ``` hoelzl@43340 ` 135` ``` unfolding indep_var_def indep_vars_def indep_set_def UNIV_bool ``` hoelzl@43340 ` 136` ``` by (intro arg_cong2[where f="op \"] arg_cong2[where f=indep_sets] ext) ``` hoelzl@43340 ` 137` ``` (auto split: bool.split) ``` hoelzl@43340 ` 138` hoelzl@42982 ` 139` ```lemma (in prob_space) ``` hoelzl@42982 ` 140` ``` assumes indep: "indep_set A B" ``` hoelzl@42983 ` 141` ``` shows indep_setD_ev1: "A \ events" ``` hoelzl@42983 ` 142` ``` and indep_setD_ev2: "B \ events" ``` hoelzl@42982 ` 143` ``` using indep unfolding indep_set_def indep_sets_def UNIV_bool by auto ``` hoelzl@42982 ` 144` hoelzl@42861 ` 145` ```lemma (in prob_space) indep_sets_dynkin: ``` hoelzl@42861 ` 146` ``` assumes indep: "indep_sets F I" ``` hoelzl@47694 ` 147` ``` shows "indep_sets (\i. dynkin (space M) (F i)) I" ``` hoelzl@42861 ` 148` ``` (is "indep_sets ?F I") ``` hoelzl@42861 ` 149` ```proof (subst indep_sets_finite_index_sets, intro allI impI ballI) ``` hoelzl@42861 ` 150` ``` fix J assume "finite J" "J \ I" "J \ {}" ``` hoelzl@42861 ` 151` ``` with indep have "indep_sets F J" ``` hoelzl@42861 ` 152` ``` by (subst (asm) indep_sets_finite_index_sets) auto ``` hoelzl@42861 ` 153` ``` { fix J K assume "indep_sets F K" ``` wenzelm@46731 ` 154` ``` let ?G = "\S i. if i \ S then ?F i else F i" ``` hoelzl@42861 ` 155` ``` assume "finite J" "J \ K" ``` hoelzl@42861 ` 156` ``` then have "indep_sets (?G J) K" ``` hoelzl@42861 ` 157` ``` proof induct ``` hoelzl@42861 ` 158` ``` case (insert j J) ``` hoelzl@42861 ` 159` ``` moreover def G \ "?G J" ``` hoelzl@42861 ` 160` ``` ultimately have G: "indep_sets G K" "\i. i \ K \ G i \ events" and "j \ K" ``` hoelzl@42861 ` 161` ``` by (auto simp: indep_sets_def) ``` hoelzl@42861 ` 162` ``` let ?D = "{E\events. indep_sets (G(j := {E})) K }" ``` hoelzl@42861 ` 163` ``` { fix X assume X: "X \ events" ``` hoelzl@42861 ` 164` ``` assume indep: "\J A. J \ {} \ J \ K \ finite J \ j \ J \ (\i\J. A i \ G i) ``` hoelzl@42861 ` 165` ``` \ prob ((\i\J. A i) \ X) = prob X * (\i\J. prob (A i))" ``` hoelzl@42861 ` 166` ``` have "indep_sets (G(j := {X})) K" ``` hoelzl@42861 ` 167` ``` proof (rule indep_setsI) ``` hoelzl@42861 ` 168` ``` fix i assume "i \ K" then show "(G(j:={X})) i \ events" ``` hoelzl@42861 ` 169` ``` using G X by auto ``` hoelzl@42861 ` 170` ``` next ``` hoelzl@42861 ` 171` ``` fix A J assume J: "J \ {}" "J \ K" "finite J" "\i\J. A i \ (G(j := {X})) i" ``` hoelzl@42861 ` 172` ``` show "prob (\j\J. A j) = (\j\J. prob (A j))" ``` hoelzl@42861 ` 173` ``` proof cases ``` hoelzl@42861 ` 174` ``` assume "j \ J" ``` hoelzl@42861 ` 175` ``` with J have "A j = X" by auto ``` hoelzl@42861 ` 176` ``` show ?thesis ``` hoelzl@42861 ` 177` ``` proof cases ``` hoelzl@42861 ` 178` ``` assume "J = {j}" then show ?thesis by simp ``` hoelzl@42861 ` 179` ``` next ``` hoelzl@42861 ` 180` ``` assume "J \ {j}" ``` hoelzl@42861 ` 181` ``` have "prob (\i\J. A i) = prob ((\i\J-{j}. A i) \ X)" ``` hoelzl@42861 ` 182` ``` using `j \ J` `A j = X` by (auto intro!: arg_cong[where f=prob] split: split_if_asm) ``` hoelzl@42861 ` 183` ``` also have "\ = prob X * (\i\J-{j}. prob (A i))" ``` hoelzl@42861 ` 184` ``` proof (rule indep) ``` hoelzl@42861 ` 185` ``` show "J - {j} \ {}" "J - {j} \ K" "finite (J - {j})" "j \ J - {j}" ``` hoelzl@42861 ` 186` ``` using J `J \ {j}` `j \ J` by auto ``` hoelzl@42861 ` 187` ``` show "\i\J - {j}. A i \ G i" ``` hoelzl@42861 ` 188` ``` using J by auto ``` hoelzl@42861 ` 189` ``` qed ``` hoelzl@42861 ` 190` ``` also have "\ = prob (A j) * (\i\J-{j}. prob (A i))" ``` hoelzl@42861 ` 191` ``` using `A j = X` by simp ``` hoelzl@42861 ` 192` ``` also have "\ = (\i\J. prob (A i))" ``` hoelzl@42861 ` 193` ``` unfolding setprod.insert_remove[OF `finite J`, symmetric, of "\i. prob (A i)"] ``` hoelzl@42861 ` 194` ``` using `j \ J` by (simp add: insert_absorb) ``` hoelzl@42861 ` 195` ``` finally show ?thesis . ``` hoelzl@42861 ` 196` ``` qed ``` hoelzl@42861 ` 197` ``` next ``` hoelzl@42861 ` 198` ``` assume "j \ J" ``` hoelzl@42861 ` 199` ``` with J have "\i\J. A i \ G i" by (auto split: split_if_asm) ``` hoelzl@42861 ` 200` ``` with J show ?thesis ``` hoelzl@42861 ` 201` ``` by (intro indep_setsD[OF G(1)]) auto ``` hoelzl@42861 ` 202` ``` qed ``` hoelzl@42861 ` 203` ``` qed } ``` hoelzl@42861 ` 204` ``` note indep_sets_insert = this ``` hoelzl@47694 ` 205` ``` have "dynkin_system (space M) ?D" ``` hoelzl@42987 ` 206` ``` proof (rule dynkin_systemI', simp_all cong del: indep_sets_cong, safe) ``` hoelzl@42861 ` 207` ``` show "indep_sets (G(j := {{}})) K" ``` hoelzl@42861 ` 208` ``` by (rule indep_sets_insert) auto ``` hoelzl@42861 ` 209` ``` next ``` hoelzl@42861 ` 210` ``` fix X assume X: "X \ events" and G': "indep_sets (G(j := {X})) K" ``` hoelzl@42861 ` 211` ``` show "indep_sets (G(j := {space M - X})) K" ``` hoelzl@42861 ` 212` ``` proof (rule indep_sets_insert) ``` hoelzl@42861 ` 213` ``` fix J A assume J: "J \ {}" "J \ K" "finite J" "j \ J" and A: "\i\J. A i \ G i" ``` hoelzl@42861 ` 214` ``` then have A_sets: "\i. i\J \ A i \ events" ``` hoelzl@42861 ` 215` ``` using G by auto ``` hoelzl@42861 ` 216` ``` have "prob ((\j\J. A j) \ (space M - X)) = ``` hoelzl@42861 ` 217` ``` prob ((\j\J. A j) - (\i\insert j J. (A(j := X)) i))" ``` hoelzl@47694 ` 218` ``` using A_sets sets_into_space[of _ M] X `J \ {}` ``` hoelzl@42861 ` 219` ``` by (auto intro!: arg_cong[where f=prob] split: split_if_asm) ``` hoelzl@42861 ` 220` ``` also have "\ = prob (\j\J. A j) - prob (\i\insert j J. (A(j := X)) i)" ``` hoelzl@42861 ` 221` ``` using J `J \ {}` `j \ J` A_sets X sets_into_space ``` hoelzl@42861 ` 222` ``` by (auto intro!: finite_measure_Diff finite_INT split: split_if_asm) ``` hoelzl@42861 ` 223` ``` finally have "prob ((\j\J. A j) \ (space M - X)) = ``` hoelzl@42861 ` 224` ``` prob (\j\J. A j) - prob (\i\insert j J. (A(j := X)) i)" . ``` hoelzl@42861 ` 225` ``` moreover { ``` hoelzl@42861 ` 226` ``` have "prob (\j\J. A j) = (\j\J. prob (A j))" ``` hoelzl@42861 ` 227` ``` using J A `finite J` by (intro indep_setsD[OF G(1)]) auto ``` hoelzl@42861 ` 228` ``` then have "prob (\j\J. A j) = prob (space M) * (\i\J. prob (A i))" ``` hoelzl@42861 ` 229` ``` using prob_space by simp } ``` hoelzl@42861 ` 230` ``` moreover { ``` hoelzl@42861 ` 231` ``` have "prob (\i\insert j J. (A(j := X)) i) = (\i\insert j J. prob ((A(j := X)) i))" ``` hoelzl@42861 ` 232` ``` using J A `j \ K` by (intro indep_setsD[OF G']) auto ``` hoelzl@42861 ` 233` ``` then have "prob (\i\insert j J. (A(j := X)) i) = prob X * (\i\J. prob (A i))" ``` hoelzl@42861 ` 234` ``` using `finite J` `j \ J` by (auto intro!: setprod_cong) } ``` hoelzl@42861 ` 235` ``` ultimately have "prob ((\j\J. A j) \ (space M - X)) = (prob (space M) - prob X) * (\i\J. prob (A i))" ``` hoelzl@42861 ` 236` ``` by (simp add: field_simps) ``` hoelzl@42861 ` 237` ``` also have "\ = prob (space M - X) * (\i\J. prob (A i))" ``` hoelzl@42861 ` 238` ``` using X A by (simp add: finite_measure_compl) ``` hoelzl@42861 ` 239` ``` finally show "prob ((\j\J. A j) \ (space M - X)) = prob (space M - X) * (\i\J. prob (A i))" . ``` hoelzl@42861 ` 240` ``` qed (insert X, auto) ``` hoelzl@42861 ` 241` ``` next ``` hoelzl@42861 ` 242` ``` fix F :: "nat \ 'a set" assume disj: "disjoint_family F" and "range F \ ?D" ``` hoelzl@42861 ` 243` ``` then have F: "\i. F i \ events" "\i. indep_sets (G(j:={F i})) K" by auto ``` hoelzl@42861 ` 244` ``` show "indep_sets (G(j := {\k. F k})) K" ``` hoelzl@42861 ` 245` ``` proof (rule indep_sets_insert) ``` hoelzl@42861 ` 246` ``` fix J A assume J: "j \ J" "J \ {}" "J \ K" "finite J" and A: "\i\J. A i \ G i" ``` hoelzl@42861 ` 247` ``` then have A_sets: "\i. i\J \ A i \ events" ``` hoelzl@42861 ` 248` ``` using G by auto ``` hoelzl@42861 ` 249` ``` have "prob ((\j\J. A j) \ (\k. F k)) = prob (\k. (\i\insert j J. (A(j := F k)) i))" ``` hoelzl@42861 ` 250` ``` using `J \ {}` `j \ J` `j \ K` by (auto intro!: arg_cong[where f=prob] split: split_if_asm) ``` hoelzl@42861 ` 251` ``` moreover have "(\k. prob (\i\insert j J. (A(j := F k)) i)) sums prob (\k. (\i\insert j J. (A(j := F k)) i))" ``` hoelzl@42861 ` 252` ``` proof (rule finite_measure_UNION) ``` hoelzl@42861 ` 253` ``` show "disjoint_family (\k. \i\insert j J. (A(j := F k)) i)" ``` hoelzl@42861 ` 254` ``` using disj by (rule disjoint_family_on_bisimulation) auto ``` hoelzl@42861 ` 255` ``` show "range (\k. \i\insert j J. (A(j := F k)) i) \ events" ``` hoelzl@42861 ` 256` ``` using A_sets F `finite J` `J \ {}` `j \ J` by (auto intro!: Int) ``` hoelzl@42861 ` 257` ``` qed ``` hoelzl@42861 ` 258` ``` moreover { fix k ``` hoelzl@42861 ` 259` ``` from J A `j \ K` have "prob (\i\insert j J. (A(j := F k)) i) = prob (F k) * (\i\J. prob (A i))" ``` hoelzl@42861 ` 260` ``` by (subst indep_setsD[OF F(2)]) (auto intro!: setprod_cong split: split_if_asm) ``` hoelzl@42861 ` 261` ``` also have "\ = prob (F k) * prob (\i\J. A i)" ``` hoelzl@42861 ` 262` ``` using J A `j \ K` by (subst indep_setsD[OF G(1)]) auto ``` hoelzl@42861 ` 263` ``` finally have "prob (\i\insert j J. (A(j := F k)) i) = prob (F k) * prob (\i\J. A i)" . } ``` hoelzl@42861 ` 264` ``` ultimately have "(\k. prob (F k) * prob (\i\J. A i)) sums (prob ((\j\J. A j) \ (\k. F k)))" ``` hoelzl@42861 ` 265` ``` by simp ``` hoelzl@42861 ` 266` ``` moreover ``` hoelzl@42861 ` 267` ``` have "(\k. prob (F k) * prob (\i\J. A i)) sums (prob (\k. F k) * prob (\i\J. A i))" ``` hoelzl@42861 ` 268` ``` using disj F(1) by (intro finite_measure_UNION sums_mult2) auto ``` hoelzl@42861 ` 269` ``` then have "(\k. prob (F k) * prob (\i\J. A i)) sums (prob (\k. F k) * (\i\J. prob (A i)))" ``` hoelzl@42861 ` 270` ``` using J A `j \ K` by (subst indep_setsD[OF G(1), symmetric]) auto ``` hoelzl@42861 ` 271` ``` ultimately ``` hoelzl@42861 ` 272` ``` show "prob ((\j\J. A j) \ (\k. F k)) = prob (\k. F k) * (\j\J. prob (A j))" ``` hoelzl@42861 ` 273` ``` by (auto dest!: sums_unique) ``` hoelzl@42861 ` 274` ``` qed (insert F, auto) ``` hoelzl@42861 ` 275` ``` qed (insert sets_into_space, auto) ``` hoelzl@47694 ` 276` ``` then have mono: "dynkin (space M) (G j) \ {E \ events. indep_sets (G(j := {E})) K}" ``` hoelzl@47694 ` 277` ``` proof (rule dynkin_system.dynkin_subset, safe) ``` hoelzl@42861 ` 278` ``` fix X assume "X \ G j" ``` hoelzl@42861 ` 279` ``` then show "X \ events" using G `j \ K` by auto ``` hoelzl@42861 ` 280` ``` from `indep_sets G K` ``` hoelzl@42861 ` 281` ``` show "indep_sets (G(j := {X})) K" ``` hoelzl@42861 ` 282` ``` by (rule indep_sets_mono_sets) (insert `X \ G j`, auto) ``` hoelzl@42861 ` 283` ``` qed ``` hoelzl@42861 ` 284` ``` have "indep_sets (G(j:=?D)) K" ``` hoelzl@42861 ` 285` ``` proof (rule indep_setsI) ``` hoelzl@42861 ` 286` ``` fix i assume "i \ K" then show "(G(j := ?D)) i \ events" ``` hoelzl@42861 ` 287` ``` using G(2) by auto ``` hoelzl@42861 ` 288` ``` next ``` hoelzl@42861 ` 289` ``` fix A J assume J: "J\{}" "J \ K" "finite J" and A: "\i\J. A i \ (G(j := ?D)) i" ``` hoelzl@42861 ` 290` ``` show "prob (\j\J. A j) = (\j\J. prob (A j))" ``` hoelzl@42861 ` 291` ``` proof cases ``` hoelzl@42861 ` 292` ``` assume "j \ J" ``` hoelzl@42861 ` 293` ``` with A have indep: "indep_sets (G(j := {A j})) K" by auto ``` hoelzl@42861 ` 294` ``` from J A show ?thesis ``` hoelzl@42861 ` 295` ``` by (intro indep_setsD[OF indep]) auto ``` hoelzl@42861 ` 296` ``` next ``` hoelzl@42861 ` 297` ``` assume "j \ J" ``` hoelzl@42861 ` 298` ``` with J A have "\i\J. A i \ G i" by (auto split: split_if_asm) ``` hoelzl@42861 ` 299` ``` with J show ?thesis ``` hoelzl@42861 ` 300` ``` by (intro indep_setsD[OF G(1)]) auto ``` hoelzl@42861 ` 301` ``` qed ``` hoelzl@42861 ` 302` ``` qed ``` hoelzl@47694 ` 303` ``` then have "indep_sets (G(j := dynkin (space M) (G j))) K" ``` hoelzl@42861 ` 304` ``` by (rule indep_sets_mono_sets) (insert mono, auto) ``` hoelzl@42861 ` 305` ``` then show ?case ``` hoelzl@42861 ` 306` ``` by (rule indep_sets_mono_sets) (insert `j \ K` `j \ J`, auto simp: G_def) ``` hoelzl@42861 ` 307` ``` qed (insert `indep_sets F K`, simp) } ``` hoelzl@42861 ` 308` ``` from this[OF `indep_sets F J` `finite J` subset_refl] ``` hoelzl@47694 ` 309` ``` show "indep_sets ?F J" ``` hoelzl@42861 ` 310` ``` by (rule indep_sets_mono_sets) auto ``` hoelzl@42861 ` 311` ```qed ``` hoelzl@42861 ` 312` hoelzl@42861 ` 313` ```lemma (in prob_space) indep_sets_sigma: ``` hoelzl@42861 ` 314` ``` assumes indep: "indep_sets F I" ``` hoelzl@47694 ` 315` ``` assumes stable: "\i. i \ I \ Int_stable (F i)" ``` hoelzl@47694 ` 316` ``` shows "indep_sets (\i. sigma_sets (space M) (F i)) I" ``` hoelzl@42861 ` 317` ```proof - ``` hoelzl@42861 ` 318` ``` from indep_sets_dynkin[OF indep] ``` hoelzl@42861 ` 319` ``` show ?thesis ``` hoelzl@42861 ` 320` ``` proof (rule indep_sets_mono_sets, subst sigma_eq_dynkin, simp_all add: stable) ``` hoelzl@42861 ` 321` ``` fix i assume "i \ I" ``` hoelzl@42861 ` 322` ``` with indep have "F i \ events" by (auto simp: indep_sets_def) ``` hoelzl@42861 ` 323` ``` with sets_into_space show "F i \ Pow (space M)" by auto ``` hoelzl@42861 ` 324` ``` qed ``` hoelzl@42861 ` 325` ```qed ``` hoelzl@42861 ` 326` hoelzl@42987 ` 327` ```lemma (in prob_space) indep_sets_sigma_sets_iff: ``` hoelzl@47694 ` 328` ``` assumes "\i. i \ I \ Int_stable (F i)" ``` hoelzl@42987 ` 329` ``` shows "indep_sets (\i. sigma_sets (space M) (F i)) I \ indep_sets F I" ``` hoelzl@42987 ` 330` ```proof ``` hoelzl@42987 ` 331` ``` assume "indep_sets F I" then show "indep_sets (\i. sigma_sets (space M) (F i)) I" ``` hoelzl@47694 ` 332` ``` by (rule indep_sets_sigma) fact ``` hoelzl@42987 ` 333` ```next ``` hoelzl@42987 ` 334` ``` assume "indep_sets (\i. sigma_sets (space M) (F i)) I" then show "indep_sets F I" ``` hoelzl@42987 ` 335` ``` by (rule indep_sets_mono_sets) (intro subsetI sigma_sets.Basic) ``` hoelzl@42987 ` 336` ```qed ``` hoelzl@42987 ` 337` hoelzl@49781 ` 338` ```lemma (in prob_space) ``` hoelzl@49781 ` 339` ``` "indep_vars M' X I \ ``` hoelzl@49781 ` 340` ``` (\i\I. random_variable (M' i) (X i)) \ ``` hoelzl@49781 ` 341` ``` indep_sets (\i. { X i -` A \ space M | A. A \ sets (M' i)}) I" ``` hoelzl@49781 ` 342` ``` unfolding indep_vars_def ``` hoelzl@49781 ` 343` ``` apply (rule conj_cong[OF refl]) ``` hoelzl@49781 ` 344` ``` apply (rule indep_sets_sigma_sets_iff) ``` hoelzl@49781 ` 345` ``` apply (auto simp: Int_stable_def) ``` hoelzl@49781 ` 346` ``` apply (rule_tac x="A \ Aa" in exI) ``` hoelzl@49781 ` 347` ``` apply auto ``` hoelzl@49781 ` 348` ``` done ``` hoelzl@49781 ` 349` hoelzl@42861 ` 350` ```lemma (in prob_space) indep_sets2_eq: ``` hoelzl@42981 ` 351` ``` "indep_set A B \ A \ events \ B \ events \ (\a\A. \b\B. prob (a \ b) = prob a * prob b)" ``` hoelzl@42981 ` 352` ``` unfolding indep_set_def ``` hoelzl@42861 ` 353` ```proof (intro iffI ballI conjI) ``` hoelzl@42861 ` 354` ``` assume indep: "indep_sets (bool_case A B) UNIV" ``` hoelzl@42861 ` 355` ``` { fix a b assume "a \ A" "b \ B" ``` hoelzl@42861 ` 356` ``` with indep_setsD[OF indep, of UNIV "bool_case a b"] ``` hoelzl@42861 ` 357` ``` show "prob (a \ b) = prob a * prob b" ``` hoelzl@42861 ` 358` ``` unfolding UNIV_bool by (simp add: ac_simps) } ``` hoelzl@42861 ` 359` ``` from indep show "A \ events" "B \ events" ``` hoelzl@42861 ` 360` ``` unfolding indep_sets_def UNIV_bool by auto ``` hoelzl@42861 ` 361` ```next ``` hoelzl@42861 ` 362` ``` assume *: "A \ events \ B \ events \ (\a\A. \b\B. prob (a \ b) = prob a * prob b)" ``` hoelzl@42861 ` 363` ``` show "indep_sets (bool_case A B) UNIV" ``` hoelzl@42861 ` 364` ``` proof (rule indep_setsI) ``` hoelzl@42861 ` 365` ``` fix i show "(case i of True \ A | False \ B) \ events" ``` hoelzl@42861 ` 366` ``` using * by (auto split: bool.split) ``` hoelzl@42861 ` 367` ``` next ``` hoelzl@42861 ` 368` ``` fix J X assume "J \ {}" "J \ UNIV" and X: "\j\J. X j \ (case j of True \ A | False \ B)" ``` hoelzl@42861 ` 369` ``` then have "J = {True} \ J = {False} \ J = {True,False}" ``` hoelzl@42861 ` 370` ``` by (auto simp: UNIV_bool) ``` hoelzl@42861 ` 371` ``` then show "prob (\j\J. X j) = (\j\J. prob (X j))" ``` hoelzl@42861 ` 372` ``` using X * by auto ``` hoelzl@42861 ` 373` ``` qed ``` hoelzl@42861 ` 374` ```qed ``` hoelzl@42861 ` 375` hoelzl@42981 ` 376` ```lemma (in prob_space) indep_set_sigma_sets: ``` hoelzl@42981 ` 377` ``` assumes "indep_set A B" ``` hoelzl@47694 ` 378` ``` assumes A: "Int_stable A" and B: "Int_stable B" ``` hoelzl@42981 ` 379` ``` shows "indep_set (sigma_sets (space M) A) (sigma_sets (space M) B)" ``` hoelzl@42861 ` 380` ```proof - ``` hoelzl@42861 ` 381` ``` have "indep_sets (\i. sigma_sets (space M) (case i of True \ A | False \ B)) UNIV" ``` hoelzl@47694 ` 382` ``` proof (rule indep_sets_sigma) ``` hoelzl@42861 ` 383` ``` show "indep_sets (bool_case A B) UNIV" ``` hoelzl@42981 ` 384` ``` by (rule `indep_set A B`[unfolded indep_set_def]) ``` hoelzl@47694 ` 385` ``` fix i show "Int_stable (case i of True \ A | False \ B)" ``` hoelzl@42861 ` 386` ``` using A B by (cases i) auto ``` hoelzl@42861 ` 387` ``` qed ``` hoelzl@42861 ` 388` ``` then show ?thesis ``` hoelzl@42981 ` 389` ``` unfolding indep_set_def ``` hoelzl@42861 ` 390` ``` by (rule indep_sets_mono_sets) (auto split: bool.split) ``` hoelzl@42861 ` 391` ```qed ``` hoelzl@42861 ` 392` hoelzl@42981 ` 393` ```lemma (in prob_space) indep_sets_collect_sigma: ``` hoelzl@42981 ` 394` ``` fixes I :: "'j \ 'i set" and J :: "'j set" and E :: "'i \ 'a set set" ``` hoelzl@42981 ` 395` ``` assumes indep: "indep_sets E (\j\J. I j)" ``` hoelzl@47694 ` 396` ``` assumes Int_stable: "\i j. j \ J \ i \ I j \ Int_stable (E i)" ``` hoelzl@42981 ` 397` ``` assumes disjoint: "disjoint_family_on I J" ``` hoelzl@42981 ` 398` ``` shows "indep_sets (\j. sigma_sets (space M) (\i\I j. E i)) J" ``` hoelzl@42981 ` 399` ```proof - ``` wenzelm@46731 ` 400` ``` let ?E = "\j. {\k\K. E' k| E' K. finite K \ K \ {} \ K \ I j \ (\k\K. E' k \ E k) }" ``` hoelzl@42981 ` 401` hoelzl@42983 ` 402` ``` from indep have E: "\j i. j \ J \ i \ I j \ E i \ events" ``` hoelzl@42981 ` 403` ``` unfolding indep_sets_def by auto ``` hoelzl@42981 ` 404` ``` { fix j ``` hoelzl@47694 ` 405` ``` let ?S = "sigma_sets (space M) (\i\I j. E i)" ``` hoelzl@42981 ` 406` ``` assume "j \ J" ``` hoelzl@47694 ` 407` ``` from E[OF this] interpret S: sigma_algebra "space M" ?S ``` hoelzl@47694 ` 408` ``` using sets_into_space[of _ M] by (intro sigma_algebra_sigma_sets) auto ``` hoelzl@42981 ` 409` hoelzl@42981 ` 410` ``` have "sigma_sets (space M) (\i\I j. E i) = sigma_sets (space M) (?E j)" ``` hoelzl@42981 ` 411` ``` proof (rule sigma_sets_eqI) ``` hoelzl@42981 ` 412` ``` fix A assume "A \ (\i\I j. E i)" ``` hoelzl@42981 ` 413` ``` then guess i .. ``` hoelzl@42981 ` 414` ``` then show "A \ sigma_sets (space M) (?E j)" ``` hoelzl@47694 ` 415` ``` by (auto intro!: sigma_sets.intros(2-) exI[of _ "{i}"] exI[of _ "\i. A"]) ``` hoelzl@42981 ` 416` ``` next ``` hoelzl@42981 ` 417` ``` fix A assume "A \ ?E j" ``` hoelzl@42981 ` 418` ``` then obtain E' K where "finite K" "K \ {}" "K \ I j" "\k. k \ K \ E' k \ E k" ``` hoelzl@42981 ` 419` ``` and A: "A = (\k\K. E' k)" ``` hoelzl@42981 ` 420` ``` by auto ``` hoelzl@47694 ` 421` ``` then have "A \ ?S" unfolding A ``` hoelzl@47694 ` 422` ``` by (safe intro!: S.finite_INT) auto ``` hoelzl@42981 ` 423` ``` then show "A \ sigma_sets (space M) (\i\I j. E i)" ``` hoelzl@47694 ` 424` ``` by simp ``` hoelzl@42981 ` 425` ``` qed } ``` hoelzl@42981 ` 426` ``` moreover have "indep_sets (\j. sigma_sets (space M) (?E j)) J" ``` hoelzl@47694 ` 427` ``` proof (rule indep_sets_sigma) ``` hoelzl@42981 ` 428` ``` show "indep_sets ?E J" ``` hoelzl@42981 ` 429` ``` proof (intro indep_setsI) ``` hoelzl@42981 ` 430` ``` fix j assume "j \ J" with E show "?E j \ events" by (force intro!: finite_INT) ``` hoelzl@42981 ` 431` ``` next ``` hoelzl@42981 ` 432` ``` fix K A assume K: "K \ {}" "K \ J" "finite K" ``` hoelzl@42981 ` 433` ``` and "\j\K. A j \ ?E j" ``` hoelzl@42981 ` 434` ``` then have "\j\K. \E' L. A j = (\l\L. E' l) \ finite L \ L \ {} \ L \ I j \ (\l\L. E' l \ E l)" ``` hoelzl@42981 ` 435` ``` by simp ``` hoelzl@42981 ` 436` ``` from bchoice[OF this] guess E' .. ``` hoelzl@42981 ` 437` ``` from bchoice[OF this] obtain L ``` hoelzl@42981 ` 438` ``` where A: "\j. j\K \ A j = (\l\L j. E' j l)" ``` hoelzl@42981 ` 439` ``` and L: "\j. j\K \ finite (L j)" "\j. j\K \ L j \ {}" "\j. j\K \ L j \ I j" ``` hoelzl@42981 ` 440` ``` and E': "\j l. j\K \ l \ L j \ E' j l \ E l" ``` hoelzl@42981 ` 441` ``` by auto ``` hoelzl@42981 ` 442` hoelzl@42981 ` 443` ``` { fix k l j assume "k \ K" "j \ K" "l \ L j" "l \ L k" ``` hoelzl@42981 ` 444` ``` have "k = j" ``` hoelzl@42981 ` 445` ``` proof (rule ccontr) ``` hoelzl@42981 ` 446` ``` assume "k \ j" ``` hoelzl@42981 ` 447` ``` with disjoint `K \ J` `k \ K` `j \ K` have "I k \ I j = {}" ``` hoelzl@42981 ` 448` ``` unfolding disjoint_family_on_def by auto ``` hoelzl@42981 ` 449` ``` with L(2,3)[OF `j \ K`] L(2,3)[OF `k \ K`] ``` hoelzl@42981 ` 450` ``` show False using `l \ L k` `l \ L j` by auto ``` hoelzl@42981 ` 451` ``` qed } ``` hoelzl@42981 ` 452` ``` note L_inj = this ``` hoelzl@42981 ` 453` hoelzl@42981 ` 454` ``` def k \ "\l. (SOME k. k \ K \ l \ L k)" ``` hoelzl@42981 ` 455` ``` { fix x j l assume *: "j \ K" "l \ L j" ``` hoelzl@42981 ` 456` ``` have "k l = j" unfolding k_def ``` hoelzl@42981 ` 457` ``` proof (rule some_equality) ``` hoelzl@42981 ` 458` ``` fix k assume "k \ K \ l \ L k" ``` hoelzl@42981 ` 459` ``` with * L_inj show "k = j" by auto ``` hoelzl@42981 ` 460` ``` qed (insert *, simp) } ``` hoelzl@42981 ` 461` ``` note k_simp[simp] = this ``` wenzelm@46731 ` 462` ``` let ?E' = "\l. E' (k l) l" ``` hoelzl@42981 ` 463` ``` have "prob (\j\K. A j) = prob (\l\(\k\K. L k). ?E' l)" ``` hoelzl@42981 ` 464` ``` by (auto simp: A intro!: arg_cong[where f=prob]) ``` hoelzl@42981 ` 465` ``` also have "\ = (\l\(\k\K. L k). prob (?E' l))" ``` hoelzl@42981 ` 466` ``` using L K E' by (intro indep_setsD[OF indep]) (simp_all add: UN_mono) ``` hoelzl@42981 ` 467` ``` also have "\ = (\j\K. \l\L j. prob (E' j l))" ``` hoelzl@42981 ` 468` ``` using K L L_inj by (subst setprod_UN_disjoint) auto ``` hoelzl@42981 ` 469` ``` also have "\ = (\j\K. prob (A j))" ``` hoelzl@42981 ` 470` ``` using K L E' by (auto simp add: A intro!: setprod_cong indep_setsD[OF indep, symmetric]) blast ``` hoelzl@42981 ` 471` ``` finally show "prob (\j\K. A j) = (\j\K. prob (A j))" . ``` hoelzl@42981 ` 472` ``` qed ``` hoelzl@42981 ` 473` ``` next ``` hoelzl@42981 ` 474` ``` fix j assume "j \ J" ``` hoelzl@47694 ` 475` ``` show "Int_stable (?E j)" ``` hoelzl@42981 ` 476` ``` proof (rule Int_stableI) ``` hoelzl@42981 ` 477` ``` fix a assume "a \ ?E j" then obtain Ka Ea ``` hoelzl@42981 ` 478` ``` where a: "a = (\k\Ka. Ea k)" "finite Ka" "Ka \ {}" "Ka \ I j" "\k. k\Ka \ Ea k \ E k" by auto ``` hoelzl@42981 ` 479` ``` fix b assume "b \ ?E j" then obtain Kb Eb ``` hoelzl@42981 ` 480` ``` where b: "b = (\k\Kb. Eb k)" "finite Kb" "Kb \ {}" "Kb \ I j" "\k. k\Kb \ Eb k \ E k" by auto ``` hoelzl@42981 ` 481` ``` let ?A = "\k. (if k \ Ka \ Kb then Ea k \ Eb k else if k \ Kb then Eb k else if k \ Ka then Ea k else {})" ``` hoelzl@42981 ` 482` ``` have "a \ b = INTER (Ka \ Kb) ?A" ``` hoelzl@42981 ` 483` ``` by (simp add: a b set_eq_iff) auto ``` hoelzl@42981 ` 484` ``` with a b `j \ J` Int_stableD[OF Int_stable] show "a \ b \ ?E j" ``` hoelzl@42981 ` 485` ``` by (intro CollectI exI[of _ "Ka \ Kb"] exI[of _ ?A]) auto ``` hoelzl@42981 ` 486` ``` qed ``` hoelzl@42981 ` 487` ``` qed ``` hoelzl@42981 ` 488` ``` ultimately show ?thesis ``` hoelzl@42981 ` 489` ``` by (simp cong: indep_sets_cong) ``` hoelzl@42981 ` 490` ```qed ``` hoelzl@42981 ` 491` hoelzl@49772 ` 492` ```definition (in prob_space) tail_events where ``` hoelzl@49772 ` 493` ``` "tail_events A = (\n. sigma_sets (space M) (UNION {n..} A))" ``` hoelzl@42982 ` 494` hoelzl@49772 ` 495` ```lemma (in prob_space) tail_events_sets: ``` hoelzl@49772 ` 496` ``` assumes A: "\i::nat. A i \ events" ``` hoelzl@49772 ` 497` ``` shows "tail_events A \ events" ``` hoelzl@49772 ` 498` ```proof ``` hoelzl@49772 ` 499` ``` fix X assume X: "X \ tail_events A" ``` hoelzl@42982 ` 500` ``` let ?A = "(\n. sigma_sets (space M) (UNION {n..} A))" ``` hoelzl@49772 ` 501` ``` from X have "\n::nat. X \ sigma_sets (space M) (UNION {n..} A)" by (auto simp: tail_events_def) ``` hoelzl@42982 ` 502` ``` from this[of 0] have "X \ sigma_sets (space M) (UNION UNIV A)" by simp ``` hoelzl@42983 ` 503` ``` then show "X \ events" ``` hoelzl@42982 ` 504` ``` by induct (insert A, auto) ``` hoelzl@42982 ` 505` ```qed ``` hoelzl@42982 ` 506` hoelzl@49772 ` 507` ```lemma (in prob_space) sigma_algebra_tail_events: ``` hoelzl@47694 ` 508` ``` assumes "\i::nat. sigma_algebra (space M) (A i)" ``` hoelzl@49772 ` 509` ``` shows "sigma_algebra (space M) (tail_events A)" ``` hoelzl@49772 ` 510` ``` unfolding tail_events_def ``` hoelzl@42982 ` 511` ```proof (simp add: sigma_algebra_iff2, safe) ``` hoelzl@42982 ` 512` ``` let ?A = "(\n. sigma_sets (space M) (UNION {n..} A))" ``` hoelzl@47694 ` 513` ``` interpret A: sigma_algebra "space M" "A i" for i by fact ``` hoelzl@43340 ` 514` ``` { fix X x assume "X \ ?A" "x \ X" ``` hoelzl@42982 ` 515` ``` then have "\n. X \ sigma_sets (space M) (UNION {n..} A)" by auto ``` hoelzl@42982 ` 516` ``` from this[of 0] have "X \ sigma_sets (space M) (UNION UNIV A)" by simp ``` hoelzl@42982 ` 517` ``` then have "X \ space M" ``` hoelzl@42982 ` 518` ``` by induct (insert A.sets_into_space, auto) ``` hoelzl@42982 ` 519` ``` with `x \ X` show "x \ space M" by auto } ``` hoelzl@42982 ` 520` ``` { fix F :: "nat \ 'a set" and n assume "range F \ ?A" ``` hoelzl@42982 ` 521` ``` then show "(UNION UNIV F) \ sigma_sets (space M) (UNION {n..} A)" ``` hoelzl@42982 ` 522` ``` by (intro sigma_sets.Union) auto } ``` hoelzl@42982 ` 523` ```qed (auto intro!: sigma_sets.Compl sigma_sets.Empty) ``` hoelzl@42982 ` 524` hoelzl@42982 ` 525` ```lemma (in prob_space) kolmogorov_0_1_law: ``` hoelzl@42982 ` 526` ``` fixes A :: "nat \ 'a set set" ``` hoelzl@47694 ` 527` ``` assumes "\i::nat. sigma_algebra (space M) (A i)" ``` hoelzl@42982 ` 528` ``` assumes indep: "indep_sets A UNIV" ``` hoelzl@49772 ` 529` ``` and X: "X \ tail_events A" ``` hoelzl@42982 ` 530` ``` shows "prob X = 0 \ prob X = 1" ``` hoelzl@42982 ` 531` ```proof - ``` hoelzl@49781 ` 532` ``` have A: "\i. A i \ events" ``` hoelzl@49781 ` 533` ``` using indep unfolding indep_sets_def by simp ``` hoelzl@49781 ` 534` hoelzl@47694 ` 535` ``` let ?D = "{D \ events. prob (X \ D) = prob X * prob D}" ``` hoelzl@47694 ` 536` ``` interpret A: sigma_algebra "space M" "A i" for i by fact ``` hoelzl@49772 ` 537` ``` interpret T: sigma_algebra "space M" "tail_events A" ``` hoelzl@49772 ` 538` ``` by (rule sigma_algebra_tail_events) fact ``` hoelzl@42982 ` 539` ``` have "X \ space M" using T.space_closed X by auto ``` hoelzl@42982 ` 540` hoelzl@42983 ` 541` ``` have X_in: "X \ events" ``` hoelzl@49772 ` 542` ``` using tail_events_sets A X by auto ``` hoelzl@42982 ` 543` hoelzl@47694 ` 544` ``` interpret D: dynkin_system "space M" ?D ``` hoelzl@42982 ` 545` ``` proof (rule dynkin_systemI) ``` hoelzl@47694 ` 546` ``` fix D assume "D \ ?D" then show "D \ space M" ``` hoelzl@42982 ` 547` ``` using sets_into_space by auto ``` hoelzl@42982 ` 548` ``` next ``` hoelzl@47694 ` 549` ``` show "space M \ ?D" ``` hoelzl@42982 ` 550` ``` using prob_space `X \ space M` by (simp add: Int_absorb2) ``` hoelzl@42982 ` 551` ``` next ``` hoelzl@47694 ` 552` ``` fix A assume A: "A \ ?D" ``` hoelzl@42982 ` 553` ``` have "prob (X \ (space M - A)) = prob (X - (X \ A))" ``` hoelzl@42982 ` 554` ``` using `X \ space M` by (auto intro!: arg_cong[where f=prob]) ``` hoelzl@42982 ` 555` ``` also have "\ = prob X - prob (X \ A)" ``` hoelzl@42982 ` 556` ``` using X_in A by (intro finite_measure_Diff) auto ``` hoelzl@42982 ` 557` ``` also have "\ = prob X * prob (space M) - prob X * prob A" ``` hoelzl@42982 ` 558` ``` using A prob_space by auto ``` hoelzl@42982 ` 559` ``` also have "\ = prob X * prob (space M - A)" ``` hoelzl@42982 ` 560` ``` using X_in A sets_into_space ``` hoelzl@42982 ` 561` ``` by (subst finite_measure_Diff) (auto simp: field_simps) ``` hoelzl@47694 ` 562` ``` finally show "space M - A \ ?D" ``` hoelzl@42982 ` 563` ``` using A `X \ space M` by auto ``` hoelzl@42982 ` 564` ``` next ``` hoelzl@47694 ` 565` ``` fix F :: "nat \ 'a set" assume dis: "disjoint_family F" and "range F \ ?D" ``` hoelzl@42982 ` 566` ``` then have F: "range F \ events" "\i. prob (X \ F i) = prob X * prob (F i)" ``` hoelzl@42982 ` 567` ``` by auto ``` hoelzl@42982 ` 568` ``` have "(\i. prob (X \ F i)) sums prob (\i. X \ F i)" ``` hoelzl@42982 ` 569` ``` proof (rule finite_measure_UNION) ``` hoelzl@42982 ` 570` ``` show "range (\i. X \ F i) \ events" ``` hoelzl@42982 ` 571` ``` using F X_in by auto ``` hoelzl@42982 ` 572` ``` show "disjoint_family (\i. X \ F i)" ``` hoelzl@42982 ` 573` ``` using dis by (rule disjoint_family_on_bisimulation) auto ``` hoelzl@42982 ` 574` ``` qed ``` hoelzl@42982 ` 575` ``` with F have "(\i. prob X * prob (F i)) sums prob (X \ (\i. F i))" ``` hoelzl@42982 ` 576` ``` by simp ``` hoelzl@42982 ` 577` ``` moreover have "(\i. prob X * prob (F i)) sums (prob X * prob (\i. F i))" ``` huffman@44282 ` 578` ``` by (intro sums_mult finite_measure_UNION F dis) ``` hoelzl@42982 ` 579` ``` ultimately have "prob (X \ (\i. F i)) = prob X * prob (\i. F i)" ``` hoelzl@42982 ` 580` ``` by (auto dest!: sums_unique) ``` hoelzl@47694 ` 581` ``` with F show "(\i. F i) \ ?D" ``` hoelzl@42982 ` 582` ``` by auto ``` hoelzl@42982 ` 583` ``` qed ``` hoelzl@42982 ` 584` hoelzl@42982 ` 585` ``` { fix n ``` hoelzl@42982 ` 586` ``` have "indep_sets (\b. sigma_sets (space M) (\m\bool_case {..n} {Suc n..} b. A m)) UNIV" ``` hoelzl@42982 ` 587` ``` proof (rule indep_sets_collect_sigma) ``` hoelzl@42982 ` 588` ``` have *: "(\b. case b of True \ {..n} | False \ {Suc n..}) = UNIV" (is "?U = _") ``` hoelzl@42982 ` 589` ``` by (simp split: bool.split add: set_eq_iff) (metis not_less_eq_eq) ``` hoelzl@42982 ` 590` ``` with indep show "indep_sets A ?U" by simp ``` hoelzl@42982 ` 591` ``` show "disjoint_family (bool_case {..n} {Suc n..})" ``` hoelzl@42982 ` 592` ``` unfolding disjoint_family_on_def by (auto split: bool.split) ``` hoelzl@42982 ` 593` ``` fix m ``` hoelzl@47694 ` 594` ``` show "Int_stable (A m)" ``` hoelzl@42982 ` 595` ``` unfolding Int_stable_def using A.Int by auto ``` hoelzl@42982 ` 596` ``` qed ``` hoelzl@43340 ` 597` ``` also have "(\b. sigma_sets (space M) (\m\bool_case {..n} {Suc n..} b. A m)) = ``` hoelzl@42982 ` 598` ``` bool_case (sigma_sets (space M) (\m\{..n}. A m)) (sigma_sets (space M) (\m\{Suc n..}. A m))" ``` hoelzl@42982 ` 599` ``` by (auto intro!: ext split: bool.split) ``` hoelzl@42982 ` 600` ``` finally have indep: "indep_set (sigma_sets (space M) (\m\{..n}. A m)) (sigma_sets (space M) (\m\{Suc n..}. A m))" ``` hoelzl@42982 ` 601` ``` unfolding indep_set_def by simp ``` hoelzl@42982 ` 602` hoelzl@47694 ` 603` ``` have "sigma_sets (space M) (\m\{..n}. A m) \ ?D" ``` hoelzl@42982 ` 604` ``` proof (simp add: subset_eq, rule) ``` hoelzl@42982 ` 605` ``` fix D assume D: "D \ sigma_sets (space M) (\m\{..n}. A m)" ``` hoelzl@42982 ` 606` ``` have "X \ sigma_sets (space M) (\m\{Suc n..}. A m)" ``` hoelzl@49772 ` 607` ``` using X unfolding tail_events_def by simp ``` hoelzl@42982 ` 608` ``` from indep_setD[OF indep D this] indep_setD_ev1[OF indep] D ``` hoelzl@42982 ` 609` ``` show "D \ events \ prob (X \ D) = prob X * prob D" ``` hoelzl@42982 ` 610` ``` by (auto simp add: ac_simps) ``` hoelzl@42982 ` 611` ``` qed } ``` hoelzl@47694 ` 612` ``` then have "(\n. sigma_sets (space M) (\m\{..n}. A m)) \ ?D" (is "?A \ _") ``` hoelzl@42982 ` 613` ``` by auto ``` hoelzl@42982 ` 614` hoelzl@49772 ` 615` ``` note `X \ tail_events A` ``` hoelzl@47694 ` 616` ``` also { ``` hoelzl@47694 ` 617` ``` have "\n. sigma_sets (space M) (\i\{n..}. A i) \ sigma_sets (space M) ?A" ``` hoelzl@47694 ` 618` ``` by (intro sigma_sets_subseteq UN_mono) auto ``` hoelzl@49772 ` 619` ``` then have "tail_events A \ sigma_sets (space M) ?A" ``` hoelzl@49772 ` 620` ``` unfolding tail_events_def by auto } ``` hoelzl@47694 ` 621` ``` also have "sigma_sets (space M) ?A = dynkin (space M) ?A" ``` hoelzl@42982 ` 622` ``` proof (rule sigma_eq_dynkin) ``` hoelzl@42982 ` 623` ``` { fix B n assume "B \ sigma_sets (space M) (\m\{..n}. A m)" ``` hoelzl@42982 ` 624` ``` then have "B \ space M" ``` hoelzl@47694 ` 625` ``` by induct (insert A sets_into_space[of _ M], auto) } ``` hoelzl@47694 ` 626` ``` then show "?A \ Pow (space M)" by auto ``` hoelzl@47694 ` 627` ``` show "Int_stable ?A" ``` hoelzl@42982 ` 628` ``` proof (rule Int_stableI) ``` hoelzl@42982 ` 629` ``` fix a assume "a \ ?A" then guess n .. note a = this ``` hoelzl@42982 ` 630` ``` fix b assume "b \ ?A" then guess m .. note b = this ``` hoelzl@47694 ` 631` ``` interpret Amn: sigma_algebra "space M" "sigma_sets (space M) (\i\{..max m n}. A i)" ``` hoelzl@47694 ` 632` ``` using A sets_into_space[of _ M] by (intro sigma_algebra_sigma_sets) auto ``` hoelzl@42982 ` 633` ``` have "sigma_sets (space M) (\i\{..n}. A i) \ sigma_sets (space M) (\i\{..max m n}. A i)" ``` hoelzl@42982 ` 634` ``` by (intro sigma_sets_subseteq UN_mono) auto ``` hoelzl@42982 ` 635` ``` with a have "a \ sigma_sets (space M) (\i\{..max m n}. A i)" by auto ``` hoelzl@42982 ` 636` ``` moreover ``` hoelzl@42982 ` 637` ``` have "sigma_sets (space M) (\i\{..m}. A i) \ sigma_sets (space M) (\i\{..max m n}. A i)" ``` hoelzl@42982 ` 638` ``` by (intro sigma_sets_subseteq UN_mono) auto ``` hoelzl@42982 ` 639` ``` with b have "b \ sigma_sets (space M) (\i\{..max m n}. A i)" by auto ``` hoelzl@42982 ` 640` ``` ultimately have "a \ b \ sigma_sets (space M) (\i\{..max m n}. A i)" ``` hoelzl@47694 ` 641` ``` using Amn.Int[of a b] by simp ``` hoelzl@42982 ` 642` ``` then show "a \ b \ (\n. sigma_sets (space M) (\i\{..n}. A i))" by auto ``` hoelzl@42982 ` 643` ``` qed ``` hoelzl@42982 ` 644` ``` qed ``` hoelzl@47694 ` 645` ``` also have "dynkin (space M) ?A \ ?D" ``` hoelzl@47694 ` 646` ``` using `?A \ ?D` by (auto intro!: D.dynkin_subset) ``` hoelzl@47694 ` 647` ``` finally show ?thesis by auto ``` hoelzl@42982 ` 648` ```qed ``` hoelzl@42982 ` 649` hoelzl@42985 ` 650` ```lemma (in prob_space) borel_0_1_law: ``` hoelzl@42985 ` 651` ``` fixes F :: "nat \ 'a set" ``` hoelzl@49781 ` 652` ``` assumes F2: "indep_events F UNIV" ``` hoelzl@42985 ` 653` ``` shows "prob (\n. \m\{n..}. F m) = 0 \ prob (\n. \m\{n..}. F m) = 1" ``` hoelzl@42985 ` 654` ```proof (rule kolmogorov_0_1_law[of "\i. sigma_sets (space M) { F i }"]) ``` hoelzl@49781 ` 655` ``` have F1: "range F \ events" ``` hoelzl@49781 ` 656` ``` using F2 by (simp add: indep_events_def subset_eq) ``` hoelzl@47694 ` 657` ``` { fix i show "sigma_algebra (space M) (sigma_sets (space M) {F i})" ``` hoelzl@49781 ` 658` ``` using sigma_algebra_sigma_sets[of "{F i}" "space M"] F1 sets_into_space ``` hoelzl@47694 ` 659` ``` by auto } ``` hoelzl@42985 ` 660` ``` show "indep_sets (\i. sigma_sets (space M) {F i}) UNIV" ``` hoelzl@47694 ` 661` ``` proof (rule indep_sets_sigma) ``` hoelzl@42985 ` 662` ``` show "indep_sets (\i. {F i}) UNIV" ``` hoelzl@42985 ` 663` ``` unfolding indep_sets_singleton_iff_indep_events by fact ``` hoelzl@47694 ` 664` ``` fix i show "Int_stable {F i}" ``` hoelzl@42985 ` 665` ``` unfolding Int_stable_def by simp ``` hoelzl@42985 ` 666` ``` qed ``` wenzelm@46731 ` 667` ``` let ?Q = "\n. \i\{n..}. F i" ``` hoelzl@49772 ` 668` ``` show "(\n. \m\{n..}. F m) \ tail_events (\i. sigma_sets (space M) {F i})" ``` hoelzl@49772 ` 669` ``` unfolding tail_events_def ``` hoelzl@42985 ` 670` ``` proof ``` hoelzl@42985 ` 671` ``` fix j ``` hoelzl@47694 ` 672` ``` interpret S: sigma_algebra "space M" "sigma_sets (space M) (\i\{j..}. sigma_sets (space M) {F i})" ``` hoelzl@49781 ` 673` ``` using order_trans[OF F1 space_closed] ``` hoelzl@47694 ` 674` ``` by (intro sigma_algebra_sigma_sets) (simp add: sigma_sets_singleton subset_eq) ``` hoelzl@42985 ` 675` ``` have "(\n. ?Q n) = (\n\{j..}. ?Q n)" ``` hoelzl@42985 ` 676` ``` by (intro decseq_SucI INT_decseq_offset UN_mono) auto ``` hoelzl@47694 ` 677` ``` also have "\ \ sigma_sets (space M) (\i\{j..}. sigma_sets (space M) {F i})" ``` hoelzl@49781 ` 678` ``` using order_trans[OF F1 space_closed] ``` hoelzl@42985 ` 679` ``` by (safe intro!: S.countable_INT S.countable_UN) ``` hoelzl@47694 ` 680` ``` (auto simp: sigma_sets_singleton intro!: sigma_sets.Basic bexI) ``` hoelzl@42985 ` 681` ``` finally show "(\n. ?Q n) \ sigma_sets (space M) (\i\{j..}. sigma_sets (space M) {F i})" ``` hoelzl@47694 ` 682` ``` by simp ``` hoelzl@42985 ` 683` ``` qed ``` hoelzl@42985 ` 684` ```qed ``` hoelzl@42985 ` 685` hoelzl@42987 ` 686` ```lemma (in prob_space) indep_sets_finite: ``` hoelzl@42987 ` 687` ``` assumes I: "I \ {}" "finite I" ``` hoelzl@42987 ` 688` ``` and F: "\i. i \ I \ F i \ events" "\i. i \ I \ space M \ F i" ``` hoelzl@42987 ` 689` ``` shows "indep_sets F I \ (\A\Pi I F. prob (\j\I. A j) = (\j\I. prob (A j)))" ``` hoelzl@42987 ` 690` ```proof ``` hoelzl@42987 ` 691` ``` assume *: "indep_sets F I" ``` hoelzl@42987 ` 692` ``` from I show "\A\Pi I F. prob (\j\I. A j) = (\j\I. prob (A j))" ``` hoelzl@42987 ` 693` ``` by (intro indep_setsD[OF *] ballI) auto ``` hoelzl@42987 ` 694` ```next ``` hoelzl@42987 ` 695` ``` assume indep: "\A\Pi I F. prob (\j\I. A j) = (\j\I. prob (A j))" ``` hoelzl@42987 ` 696` ``` show "indep_sets F I" ``` hoelzl@42987 ` 697` ``` proof (rule indep_setsI[OF F(1)]) ``` hoelzl@42987 ` 698` ``` fix A J assume J: "J \ {}" "J \ I" "finite J" ``` hoelzl@42987 ` 699` ``` assume A: "\j\J. A j \ F j" ``` wenzelm@46731 ` 700` ``` let ?A = "\j. if j \ J then A j else space M" ``` hoelzl@42987 ` 701` ``` have "prob (\j\I. ?A j) = prob (\j\J. A j)" ``` hoelzl@42987 ` 702` ``` using subset_trans[OF F(1) space_closed] J A ``` hoelzl@42987 ` 703` ``` by (auto intro!: arg_cong[where f=prob] split: split_if_asm) blast ``` hoelzl@42987 ` 704` ``` also ``` hoelzl@42987 ` 705` ``` from A F have "(\j. if j \ J then A j else space M) \ Pi I F" (is "?A \ _") ``` hoelzl@42987 ` 706` ``` by (auto split: split_if_asm) ``` hoelzl@42987 ` 707` ``` with indep have "prob (\j\I. ?A j) = (\j\I. prob (?A j))" ``` hoelzl@42987 ` 708` ``` by auto ``` hoelzl@42987 ` 709` ``` also have "\ = (\j\J. prob (A j))" ``` hoelzl@42987 ` 710` ``` unfolding if_distrib setprod.If_cases[OF `finite I`] ``` hoelzl@42987 ` 711` ``` using prob_space `J \ I` by (simp add: Int_absorb1 setprod_1) ``` hoelzl@42987 ` 712` ``` finally show "prob (\j\J. A j) = (\j\J. prob (A j))" .. ``` hoelzl@42987 ` 713` ``` qed ``` hoelzl@42987 ` 714` ```qed ``` hoelzl@42987 ` 715` hoelzl@42989 ` 716` ```lemma (in prob_space) indep_vars_finite: ``` hoelzl@42987 ` 717` ``` fixes I :: "'i set" ``` hoelzl@42987 ` 718` ``` assumes I: "I \ {}" "finite I" ``` hoelzl@47694 ` 719` ``` and M': "\i. i \ I \ sets (M' i) = sigma_sets (space (M' i)) (E i)" ``` hoelzl@47694 ` 720` ``` and rv: "\i. i \ I \ random_variable (M' i) (X i)" ``` hoelzl@47694 ` 721` ``` and Int_stable: "\i. i \ I \ Int_stable (E i)" ``` hoelzl@47694 ` 722` ``` and space: "\i. i \ I \ space (M' i) \ E i" and closed: "\i. i \ I \ E i \ Pow (space (M' i))" ``` hoelzl@47694 ` 723` ``` shows "indep_vars M' X I \ ``` hoelzl@47694 ` 724` ``` (\A\(\ i\I. E i). prob (\j\I. X j -` A j \ space M) = (\j\I. prob (X j -` A j \ space M)))" ``` hoelzl@42987 ` 725` ```proof - ``` hoelzl@42987 ` 726` ``` from rv have X: "\i. i \ I \ X i \ space M \ space (M' i)" ``` hoelzl@42987 ` 727` ``` unfolding measurable_def by simp ``` hoelzl@42987 ` 728` hoelzl@42987 ` 729` ``` { fix i assume "i\I" ``` hoelzl@47694 ` 730` ``` from closed[OF `i \ I`] ``` hoelzl@47694 ` 731` ``` have "sigma_sets (space M) {X i -` A \ space M |A. A \ sets (M' i)} ``` hoelzl@47694 ` 732` ``` = sigma_sets (space M) {X i -` A \ space M |A. A \ E i}" ``` hoelzl@47694 ` 733` ``` unfolding sigma_sets_vimage_commute[OF X, OF `i \ I`, symmetric] M'[OF `i \ I`] ``` hoelzl@42987 ` 734` ``` by (subst sigma_sets_sigma_sets_eq) auto } ``` hoelzl@47694 ` 735` ``` note sigma_sets_X = this ``` hoelzl@42987 ` 736` hoelzl@42987 ` 737` ``` { fix i assume "i\I" ``` hoelzl@47694 ` 738` ``` have "Int_stable {X i -` A \ space M |A. A \ E i}" ``` hoelzl@42987 ` 739` ``` proof (rule Int_stableI) ``` hoelzl@47694 ` 740` ``` fix a assume "a \ {X i -` A \ space M |A. A \ E i}" ``` hoelzl@47694 ` 741` ``` then obtain A where "a = X i -` A \ space M" "A \ E i" by auto ``` hoelzl@42987 ` 742` ``` moreover ``` hoelzl@47694 ` 743` ``` fix b assume "b \ {X i -` A \ space M |A. A \ E i}" ``` hoelzl@47694 ` 744` ``` then obtain B where "b = X i -` B \ space M" "B \ E i" by auto ``` hoelzl@42987 ` 745` ``` moreover ``` hoelzl@42987 ` 746` ``` have "(X i -` A \ space M) \ (X i -` B \ space M) = X i -` (A \ B) \ space M" by auto ``` hoelzl@42987 ` 747` ``` moreover note Int_stable[OF `i \ I`] ``` hoelzl@42987 ` 748` ``` ultimately ``` hoelzl@47694 ` 749` ``` show "a \ b \ {X i -` A \ space M |A. A \ E i}" ``` hoelzl@42987 ` 750` ``` by (auto simp del: vimage_Int intro!: exI[of _ "A \ B"] dest: Int_stableD) ``` hoelzl@42987 ` 751` ``` qed } ``` hoelzl@47694 ` 752` ``` note indep_sets_X = indep_sets_sigma_sets_iff[OF this] ``` hoelzl@43340 ` 753` hoelzl@42987 ` 754` ``` { fix i assume "i \ I" ``` hoelzl@47694 ` 755` ``` { fix A assume "A \ E i" ``` hoelzl@47694 ` 756` ``` with M'[OF `i \ I`] have "A \ sets (M' i)" by auto ``` hoelzl@42987 ` 757` ``` moreover ``` hoelzl@47694 ` 758` ``` from rv[OF `i\I`] have "X i \ measurable M (M' i)" by auto ``` hoelzl@42987 ` 759` ``` ultimately ``` hoelzl@42987 ` 760` ``` have "X i -` A \ space M \ sets M" by (auto intro: measurable_sets) } ``` hoelzl@42987 ` 761` ``` with X[OF `i\I`] space[OF `i\I`] ``` hoelzl@47694 ` 762` ``` have "{X i -` A \ space M |A. A \ E i} \ events" ``` hoelzl@47694 ` 763` ``` "space M \ {X i -` A \ space M |A. A \ E i}" ``` hoelzl@42987 ` 764` ``` by (auto intro!: exI[of _ "space (M' i)"]) } ``` hoelzl@47694 ` 765` ``` note indep_sets_finite_X = indep_sets_finite[OF I this] ``` hoelzl@43340 ` 766` hoelzl@47694 ` 767` ``` have "(\A\\ i\I. {X i -` A \ space M |A. A \ E i}. prob (INTER I A) = (\j\I. prob (A j))) = ``` hoelzl@47694 ` 768` ``` (\A\\ i\I. E i. prob ((\j\I. X j -` A j) \ space M) = (\x\I. prob (X x -` A x \ space M)))" ``` hoelzl@42987 ` 769` ``` (is "?L = ?R") ``` hoelzl@42987 ` 770` ``` proof safe ``` hoelzl@47694 ` 771` ``` fix A assume ?L and A: "A \ (\ i\I. E i)" ``` hoelzl@42987 ` 772` ``` from `?L`[THEN bspec, of "\i. X i -` A i \ space M"] A `I \ {}` ``` hoelzl@42987 ` 773` ``` show "prob ((\j\I. X j -` A j) \ space M) = (\x\I. prob (X x -` A x \ space M))" ``` hoelzl@42987 ` 774` ``` by (auto simp add: Pi_iff) ``` hoelzl@42987 ` 775` ``` next ``` hoelzl@47694 ` 776` ``` fix A assume ?R and A: "A \ (\ i\I. {X i -` A \ space M |A. A \ E i})" ``` hoelzl@47694 ` 777` ``` from A have "\i\I. \B. A i = X i -` B \ space M \ B \ E i" by auto ``` hoelzl@42987 ` 778` ``` from bchoice[OF this] obtain B where B: "\i\I. A i = X i -` B i \ space M" ``` hoelzl@47694 ` 779` ``` "B \ (\ i\I. E i)" by auto ``` hoelzl@42987 ` 780` ``` from `?R`[THEN bspec, OF B(2)] B(1) `I \ {}` ``` hoelzl@42987 ` 781` ``` show "prob (INTER I A) = (\j\I. prob (A j))" ``` hoelzl@42987 ` 782` ``` by simp ``` hoelzl@42987 ` 783` ``` qed ``` hoelzl@42987 ` 784` ``` then show ?thesis using `I \ {}` ``` hoelzl@47694 ` 785` ``` by (simp add: rv indep_vars_def indep_sets_X sigma_sets_X indep_sets_finite_X cong: indep_sets_cong) ``` hoelzl@42988 ` 786` ```qed ``` hoelzl@42988 ` 787` hoelzl@42989 ` 788` ```lemma (in prob_space) indep_vars_compose: ``` hoelzl@42989 ` 789` ``` assumes "indep_vars M' X I" ``` hoelzl@47694 ` 790` ``` assumes rv: "\i. i \ I \ Y i \ measurable (M' i) (N i)" ``` hoelzl@42989 ` 791` ``` shows "indep_vars N (\i. Y i \ X i) I" ``` hoelzl@42989 ` 792` ``` unfolding indep_vars_def ``` hoelzl@42988 ` 793` ```proof ``` hoelzl@42989 ` 794` ``` from rv `indep_vars M' X I` ``` hoelzl@42988 ` 795` ``` show "\i\I. random_variable (N i) (Y i \ X i)" ``` hoelzl@47694 ` 796` ``` by (auto simp: indep_vars_def) ``` hoelzl@42988 ` 797` hoelzl@42988 ` 798` ``` have "indep_sets (\i. sigma_sets (space M) {X i -` A \ space M |A. A \ sets (M' i)}) I" ``` hoelzl@42989 ` 799` ``` using `indep_vars M' X I` by (simp add: indep_vars_def) ``` hoelzl@42988 ` 800` ``` then show "indep_sets (\i. sigma_sets (space M) {(Y i \ X i) -` A \ space M |A. A \ sets (N i)}) I" ``` hoelzl@42988 ` 801` ``` proof (rule indep_sets_mono_sets) ``` hoelzl@42988 ` 802` ``` fix i assume "i \ I" ``` hoelzl@42989 ` 803` ``` with `indep_vars M' X I` have X: "X i \ space M \ space (M' i)" ``` hoelzl@42989 ` 804` ``` unfolding indep_vars_def measurable_def by auto ``` hoelzl@42988 ` 805` ``` { fix A assume "A \ sets (N i)" ``` hoelzl@42988 ` 806` ``` then have "\B. (Y i \ X i) -` A \ space M = X i -` B \ space M \ B \ sets (M' i)" ``` hoelzl@42988 ` 807` ``` by (intro exI[of _ "Y i -` A \ space (M' i)"]) ``` hoelzl@42988 ` 808` ``` (auto simp: vimage_compose intro!: measurable_sets rv `i \ I` funcset_mem[OF X]) } ``` hoelzl@42988 ` 809` ``` then show "sigma_sets (space M) {(Y i \ X i) -` A \ space M |A. A \ sets (N i)} \ ``` hoelzl@42988 ` 810` ``` sigma_sets (space M) {X i -` A \ space M |A. A \ sets (M' i)}" ``` hoelzl@42988 ` 811` ``` by (intro sigma_sets_subseteq) (auto simp: vimage_compose) ``` hoelzl@42988 ` 812` ``` qed ``` hoelzl@42988 ` 813` ```qed ``` hoelzl@42988 ` 814` hoelzl@47694 ` 815` ```lemma (in prob_space) indep_varsD_finite: ``` hoelzl@42989 ` 816` ``` assumes X: "indep_vars M' X I" ``` hoelzl@42988 ` 817` ``` assumes I: "I \ {}" "finite I" "\i. i \ I \ A i \ sets (M' i)" ``` hoelzl@42988 ` 818` ``` shows "prob (\i\I. X i -` A i \ space M) = (\i\I. prob (X i -` A i \ space M))" ``` hoelzl@42988 ` 819` ```proof (rule indep_setsD) ``` hoelzl@42988 ` 820` ``` show "indep_sets (\i. sigma_sets (space M) {X i -` A \ space M |A. A \ sets (M' i)}) I" ``` hoelzl@42989 ` 821` ``` using X by (auto simp: indep_vars_def) ``` hoelzl@42988 ` 822` ``` show "I \ I" "I \ {}" "finite I" using I by auto ``` hoelzl@42988 ` 823` ``` show "\i\I. X i -` A i \ space M \ sigma_sets (space M) {X i -` A \ space M |A. A \ sets (M' i)}" ``` hoelzl@47694 ` 824` ``` using I by auto ``` hoelzl@42988 ` 825` ```qed ``` hoelzl@42988 ` 826` hoelzl@47694 ` 827` ```lemma (in prob_space) indep_varsD: ``` hoelzl@47694 ` 828` ``` assumes X: "indep_vars M' X I" ``` hoelzl@47694 ` 829` ``` assumes I: "J \ {}" "finite J" "J \ I" "\i. i \ J \ A i \ sets (M' i)" ``` hoelzl@47694 ` 830` ``` shows "prob (\i\J. X i -` A i \ space M) = (\i\J. prob (X i -` A i \ space M))" ``` hoelzl@47694 ` 831` ```proof (rule indep_setsD) ``` hoelzl@47694 ` 832` ``` show "indep_sets (\i. sigma_sets (space M) {X i -` A \ space M |A. A \ sets (M' i)}) I" ``` hoelzl@47694 ` 833` ``` using X by (auto simp: indep_vars_def) ``` hoelzl@47694 ` 834` ``` show "\i\J. X i -` A i \ space M \ sigma_sets (space M) {X i -` A \ space M |A. A \ sets (M' i)}" ``` hoelzl@47694 ` 835` ``` using I by auto ``` hoelzl@47694 ` 836` ```qed fact+ ``` hoelzl@47694 ` 837` hoelzl@47694 ` 838` ```lemma prod_algebra_cong: ``` hoelzl@47694 ` 839` ``` assumes "I = J" and sets: "(\i. i \ I \ sets (M i) = sets (N i))" ``` hoelzl@47694 ` 840` ``` shows "prod_algebra I M = prod_algebra J N" ``` hoelzl@47694 ` 841` ```proof - ``` hoelzl@47694 ` 842` ``` have space: "\i. i \ I \ space (M i) = space (N i)" ``` hoelzl@47694 ` 843` ``` using sets_eq_imp_space_eq[OF sets] by auto ``` hoelzl@47694 ` 844` ``` with sets show ?thesis unfolding `I = J` ``` hoelzl@47694 ` 845` ``` by (intro antisym prod_algebra_mono) auto ``` hoelzl@47694 ` 846` ```qed ``` hoelzl@47694 ` 847` hoelzl@47694 ` 848` ```lemma space_in_prod_algebra: ``` hoelzl@47694 ` 849` ``` "(\\<^isub>E i\I. space (M i)) \ prod_algebra I M" ``` hoelzl@47694 ` 850` ```proof cases ``` hoelzl@47694 ` 851` ``` assume "I = {}" then show ?thesis ``` hoelzl@47694 ` 852` ``` by (auto simp add: prod_algebra_def image_iff prod_emb_def) ``` hoelzl@47694 ` 853` ```next ``` hoelzl@47694 ` 854` ``` assume "I \ {}" ``` hoelzl@47694 ` 855` ``` then obtain i where "i \ I" by auto ``` hoelzl@47694 ` 856` ``` then have "(\\<^isub>E i\I. space (M i)) = prod_emb I M {i} (\\<^isub>E i\{i}. space (M i))" ``` hoelzl@47694 ` 857` ``` by (auto simp: prod_emb_def Pi_iff) ``` hoelzl@47694 ` 858` ``` also have "\ \ prod_algebra I M" ``` hoelzl@47694 ` 859` ``` using `i \ I` by (intro prod_algebraI) auto ``` hoelzl@47694 ` 860` ``` finally show ?thesis . ``` hoelzl@47694 ` 861` ```qed ``` hoelzl@47694 ` 862` hoelzl@47694 ` 863` ```lemma (in prob_space) indep_vars_iff_distr_eq_PiM: ``` hoelzl@47694 ` 864` ``` fixes I :: "'i set" and X :: "'i \ 'a \ 'b" ``` hoelzl@47694 ` 865` ``` assumes "I \ {}" ``` hoelzl@42988 ` 866` ``` assumes rv: "\i. random_variable (M' i) (X i)" ``` hoelzl@42989 ` 867` ``` shows "indep_vars M' X I \ ``` hoelzl@47694 ` 868` ``` distr M (\\<^isub>M i\I. M' i) (\x. \i\I. X i x) = (\\<^isub>M i\I. distr M (M' i) (X i))" ``` hoelzl@42988 ` 869` ```proof - ``` hoelzl@47694 ` 870` ``` let ?P = "\\<^isub>M i\I. M' i" ``` hoelzl@47694 ` 871` ``` let ?X = "\x. \i\I. X i x" ``` hoelzl@47694 ` 872` ``` let ?D = "distr M ?P ?X" ``` hoelzl@47694 ` 873` ``` have X: "random_variable ?P ?X" by (intro measurable_restrict rv) ``` hoelzl@47694 ` 874` ``` interpret D: prob_space ?D by (intro prob_space_distr X) ``` hoelzl@42988 ` 875` hoelzl@47694 ` 876` ``` let ?D' = "\i. distr M (M' i) (X i)" ``` hoelzl@47694 ` 877` ``` let ?P' = "\\<^isub>M i\I. distr M (M' i) (X i)" ``` hoelzl@47694 ` 878` ``` interpret D': prob_space "?D' i" for i by (intro prob_space_distr rv) ``` hoelzl@47694 ` 879` ``` interpret P: product_prob_space ?D' I .. ``` hoelzl@47694 ` 880` ``` ``` hoelzl@42988 ` 881` ``` show ?thesis ``` hoelzl@47694 ` 882` ``` proof ``` hoelzl@42989 ` 883` ``` assume "indep_vars M' X I" ``` hoelzl@47694 ` 884` ``` show "?D = ?P'" ``` hoelzl@47694 ` 885` ``` proof (rule measure_eqI_generator_eq) ``` hoelzl@47694 ` 886` ``` show "Int_stable (prod_algebra I M')" ``` hoelzl@47694 ` 887` ``` by (rule Int_stable_prod_algebra) ``` hoelzl@47694 ` 888` ``` show "prod_algebra I M' \ Pow (space ?P)" ``` hoelzl@47694 ` 889` ``` using prod_algebra_sets_into_space by (simp add: space_PiM) ``` hoelzl@47694 ` 890` ``` show "sets ?D = sigma_sets (space ?P) (prod_algebra I M')" ``` hoelzl@47694 ` 891` ``` by (simp add: sets_PiM space_PiM) ``` hoelzl@47694 ` 892` ``` show "sets ?P' = sigma_sets (space ?P) (prod_algebra I M')" ``` hoelzl@47694 ` 893` ``` by (simp add: sets_PiM space_PiM cong: prod_algebra_cong) ``` hoelzl@47694 ` 894` ``` let ?A = "\i. \\<^isub>E i\I. space (M' i)" ``` hoelzl@47694 ` 895` ``` show "range ?A \ prod_algebra I M'" "incseq ?A" "(\i. ?A i) = space (Pi\<^isub>M I M')" ``` hoelzl@47694 ` 896` ``` by (auto simp: space_PiM intro!: space_in_prod_algebra cong: prod_algebra_cong) ``` hoelzl@47694 ` 897` ``` { fix i show "emeasure ?D (\\<^isub>E i\I. space (M' i)) \ \" by auto } ``` hoelzl@47694 ` 898` ``` next ``` hoelzl@47694 ` 899` ``` fix E assume E: "E \ prod_algebra I M'" ``` hoelzl@47694 ` 900` ``` from prod_algebraE[OF E] guess J Y . note J = this ``` hoelzl@43340 ` 901` hoelzl@47694 ` 902` ``` from E have "E \ sets ?P" by (auto simp: sets_PiM) ``` hoelzl@47694 ` 903` ``` then have "emeasure ?D E = emeasure M (?X -` E \ space M)" ``` hoelzl@47694 ` 904` ``` by (simp add: emeasure_distr X) ``` hoelzl@47694 ` 905` ``` also have "?X -` E \ space M = (\i\J. X i -` Y i \ space M)" ``` hoelzl@47694 ` 906` ``` using J `I \ {}` measurable_space[OF rv] by (auto simp: prod_emb_def Pi_iff split: split_if_asm) ``` hoelzl@47694 ` 907` ``` also have "emeasure M (\i\J. X i -` Y i \ space M) = (\ i\J. emeasure M (X i -` Y i \ space M))" ``` hoelzl@47694 ` 908` ``` using `indep_vars M' X I` J `I \ {}` using indep_varsD[of M' X I J] ``` hoelzl@47694 ` 909` ``` by (auto simp: emeasure_eq_measure setprod_ereal) ``` hoelzl@47694 ` 910` ``` also have "\ = (\ i\J. emeasure (?D' i) (Y i))" ``` hoelzl@47694 ` 911` ``` using rv J by (simp add: emeasure_distr) ``` hoelzl@47694 ` 912` ``` also have "\ = emeasure ?P' E" ``` hoelzl@47694 ` 913` ``` using P.emeasure_PiM_emb[of J Y] J by (simp add: prod_emb_def) ``` hoelzl@47694 ` 914` ``` finally show "emeasure ?D E = emeasure ?P' E" . ``` hoelzl@42988 ` 915` ``` qed ``` hoelzl@42988 ` 916` ``` next ``` hoelzl@47694 ` 917` ``` assume "?D = ?P'" ``` hoelzl@47694 ` 918` ``` show "indep_vars M' X I" unfolding indep_vars_def ``` hoelzl@47694 ` 919` ``` proof (intro conjI indep_setsI ballI rv) ``` hoelzl@47694 ` 920` ``` fix i show "sigma_sets (space M) {X i -` A \ space M |A. A \ sets (M' i)} \ events" ``` hoelzl@47694 ` 921` ``` by (auto intro!: sigma_sets_subset measurable_sets rv) ``` hoelzl@42988 ` 922` ``` next ``` hoelzl@47694 ` 923` ``` fix J Y' assume J: "J \ {}" "J \ I" "finite J" ``` hoelzl@47694 ` 924` ``` assume Y': "\j\J. Y' j \ sigma_sets (space M) {X j -` A \ space M |A. A \ sets (M' j)}" ``` hoelzl@47694 ` 925` ``` have "\j\J. \Y. Y' j = X j -` Y \ space M \ Y \ sets (M' j)" ``` hoelzl@42988 ` 926` ``` proof ``` hoelzl@47694 ` 927` ``` fix j assume "j \ J" ``` hoelzl@47694 ` 928` ``` from Y'[rule_format, OF this] rv[of j] ``` hoelzl@47694 ` 929` ``` show "\Y. Y' j = X j -` Y \ space M \ Y \ sets (M' j)" ``` hoelzl@47694 ` 930` ``` by (subst (asm) sigma_sets_vimage_commute[symmetric, of _ _ "space (M' j)"]) ``` hoelzl@47694 ` 931` ``` (auto dest: measurable_space simp: sigma_sets_eq) ``` hoelzl@42988 ` 932` ``` qed ``` hoelzl@47694 ` 933` ``` from bchoice[OF this] obtain Y where ``` hoelzl@47694 ` 934` ``` Y: "\j. j \ J \ Y' j = X j -` Y j \ space M" "\j. j \ J \ Y j \ sets (M' j)" by auto ``` hoelzl@47694 ` 935` ``` let ?E = "prod_emb I M' J (Pi\<^isub>E J Y)" ``` hoelzl@47694 ` 936` ``` from Y have "(\j\J. Y' j) = ?X -` ?E \ space M" ``` hoelzl@47694 ` 937` ``` using J `I \ {}` measurable_space[OF rv] by (auto simp: prod_emb_def Pi_iff split: split_if_asm) ``` hoelzl@47694 ` 938` ``` then have "emeasure M (\j\J. Y' j) = emeasure M (?X -` ?E \ space M)" ``` hoelzl@47694 ` 939` ``` by simp ``` hoelzl@47694 ` 940` ``` also have "\ = emeasure ?D ?E" ``` hoelzl@47694 ` 941` ``` using Y J by (intro emeasure_distr[symmetric] X sets_PiM_I) auto ``` hoelzl@47694 ` 942` ``` also have "\ = emeasure ?P' ?E" ``` hoelzl@47694 ` 943` ``` using `?D = ?P'` by simp ``` hoelzl@47694 ` 944` ``` also have "\ = (\ i\J. emeasure (?D' i) (Y i))" ``` hoelzl@47694 ` 945` ``` using P.emeasure_PiM_emb[of J Y] J Y by (simp add: prod_emb_def) ``` hoelzl@47694 ` 946` ``` also have "\ = (\ i\J. emeasure M (Y' i))" ``` hoelzl@47694 ` 947` ``` using rv J Y by (simp add: emeasure_distr) ``` hoelzl@47694 ` 948` ``` finally have "emeasure M (\j\J. Y' j) = (\ i\J. emeasure M (Y' i))" . ``` hoelzl@47694 ` 949` ``` then show "prob (\j\J. Y' j) = (\ i\J. prob (Y' i))" ``` hoelzl@47694 ` 950` ``` by (auto simp: emeasure_eq_measure setprod_ereal) ``` hoelzl@42988 ` 951` ``` qed ``` hoelzl@42988 ` 952` ``` qed ``` hoelzl@42987 ` 953` ```qed ``` hoelzl@42987 ` 954` hoelzl@42989 ` 955` ```lemma (in prob_space) indep_varD: ``` hoelzl@42989 ` 956` ``` assumes indep: "indep_var Ma A Mb B" ``` hoelzl@42989 ` 957` ``` assumes sets: "Xa \ sets Ma" "Xb \ sets Mb" ``` hoelzl@42989 ` 958` ``` shows "prob ((\x. (A x, B x)) -` (Xa \ Xb) \ space M) = ``` hoelzl@42989 ` 959` ``` prob (A -` Xa \ space M) * prob (B -` Xb \ space M)" ``` hoelzl@42989 ` 960` ```proof - ``` hoelzl@42989 ` 961` ``` have "prob ((\x. (A x, B x)) -` (Xa \ Xb) \ space M) = ``` hoelzl@42989 ` 962` ``` prob (\i\UNIV. (bool_case A B i -` bool_case Xa Xb i \ space M))" ``` hoelzl@42989 ` 963` ``` by (auto intro!: arg_cong[where f=prob] simp: UNIV_bool) ``` hoelzl@42989 ` 964` ``` also have "\ = (\i\UNIV. prob (bool_case A B i -` bool_case Xa Xb i \ space M))" ``` hoelzl@42989 ` 965` ``` using indep unfolding indep_var_def ``` hoelzl@42989 ` 966` ``` by (rule indep_varsD) (auto split: bool.split intro: sets) ``` hoelzl@42989 ` 967` ``` also have "\ = prob (A -` Xa \ space M) * prob (B -` Xb \ space M)" ``` hoelzl@42989 ` 968` ``` unfolding UNIV_bool by simp ``` hoelzl@42989 ` 969` ``` finally show ?thesis . ``` hoelzl@42989 ` 970` ```qed ``` hoelzl@42989 ` 971` hoelzl@43340 ` 972` ```lemma (in prob_space) ``` hoelzl@43340 ` 973` ``` assumes "indep_var S X T Y" ``` hoelzl@43340 ` 974` ``` shows indep_var_rv1: "random_variable S X" ``` hoelzl@43340 ` 975` ``` and indep_var_rv2: "random_variable T Y" ``` hoelzl@43340 ` 976` ```proof - ``` hoelzl@43340 ` 977` ``` have "\i\UNIV. random_variable (bool_case S T i) (bool_case X Y i)" ``` hoelzl@43340 ` 978` ``` using assms unfolding indep_var_def indep_vars_def by auto ``` hoelzl@43340 ` 979` ``` then show "random_variable S X" "random_variable T Y" ``` hoelzl@43340 ` 980` ``` unfolding UNIV_bool by auto ``` hoelzl@43340 ` 981` ```qed ``` hoelzl@43340 ` 982` hoelzl@47694 ` 983` ```lemma measurable_bool_case[simp, intro]: ``` hoelzl@47694 ` 984` ``` "(\(x, y). bool_case x y) \ measurable (M \\<^isub>M N) (Pi\<^isub>M UNIV (bool_case M N))" ``` hoelzl@47694 ` 985` ``` (is "?f \ measurable ?B ?P") ``` hoelzl@47694 ` 986` ```proof (rule measurable_PiM_single) ``` hoelzl@47694 ` 987` ``` show "?f \ space ?B \ (\\<^isub>E i\UNIV. space (bool_case M N i))" ``` hoelzl@47694 ` 988` ``` by (auto simp: space_pair_measure extensional_def split: bool.split) ``` hoelzl@47694 ` 989` ``` fix i A assume "A \ sets (case i of True \ M | False \ N)" ``` hoelzl@47694 ` 990` ``` moreover then have "{\ \ space (M \\<^isub>M N). prod_case bool_case \ i \ A} ``` hoelzl@47694 ` 991` ``` = (case i of True \ A \ space N | False \ space M \ A)" ``` hoelzl@47694 ` 992` ``` by (auto simp: space_pair_measure split: bool.split dest!: sets_into_space) ``` hoelzl@47694 ` 993` ``` ultimately show "{\ \ space (M \\<^isub>M N). prod_case bool_case \ i \ A} \ sets ?B" ``` hoelzl@47694 ` 994` ``` by (auto split: bool.split) ``` hoelzl@47694 ` 995` ```qed ``` hoelzl@47694 ` 996` hoelzl@47694 ` 997` ```lemma borel_measurable_indicator': ``` hoelzl@47694 ` 998` ``` "A \ sets N \ f \ measurable M N \ (\x. indicator A (f x)) \ borel_measurable M" ``` hoelzl@47694 ` 999` ``` using measurable_comp[OF _ borel_measurable_indicator, of f M N A] by (auto simp add: comp_def) ``` hoelzl@47694 ` 1000` hoelzl@47694 ` 1001` ```lemma (in product_sigma_finite) distr_component: ``` hoelzl@47694 ` 1002` ``` "distr (M i) (Pi\<^isub>M {i} M) (\x. \i\{i}. x) = Pi\<^isub>M {i} M" (is "?D = ?P") ``` hoelzl@47694 ` 1003` ```proof (intro measure_eqI[symmetric]) ``` hoelzl@47694 ` 1004` ``` interpret I: finite_product_sigma_finite M "{i}" by default simp ``` hoelzl@47694 ` 1005` hoelzl@47694 ` 1006` ``` have eq: "\x. x \ extensional {i} \ (\j\{i}. x i) = x" ``` hoelzl@47694 ` 1007` ``` by (auto simp: extensional_def restrict_def) ``` hoelzl@47694 ` 1008` hoelzl@47694 ` 1009` ``` fix A assume A: "A \ sets ?P" ``` hoelzl@47694 ` 1010` ``` then have "emeasure ?P A = (\\<^isup>+x. indicator A x \?P)" ``` hoelzl@47694 ` 1011` ``` by simp ``` hoelzl@47694 ` 1012` ``` also have "\ = (\\<^isup>+x. indicator ((\x. \i\{i}. x) -` A \ space (M i)) x \M i)" ``` hoelzl@47694 ` 1013` ``` apply (subst product_positive_integral_singleton[symmetric]) ``` hoelzl@47694 ` 1014` ``` apply (force intro!: measurable_restrict measurable_sets A) ``` hoelzl@47694 ` 1015` ``` apply (auto intro!: positive_integral_cong simp: space_PiM indicator_def simp: eq) ``` hoelzl@47694 ` 1016` ``` done ``` hoelzl@47694 ` 1017` ``` also have "\ = emeasure (M i) ((\x. \i\{i}. x) -` A \ space (M i))" ``` hoelzl@47694 ` 1018` ``` by (force intro!: measurable_restrict measurable_sets A positive_integral_indicator) ``` hoelzl@47694 ` 1019` ``` also have "\ = emeasure ?D A" ``` hoelzl@47694 ` 1020` ``` using A by (auto intro!: emeasure_distr[symmetric] measurable_restrict) ``` hoelzl@47694 ` 1021` ``` finally show "emeasure (Pi\<^isub>M {i} M) A = emeasure ?D A" . ``` hoelzl@47694 ` 1022` ```qed simp ``` hoelzl@43340 ` 1023` hoelzl@47694 ` 1024` ```lemma pair_measure_eqI: ``` hoelzl@47694 ` 1025` ``` assumes "sigma_finite_measure M1" "sigma_finite_measure M2" ``` hoelzl@47694 ` 1026` ``` assumes sets: "sets (M1 \\<^isub>M M2) = sets M" ``` hoelzl@47694 ` 1027` ``` assumes emeasure: "\A B. A \ sets M1 \ B \ sets M2 \ emeasure M1 A * emeasure M2 B = emeasure M (A \ B)" ``` hoelzl@47694 ` 1028` ``` shows "M1 \\<^isub>M M2 = M" ``` hoelzl@47694 ` 1029` ```proof - ``` hoelzl@47694 ` 1030` ``` interpret M1: sigma_finite_measure M1 by fact ``` hoelzl@47694 ` 1031` ``` interpret M2: sigma_finite_measure M2 by fact ``` hoelzl@47694 ` 1032` ``` interpret pair_sigma_finite M1 M2 by default ``` hoelzl@47694 ` 1033` ``` from sigma_finite_up_in_pair_measure_generator guess F :: "nat \ ('a \ 'b) set" .. note F = this ``` hoelzl@47694 ` 1034` ``` let ?E = "{a \ b |a b. a \ sets M1 \ b \ sets M2}" ``` hoelzl@47694 ` 1035` ``` let ?P = "M1 \\<^isub>M M2" ``` hoelzl@47694 ` 1036` ``` show ?thesis ``` hoelzl@47694 ` 1037` ``` proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of M1 M2]]) ``` hoelzl@47694 ` 1038` ``` show "?E \ Pow (space ?P)" ``` hoelzl@47694 ` 1039` ``` using space_closed[of M1] space_closed[of M2] by (auto simp: space_pair_measure) ``` hoelzl@47694 ` 1040` ``` show "sets ?P = sigma_sets (space ?P) ?E" ``` hoelzl@47694 ` 1041` ``` by (simp add: sets_pair_measure space_pair_measure) ``` hoelzl@47694 ` 1042` ``` then show "sets M = sigma_sets (space ?P) ?E" ``` hoelzl@47694 ` 1043` ``` using sets[symmetric] by simp ``` hoelzl@47694 ` 1044` ``` next ``` hoelzl@47694 ` 1045` ``` show "range F \ ?E" "incseq F" "(\i. F i) = space ?P" "\i. emeasure ?P (F i) \ \" ``` hoelzl@47694 ` 1046` ``` using F by (auto simp: space_pair_measure) ``` hoelzl@47694 ` 1047` ``` next ``` hoelzl@47694 ` 1048` ``` fix X assume "X \ ?E" ``` hoelzl@47694 ` 1049` ``` then obtain A B where X[simp]: "X = A \ B" and A: "A \ sets M1" and B: "B \ sets M2" by auto ``` hoelzl@47694 ` 1050` ``` then have "emeasure ?P X = emeasure M1 A * emeasure M2 B" ``` hoelzl@49776 ` 1051` ``` by (simp add: M2.emeasure_pair_measure_Times) ``` hoelzl@47694 ` 1052` ``` also have "\ = emeasure M (A \ B)" ``` hoelzl@47694 ` 1053` ``` using A B emeasure by auto ``` hoelzl@47694 ` 1054` ``` finally show "emeasure ?P X = emeasure M X" ``` hoelzl@47694 ` 1055` ``` by simp ``` hoelzl@47694 ` 1056` ``` qed ``` hoelzl@47694 ` 1057` ```qed ``` hoelzl@43340 ` 1058` hoelzl@47694 ` 1059` ```lemma pair_measure_eq_distr_PiM: ``` hoelzl@47694 ` 1060` ``` fixes M1 :: "'a measure" and M2 :: "'a measure" ``` hoelzl@47694 ` 1061` ``` assumes "sigma_finite_measure M1" "sigma_finite_measure M2" ``` hoelzl@47694 ` 1062` ``` shows "(M1 \\<^isub>M M2) = distr (Pi\<^isub>M UNIV (bool_case M1 M2)) (M1 \\<^isub>M M2) (\x. (x True, x False))" ``` hoelzl@47694 ` 1063` ``` (is "?P = ?D") ``` hoelzl@47694 ` 1064` ```proof (rule pair_measure_eqI[OF assms]) ``` hoelzl@47694 ` 1065` ``` interpret B: product_sigma_finite "bool_case M1 M2" ``` hoelzl@47694 ` 1066` ``` unfolding product_sigma_finite_def using assms by (auto split: bool.split) ``` hoelzl@47694 ` 1067` ``` let ?B = "Pi\<^isub>M UNIV (bool_case M1 M2)" ``` hoelzl@43340 ` 1068` hoelzl@47694 ` 1069` ``` have [simp]: "fst \ (\x. (x True, x False)) = (\x. x True)" "snd \ (\x. (x True, x False)) = (\x. x False)" ``` hoelzl@47694 ` 1070` ``` by auto ``` hoelzl@47694 ` 1071` ``` fix A B assume A: "A \ sets M1" and B: "B \ sets M2" ``` hoelzl@47694 ` 1072` ``` have "emeasure M1 A * emeasure M2 B = (\ i\UNIV. emeasure (bool_case M1 M2 i) (bool_case A B i))" ``` hoelzl@47694 ` 1073` ``` by (simp add: UNIV_bool ac_simps) ``` hoelzl@47694 ` 1074` ``` also have "\ = emeasure ?B (Pi\<^isub>E UNIV (bool_case A B))" ``` hoelzl@47694 ` 1075` ``` using A B by (subst B.emeasure_PiM) (auto split: bool.split) ``` hoelzl@47694 ` 1076` ``` also have "Pi\<^isub>E UNIV (bool_case A B) = (\x. (x True, x False)) -` (A \ B) \ space ?B" ``` hoelzl@47694 ` 1077` ``` using A[THEN sets_into_space] B[THEN sets_into_space] ``` hoelzl@47694 ` 1078` ``` by (auto simp: Pi_iff all_bool_eq space_PiM split: bool.split) ``` hoelzl@47694 ` 1079` ``` finally show "emeasure M1 A * emeasure M2 B = emeasure ?D (A \ B)" ``` hoelzl@47694 ` 1080` ``` using A B ``` hoelzl@47694 ` 1081` ``` measurable_component_singleton[of True UNIV "bool_case M1 M2"] ``` hoelzl@47694 ` 1082` ``` measurable_component_singleton[of False UNIV "bool_case M1 M2"] ``` hoelzl@47694 ` 1083` ``` by (subst emeasure_distr) (auto simp: measurable_pair_iff) ``` hoelzl@47694 ` 1084` ```qed simp ``` hoelzl@43340 ` 1085` hoelzl@47694 ` 1086` ```lemma measurable_Pair: ``` hoelzl@47694 ` 1087` ``` assumes rvs: "X \ measurable M S" "Y \ measurable M T" ``` hoelzl@47694 ` 1088` ``` shows "(\x. (X x, Y x)) \ measurable M (S \\<^isub>M T)" ``` hoelzl@47694 ` 1089` ```proof - ``` hoelzl@47694 ` 1090` ``` have [simp]: "fst \ (\x. (X x, Y x)) = (\x. X x)" "snd \ (\x. (X x, Y x)) = (\x. Y x)" ``` hoelzl@47694 ` 1091` ``` by auto ``` hoelzl@47694 ` 1092` ``` show " (\x. (X x, Y x)) \ measurable M (S \\<^isub>M T)" ``` hoelzl@47694 ` 1093` ``` by (auto simp: measurable_pair_iff rvs) ``` hoelzl@47694 ` 1094` ```qed ``` hoelzl@47694 ` 1095` hoelzl@47694 ` 1096` ```lemma (in prob_space) indep_var_distribution_eq: ``` hoelzl@47694 ` 1097` ``` "indep_var S X T Y \ random_variable S X \ random_variable T Y \ ``` hoelzl@47694 ` 1098` ``` distr M S X \\<^isub>M distr M T Y = distr M (S \\<^isub>M T) (\x. (X x, Y x))" (is "_ \ _ \ _ \ ?S \\<^isub>M ?T = ?J") ``` hoelzl@47694 ` 1099` ```proof safe ``` hoelzl@47694 ` 1100` ``` assume "indep_var S X T Y" ``` hoelzl@47694 ` 1101` ``` then show rvs: "random_variable S X" "random_variable T Y" ``` hoelzl@47694 ` 1102` ``` by (blast dest: indep_var_rv1 indep_var_rv2)+ ``` hoelzl@47694 ` 1103` ``` then have XY: "random_variable (S \\<^isub>M T) (\x. (X x, Y x))" ``` hoelzl@47694 ` 1104` ``` by (rule measurable_Pair) ``` hoelzl@47694 ` 1105` hoelzl@47694 ` 1106` ``` interpret X: prob_space ?S by (rule prob_space_distr) fact ``` hoelzl@47694 ` 1107` ``` interpret Y: prob_space ?T by (rule prob_space_distr) fact ``` hoelzl@47694 ` 1108` ``` interpret XY: pair_prob_space ?S ?T .. ``` hoelzl@47694 ` 1109` ``` show "?S \\<^isub>M ?T = ?J" ``` hoelzl@47694 ` 1110` ``` proof (rule pair_measure_eqI) ``` hoelzl@47694 ` 1111` ``` show "sigma_finite_measure ?S" .. ``` hoelzl@47694 ` 1112` ``` show "sigma_finite_measure ?T" .. ``` hoelzl@43340 ` 1113` hoelzl@47694 ` 1114` ``` fix A B assume A: "A \ sets ?S" and B: "B \ sets ?T" ``` hoelzl@47694 ` 1115` ``` have "emeasure ?J (A \ B) = emeasure M ((\x. (X x, Y x)) -` (A \ B) \ space M)" ``` hoelzl@47694 ` 1116` ``` using A B by (intro emeasure_distr[OF XY]) auto ``` hoelzl@47694 ` 1117` ``` also have "\ = emeasure M (X -` A \ space M) * emeasure M (Y -` B \ space M)" ``` hoelzl@47694 ` 1118` ``` using indep_varD[OF `indep_var S X T Y`, of A B] A B by (simp add: emeasure_eq_measure) ``` hoelzl@47694 ` 1119` ``` also have "\ = emeasure ?S A * emeasure ?T B" ``` hoelzl@47694 ` 1120` ``` using rvs A B by (simp add: emeasure_distr) ``` hoelzl@47694 ` 1121` ``` finally show "emeasure ?S A * emeasure ?T B = emeasure ?J (A \ B)" by simp ``` hoelzl@47694 ` 1122` ``` qed simp ``` hoelzl@47694 ` 1123` ```next ``` hoelzl@47694 ` 1124` ``` assume rvs: "random_variable S X" "random_variable T Y" ``` hoelzl@47694 ` 1125` ``` then have XY: "random_variable (S \\<^isub>M T) (\x. (X x, Y x))" ``` hoelzl@47694 ` 1126` ``` by (rule measurable_Pair) ``` hoelzl@43340 ` 1127` hoelzl@47694 ` 1128` ``` let ?S = "distr M S X" and ?T = "distr M T Y" ``` hoelzl@47694 ` 1129` ``` interpret X: prob_space ?S by (rule prob_space_distr) fact ``` hoelzl@47694 ` 1130` ``` interpret Y: prob_space ?T by (rule prob_space_distr) fact ``` hoelzl@47694 ` 1131` ``` interpret XY: pair_prob_space ?S ?T .. ``` hoelzl@47694 ` 1132` hoelzl@47694 ` 1133` ``` assume "?S \\<^isub>M ?T = ?J" ``` hoelzl@43340 ` 1134` hoelzl@47694 ` 1135` ``` { fix S and X ``` hoelzl@47694 ` 1136` ``` have "Int_stable {X -` A \ space M |A. A \ sets S}" ``` hoelzl@47694 ` 1137` ``` proof (safe intro!: Int_stableI) ``` hoelzl@47694 ` 1138` ``` fix A B assume "A \ sets S" "B \ sets S" ``` hoelzl@47694 ` 1139` ``` then show "\C. (X -` A \ space M) \ (X -` B \ space M) = (X -` C \ space M) \ C \ sets S" ``` hoelzl@47694 ` 1140` ``` by (intro exI[of _ "A \ B"]) auto ``` hoelzl@47694 ` 1141` ``` qed } ``` hoelzl@47694 ` 1142` ``` note Int_stable = this ``` hoelzl@47694 ` 1143` hoelzl@47694 ` 1144` ``` show "indep_var S X T Y" unfolding indep_var_eq ``` hoelzl@47694 ` 1145` ``` proof (intro conjI indep_set_sigma_sets Int_stable rvs) ``` hoelzl@47694 ` 1146` ``` show "indep_set {X -` A \ space M |A. A \ sets S} {Y -` A \ space M |A. A \ sets T}" ``` hoelzl@47694 ` 1147` ``` proof (safe intro!: indep_setI) ``` hoelzl@47694 ` 1148` ``` { fix A assume "A \ sets S" then show "X -` A \ space M \ sets M" ``` hoelzl@47694 ` 1149` ``` using `X \ measurable M S` by (auto intro: measurable_sets) } ``` hoelzl@47694 ` 1150` ``` { fix A assume "A \ sets T" then show "Y -` A \ space M \ sets M" ``` hoelzl@47694 ` 1151` ``` using `Y \ measurable M T` by (auto intro: measurable_sets) } ``` hoelzl@47694 ` 1152` ``` next ``` hoelzl@47694 ` 1153` ``` fix A B assume ab: "A \ sets S" "B \ sets T" ``` hoelzl@47694 ` 1154` ``` then have "ereal (prob ((X -` A \ space M) \ (Y -` B \ space M))) = emeasure ?J (A \ B)" ``` hoelzl@47694 ` 1155` ``` using XY by (auto simp add: emeasure_distr emeasure_eq_measure intro!: arg_cong[where f="prob"]) ``` hoelzl@47694 ` 1156` ``` also have "\ = emeasure (?S \\<^isub>M ?T) (A \ B)" ``` hoelzl@47694 ` 1157` ``` unfolding `?S \\<^isub>M ?T = ?J` .. ``` hoelzl@47694 ` 1158` ``` also have "\ = emeasure ?S A * emeasure ?T B" ``` hoelzl@49776 ` 1159` ``` using ab by (simp add: Y.emeasure_pair_measure_Times) ``` hoelzl@47694 ` 1160` ``` finally show "prob ((X -` A \ space M) \ (Y -` B \ space M)) = ``` hoelzl@47694 ` 1161` ``` prob (X -` A \ space M) * prob (Y -` B \ space M)" ``` hoelzl@47694 ` 1162` ``` using rvs ab by (simp add: emeasure_eq_measure emeasure_distr) ``` hoelzl@47694 ` 1163` ``` qed ``` hoelzl@43340 ` 1164` ``` qed ``` hoelzl@43340 ` 1165` ```qed ``` hoelzl@42989 ` 1166` hoelzl@42861 ` 1167` ```end ```