src/HOL/Probability/Independent_Family.thy
 author huffman Sun Apr 01 16:09:58 2012 +0200 (2012-04-01) changeset 47255 30a1692557b0 parent 46731 5302e932d1e5 child 47694 05663f75964c permissions -rw-r--r--
removed Nat_Numeral.thy, moving all theorems elsewhere
 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@42861 ` 8` ``` imports Probability_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@42987 ` 47` ```lemma (in prob_space) indep_sets_cong[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@42861 ` 89` ```lemma (in prob_space) indep_setsI: ``` hoelzl@42861 ` 90` ``` assumes "\i. i \ I \ F i \ events" ``` hoelzl@42861 ` 91` ``` 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 ` 92` ``` shows "indep_sets F I" ``` hoelzl@42861 ` 93` ``` using assms unfolding indep_sets_def by (auto simp: Pi_iff) ``` hoelzl@42861 ` 94` hoelzl@42861 ` 95` ```lemma (in prob_space) indep_setsD: ``` hoelzl@42861 ` 96` ``` assumes "indep_sets F I" and "J \ I" "J \ {}" "finite J" "\j\J. A j \ F j" ``` hoelzl@42861 ` 97` ``` shows "prob (\j\J. A j) = (\j\J. prob (A j))" ``` hoelzl@42861 ` 98` ``` using assms unfolding indep_sets_def by auto ``` hoelzl@42861 ` 99` hoelzl@42982 ` 100` ```lemma (in prob_space) indep_setI: ``` hoelzl@42982 ` 101` ``` assumes ev: "A \ events" "B \ events" ``` hoelzl@42982 ` 102` ``` and indep: "\a b. a \ A \ b \ B \ prob (a \ b) = prob a * prob b" ``` hoelzl@42982 ` 103` ``` shows "indep_set A B" ``` hoelzl@42982 ` 104` ``` unfolding indep_set_def ``` hoelzl@42982 ` 105` ```proof (rule indep_setsI) ``` hoelzl@42982 ` 106` ``` fix F J assume "J \ {}" "J \ UNIV" ``` hoelzl@42982 ` 107` ``` and F: "\j\J. F j \ (case j of True \ A | False \ B)" ``` hoelzl@42982 ` 108` ``` have "J \ Pow UNIV" by auto ``` hoelzl@42982 ` 109` ``` with F `J \ {}` indep[of "F True" "F False"] ``` hoelzl@42982 ` 110` ``` show "prob (\j\J. F j) = (\j\J. prob (F j))" ``` hoelzl@42982 ` 111` ``` unfolding UNIV_bool Pow_insert by (auto simp: ac_simps) ``` hoelzl@42982 ` 112` ```qed (auto split: bool.split simp: ev) ``` hoelzl@42982 ` 113` hoelzl@42982 ` 114` ```lemma (in prob_space) indep_setD: ``` hoelzl@42982 ` 115` ``` assumes indep: "indep_set A B" and ev: "a \ A" "b \ B" ``` hoelzl@42982 ` 116` ``` shows "prob (a \ b) = prob a * prob b" ``` hoelzl@42982 ` 117` ``` using indep[unfolded indep_set_def, THEN indep_setsD, of UNIV "bool_case a b"] ev ``` hoelzl@42982 ` 118` ``` by (simp add: ac_simps UNIV_bool) ``` hoelzl@42982 ` 119` hoelzl@43340 ` 120` ```lemma (in prob_space) indep_var_eq: ``` hoelzl@43340 ` 121` ``` "indep_var S X T Y \ ``` hoelzl@43340 ` 122` ``` (random_variable S X \ random_variable T Y) \ ``` hoelzl@43340 ` 123` ``` indep_set ``` hoelzl@43340 ` 124` ``` (sigma_sets (space M) { X -` A \ space M | A. A \ sets S}) ``` hoelzl@43340 ` 125` ``` (sigma_sets (space M) { Y -` A \ space M | A. A \ sets T})" ``` hoelzl@43340 ` 126` ``` unfolding indep_var_def indep_vars_def indep_set_def UNIV_bool ``` hoelzl@43340 ` 127` ``` by (intro arg_cong2[where f="op \"] arg_cong2[where f=indep_sets] ext) ``` hoelzl@43340 ` 128` ``` (auto split: bool.split) ``` hoelzl@43340 ` 129` hoelzl@42982 ` 130` ```lemma (in prob_space) ``` hoelzl@42982 ` 131` ``` assumes indep: "indep_set A B" ``` hoelzl@42983 ` 132` ``` shows indep_setD_ev1: "A \ events" ``` hoelzl@42983 ` 133` ``` and indep_setD_ev2: "B \ events" ``` hoelzl@42982 ` 134` ``` using indep unfolding indep_set_def indep_sets_def UNIV_bool by auto ``` hoelzl@42982 ` 135` hoelzl@42861 ` 136` ```lemma (in prob_space) indep_sets_dynkin: ``` hoelzl@42861 ` 137` ``` assumes indep: "indep_sets F I" ``` hoelzl@42861 ` 138` ``` shows "indep_sets (\i. sets (dynkin \ space = space M, sets = F i \)) I" ``` hoelzl@42861 ` 139` ``` (is "indep_sets ?F I") ``` hoelzl@42861 ` 140` ```proof (subst indep_sets_finite_index_sets, intro allI impI ballI) ``` hoelzl@42861 ` 141` ``` fix J assume "finite J" "J \ I" "J \ {}" ``` hoelzl@42861 ` 142` ``` with indep have "indep_sets F J" ``` hoelzl@42861 ` 143` ``` by (subst (asm) indep_sets_finite_index_sets) auto ``` hoelzl@42861 ` 144` ``` { fix J K assume "indep_sets F K" ``` wenzelm@46731 ` 145` ``` let ?G = "\S i. if i \ S then ?F i else F i" ``` hoelzl@42861 ` 146` ``` assume "finite J" "J \ K" ``` hoelzl@42861 ` 147` ``` then have "indep_sets (?G J) K" ``` hoelzl@42861 ` 148` ``` proof induct ``` hoelzl@42861 ` 149` ``` case (insert j J) ``` hoelzl@42861 ` 150` ``` moreover def G \ "?G J" ``` hoelzl@42861 ` 151` ``` ultimately have G: "indep_sets G K" "\i. i \ K \ G i \ events" and "j \ K" ``` hoelzl@42861 ` 152` ``` by (auto simp: indep_sets_def) ``` hoelzl@42861 ` 153` ``` let ?D = "{E\events. indep_sets (G(j := {E})) K }" ``` hoelzl@42861 ` 154` ``` { fix X assume X: "X \ events" ``` hoelzl@42861 ` 155` ``` assume indep: "\J A. J \ {} \ J \ K \ finite J \ j \ J \ (\i\J. A i \ G i) ``` hoelzl@42861 ` 156` ``` \ prob ((\i\J. A i) \ X) = prob X * (\i\J. prob (A i))" ``` hoelzl@42861 ` 157` ``` have "indep_sets (G(j := {X})) K" ``` hoelzl@42861 ` 158` ``` proof (rule indep_setsI) ``` hoelzl@42861 ` 159` ``` fix i assume "i \ K" then show "(G(j:={X})) i \ events" ``` hoelzl@42861 ` 160` ``` using G X by auto ``` hoelzl@42861 ` 161` ``` next ``` hoelzl@42861 ` 162` ``` fix A J assume J: "J \ {}" "J \ K" "finite J" "\i\J. A i \ (G(j := {X})) i" ``` hoelzl@42861 ` 163` ``` show "prob (\j\J. A j) = (\j\J. prob (A j))" ``` hoelzl@42861 ` 164` ``` proof cases ``` hoelzl@42861 ` 165` ``` assume "j \ J" ``` hoelzl@42861 ` 166` ``` with J have "A j = X" by auto ``` hoelzl@42861 ` 167` ``` show ?thesis ``` hoelzl@42861 ` 168` ``` proof cases ``` hoelzl@42861 ` 169` ``` assume "J = {j}" then show ?thesis by simp ``` hoelzl@42861 ` 170` ``` next ``` hoelzl@42861 ` 171` ``` assume "J \ {j}" ``` hoelzl@42861 ` 172` ``` have "prob (\i\J. A i) = prob ((\i\J-{j}. A i) \ X)" ``` hoelzl@42861 ` 173` ``` using `j \ J` `A j = X` by (auto intro!: arg_cong[where f=prob] split: split_if_asm) ``` hoelzl@42861 ` 174` ``` also have "\ = prob X * (\i\J-{j}. prob (A i))" ``` hoelzl@42861 ` 175` ``` proof (rule indep) ``` hoelzl@42861 ` 176` ``` show "J - {j} \ {}" "J - {j} \ K" "finite (J - {j})" "j \ J - {j}" ``` hoelzl@42861 ` 177` ``` using J `J \ {j}` `j \ J` by auto ``` hoelzl@42861 ` 178` ``` show "\i\J - {j}. A i \ G i" ``` hoelzl@42861 ` 179` ``` using J by auto ``` hoelzl@42861 ` 180` ``` qed ``` hoelzl@42861 ` 181` ``` also have "\ = prob (A j) * (\i\J-{j}. prob (A i))" ``` hoelzl@42861 ` 182` ``` using `A j = X` by simp ``` hoelzl@42861 ` 183` ``` also have "\ = (\i\J. prob (A i))" ``` hoelzl@42861 ` 184` ``` unfolding setprod.insert_remove[OF `finite J`, symmetric, of "\i. prob (A i)"] ``` hoelzl@42861 ` 185` ``` using `j \ J` by (simp add: insert_absorb) ``` hoelzl@42861 ` 186` ``` finally show ?thesis . ``` hoelzl@42861 ` 187` ``` qed ``` hoelzl@42861 ` 188` ``` next ``` hoelzl@42861 ` 189` ``` assume "j \ J" ``` hoelzl@42861 ` 190` ``` with J have "\i\J. A i \ G i" by (auto split: split_if_asm) ``` hoelzl@42861 ` 191` ``` with J show ?thesis ``` hoelzl@42861 ` 192` ``` by (intro indep_setsD[OF G(1)]) auto ``` hoelzl@42861 ` 193` ``` qed ``` hoelzl@42861 ` 194` ``` qed } ``` hoelzl@42861 ` 195` ``` note indep_sets_insert = this ``` hoelzl@42861 ` 196` ``` have "dynkin_system \ space = space M, sets = ?D \" ``` hoelzl@42987 ` 197` ``` proof (rule dynkin_systemI', simp_all cong del: indep_sets_cong, safe) ``` hoelzl@42861 ` 198` ``` show "indep_sets (G(j := {{}})) K" ``` hoelzl@42861 ` 199` ``` by (rule indep_sets_insert) auto ``` hoelzl@42861 ` 200` ``` next ``` hoelzl@42861 ` 201` ``` fix X assume X: "X \ events" and G': "indep_sets (G(j := {X})) K" ``` hoelzl@42861 ` 202` ``` show "indep_sets (G(j := {space M - X})) K" ``` hoelzl@42861 ` 203` ``` proof (rule indep_sets_insert) ``` hoelzl@42861 ` 204` ``` fix J A assume J: "J \ {}" "J \ K" "finite J" "j \ J" and A: "\i\J. A i \ G i" ``` hoelzl@42861 ` 205` ``` then have A_sets: "\i. i\J \ A i \ events" ``` hoelzl@42861 ` 206` ``` using G by auto ``` hoelzl@42861 ` 207` ``` have "prob ((\j\J. A j) \ (space M - X)) = ``` hoelzl@42861 ` 208` ``` prob ((\j\J. A j) - (\i\insert j J. (A(j := X)) i))" ``` hoelzl@42861 ` 209` ``` using A_sets sets_into_space X `J \ {}` ``` hoelzl@42861 ` 210` ``` by (auto intro!: arg_cong[where f=prob] split: split_if_asm) ``` hoelzl@42861 ` 211` ``` also have "\ = prob (\j\J. A j) - prob (\i\insert j J. (A(j := X)) i)" ``` hoelzl@42861 ` 212` ``` using J `J \ {}` `j \ J` A_sets X sets_into_space ``` hoelzl@42861 ` 213` ``` by (auto intro!: finite_measure_Diff finite_INT split: split_if_asm) ``` hoelzl@42861 ` 214` ``` finally have "prob ((\j\J. A j) \ (space M - X)) = ``` hoelzl@42861 ` 215` ``` prob (\j\J. A j) - prob (\i\insert j J. (A(j := X)) i)" . ``` hoelzl@42861 ` 216` ``` moreover { ``` hoelzl@42861 ` 217` ``` have "prob (\j\J. A j) = (\j\J. prob (A j))" ``` hoelzl@42861 ` 218` ``` using J A `finite J` by (intro indep_setsD[OF G(1)]) auto ``` hoelzl@42861 ` 219` ``` then have "prob (\j\J. A j) = prob (space M) * (\i\J. prob (A i))" ``` hoelzl@42861 ` 220` ``` using prob_space by simp } ``` hoelzl@42861 ` 221` ``` moreover { ``` hoelzl@42861 ` 222` ``` have "prob (\i\insert j J. (A(j := X)) i) = (\i\insert j J. prob ((A(j := X)) i))" ``` hoelzl@42861 ` 223` ``` using J A `j \ K` by (intro indep_setsD[OF G']) auto ``` hoelzl@42861 ` 224` ``` then have "prob (\i\insert j J. (A(j := X)) i) = prob X * (\i\J. prob (A i))" ``` hoelzl@42861 ` 225` ``` using `finite J` `j \ J` by (auto intro!: setprod_cong) } ``` hoelzl@42861 ` 226` ``` ultimately have "prob ((\j\J. A j) \ (space M - X)) = (prob (space M) - prob X) * (\i\J. prob (A i))" ``` hoelzl@42861 ` 227` ``` by (simp add: field_simps) ``` hoelzl@42861 ` 228` ``` also have "\ = prob (space M - X) * (\i\J. prob (A i))" ``` hoelzl@42861 ` 229` ``` using X A by (simp add: finite_measure_compl) ``` hoelzl@42861 ` 230` ``` finally show "prob ((\j\J. A j) \ (space M - X)) = prob (space M - X) * (\i\J. prob (A i))" . ``` hoelzl@42861 ` 231` ``` qed (insert X, auto) ``` hoelzl@42861 ` 232` ``` next ``` hoelzl@42861 ` 233` ``` fix F :: "nat \ 'a set" assume disj: "disjoint_family F" and "range F \ ?D" ``` hoelzl@42861 ` 234` ``` then have F: "\i. F i \ events" "\i. indep_sets (G(j:={F i})) K" by auto ``` hoelzl@42861 ` 235` ``` show "indep_sets (G(j := {\k. F k})) K" ``` hoelzl@42861 ` 236` ``` proof (rule indep_sets_insert) ``` hoelzl@42861 ` 237` ``` fix J A assume J: "j \ J" "J \ {}" "J \ K" "finite J" and A: "\i\J. A i \ G i" ``` hoelzl@42861 ` 238` ``` then have A_sets: "\i. i\J \ A i \ events" ``` hoelzl@42861 ` 239` ``` using G by auto ``` hoelzl@42861 ` 240` ``` have "prob ((\j\J. A j) \ (\k. F k)) = prob (\k. (\i\insert j J. (A(j := F k)) i))" ``` hoelzl@42861 ` 241` ``` using `J \ {}` `j \ J` `j \ K` by (auto intro!: arg_cong[where f=prob] split: split_if_asm) ``` hoelzl@42861 ` 242` ``` 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 ` 243` ``` proof (rule finite_measure_UNION) ``` hoelzl@42861 ` 244` ``` show "disjoint_family (\k. \i\insert j J. (A(j := F k)) i)" ``` hoelzl@42861 ` 245` ``` using disj by (rule disjoint_family_on_bisimulation) auto ``` hoelzl@42861 ` 246` ``` show "range (\k. \i\insert j J. (A(j := F k)) i) \ events" ``` hoelzl@42861 ` 247` ``` using A_sets F `finite J` `J \ {}` `j \ J` by (auto intro!: Int) ``` hoelzl@42861 ` 248` ``` qed ``` hoelzl@42861 ` 249` ``` moreover { fix k ``` hoelzl@42861 ` 250` ``` 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 ` 251` ``` by (subst indep_setsD[OF F(2)]) (auto intro!: setprod_cong split: split_if_asm) ``` hoelzl@42861 ` 252` ``` also have "\ = prob (F k) * prob (\i\J. A i)" ``` hoelzl@42861 ` 253` ``` using J A `j \ K` by (subst indep_setsD[OF G(1)]) auto ``` hoelzl@42861 ` 254` ``` finally have "prob (\i\insert j J. (A(j := F k)) i) = prob (F k) * prob (\i\J. A i)" . } ``` hoelzl@42861 ` 255` ``` ultimately have "(\k. prob (F k) * prob (\i\J. A i)) sums (prob ((\j\J. A j) \ (\k. F k)))" ``` hoelzl@42861 ` 256` ``` by simp ``` hoelzl@42861 ` 257` ``` moreover ``` hoelzl@42861 ` 258` ``` have "(\k. prob (F k) * prob (\i\J. A i)) sums (prob (\k. F k) * prob (\i\J. A i))" ``` hoelzl@42861 ` 259` ``` using disj F(1) by (intro finite_measure_UNION sums_mult2) auto ``` hoelzl@42861 ` 260` ``` then have "(\k. prob (F k) * prob (\i\J. A i)) sums (prob (\k. F k) * (\i\J. prob (A i)))" ``` hoelzl@42861 ` 261` ``` using J A `j \ K` by (subst indep_setsD[OF G(1), symmetric]) auto ``` hoelzl@42861 ` 262` ``` ultimately ``` hoelzl@42861 ` 263` ``` show "prob ((\j\J. A j) \ (\k. F k)) = prob (\k. F k) * (\j\J. prob (A j))" ``` hoelzl@42861 ` 264` ``` by (auto dest!: sums_unique) ``` hoelzl@42861 ` 265` ``` qed (insert F, auto) ``` hoelzl@42861 ` 266` ``` qed (insert sets_into_space, auto) ``` hoelzl@42861 ` 267` ``` then have mono: "sets (dynkin \space = space M, sets = G j\) \ ``` hoelzl@42861 ` 268` ``` sets \space = space M, sets = {E \ events. indep_sets (G(j := {E})) K}\" ``` hoelzl@42987 ` 269` ``` proof (rule dynkin_system.dynkin_subset, simp_all cong del: indep_sets_cong, safe) ``` hoelzl@42861 ` 270` ``` fix X assume "X \ G j" ``` hoelzl@42861 ` 271` ``` then show "X \ events" using G `j \ K` by auto ``` hoelzl@42861 ` 272` ``` from `indep_sets G K` ``` hoelzl@42861 ` 273` ``` show "indep_sets (G(j := {X})) K" ``` hoelzl@42861 ` 274` ``` by (rule indep_sets_mono_sets) (insert `X \ G j`, auto) ``` hoelzl@42861 ` 275` ``` qed ``` hoelzl@42861 ` 276` ``` have "indep_sets (G(j:=?D)) K" ``` hoelzl@42861 ` 277` ``` proof (rule indep_setsI) ``` hoelzl@42861 ` 278` ``` fix i assume "i \ K" then show "(G(j := ?D)) i \ events" ``` hoelzl@42861 ` 279` ``` using G(2) by auto ``` hoelzl@42861 ` 280` ``` next ``` hoelzl@42861 ` 281` ``` fix A J assume J: "J\{}" "J \ K" "finite J" and A: "\i\J. A i \ (G(j := ?D)) i" ``` hoelzl@42861 ` 282` ``` show "prob (\j\J. A j) = (\j\J. prob (A j))" ``` hoelzl@42861 ` 283` ``` proof cases ``` hoelzl@42861 ` 284` ``` assume "j \ J" ``` hoelzl@42861 ` 285` ``` with A have indep: "indep_sets (G(j := {A j})) K" by auto ``` hoelzl@42861 ` 286` ``` from J A show ?thesis ``` hoelzl@42861 ` 287` ``` by (intro indep_setsD[OF indep]) auto ``` hoelzl@42861 ` 288` ``` next ``` hoelzl@42861 ` 289` ``` assume "j \ J" ``` hoelzl@42861 ` 290` ``` with J A have "\i\J. A i \ G i" by (auto split: split_if_asm) ``` hoelzl@42861 ` 291` ``` with J show ?thesis ``` hoelzl@42861 ` 292` ``` by (intro indep_setsD[OF G(1)]) auto ``` hoelzl@42861 ` 293` ``` qed ``` hoelzl@42861 ` 294` ``` qed ``` hoelzl@42861 ` 295` ``` then have "indep_sets (G(j:=sets (dynkin \space = space M, sets = G j\))) K" ``` hoelzl@42861 ` 296` ``` by (rule indep_sets_mono_sets) (insert mono, auto) ``` hoelzl@42861 ` 297` ``` then show ?case ``` hoelzl@42861 ` 298` ``` by (rule indep_sets_mono_sets) (insert `j \ K` `j \ J`, auto simp: G_def) ``` hoelzl@42861 ` 299` ``` qed (insert `indep_sets F K`, simp) } ``` hoelzl@42861 ` 300` ``` from this[OF `indep_sets F J` `finite J` subset_refl] ``` hoelzl@42861 ` 301` ``` show "indep_sets (\i. sets (dynkin \ space = space M, sets = F i \)) J" ``` hoelzl@42861 ` 302` ``` by (rule indep_sets_mono_sets) auto ``` hoelzl@42861 ` 303` ```qed ``` hoelzl@42861 ` 304` hoelzl@42861 ` 305` ```lemma (in prob_space) indep_sets_sigma: ``` hoelzl@42861 ` 306` ``` assumes indep: "indep_sets F I" ``` hoelzl@42861 ` 307` ``` assumes stable: "\i. i \ I \ Int_stable \ space = space M, sets = F i \" ``` hoelzl@42861 ` 308` ``` shows "indep_sets (\i. sets (sigma \ space = space M, sets = F i \)) I" ``` hoelzl@42861 ` 309` ```proof - ``` hoelzl@42861 ` 310` ``` from indep_sets_dynkin[OF indep] ``` hoelzl@42861 ` 311` ``` show ?thesis ``` hoelzl@42861 ` 312` ``` proof (rule indep_sets_mono_sets, subst sigma_eq_dynkin, simp_all add: stable) ``` hoelzl@42861 ` 313` ``` fix i assume "i \ I" ``` hoelzl@42861 ` 314` ``` with indep have "F i \ events" by (auto simp: indep_sets_def) ``` hoelzl@42861 ` 315` ``` with sets_into_space show "F i \ Pow (space M)" by auto ``` hoelzl@42861 ` 316` ``` qed ``` hoelzl@42861 ` 317` ```qed ``` hoelzl@42861 ` 318` hoelzl@42861 ` 319` ```lemma (in prob_space) indep_sets_sigma_sets: ``` hoelzl@42861 ` 320` ``` assumes "indep_sets F I" ``` hoelzl@42861 ` 321` ``` assumes "\i. i \ I \ Int_stable \ space = space M, sets = F i \" ``` hoelzl@42861 ` 322` ``` shows "indep_sets (\i. sigma_sets (space M) (F i)) I" ``` hoelzl@42861 ` 323` ``` using indep_sets_sigma[OF assms] by (simp add: sets_sigma) ``` hoelzl@42861 ` 324` hoelzl@42987 ` 325` ```lemma (in prob_space) indep_sets_sigma_sets_iff: ``` hoelzl@42987 ` 326` ``` assumes "\i. i \ I \ Int_stable \ space = space M, sets = F i \" ``` hoelzl@42987 ` 327` ``` shows "indep_sets (\i. sigma_sets (space M) (F i)) I \ indep_sets F I" ``` hoelzl@42987 ` 328` ```proof ``` hoelzl@42987 ` 329` ``` assume "indep_sets F I" then show "indep_sets (\i. sigma_sets (space M) (F i)) I" ``` hoelzl@42987 ` 330` ``` by (rule indep_sets_sigma_sets) fact ``` hoelzl@42987 ` 331` ```next ``` hoelzl@42987 ` 332` ``` assume "indep_sets (\i. sigma_sets (space M) (F i)) I" then show "indep_sets F I" ``` hoelzl@42987 ` 333` ``` by (rule indep_sets_mono_sets) (intro subsetI sigma_sets.Basic) ``` hoelzl@42987 ` 334` ```qed ``` hoelzl@42987 ` 335` hoelzl@42861 ` 336` ```lemma (in prob_space) indep_sets2_eq: ``` hoelzl@42981 ` 337` ``` "indep_set A B \ A \ events \ B \ events \ (\a\A. \b\B. prob (a \ b) = prob a * prob b)" ``` hoelzl@42981 ` 338` ``` unfolding indep_set_def ``` hoelzl@42861 ` 339` ```proof (intro iffI ballI conjI) ``` hoelzl@42861 ` 340` ``` assume indep: "indep_sets (bool_case A B) UNIV" ``` hoelzl@42861 ` 341` ``` { fix a b assume "a \ A" "b \ B" ``` hoelzl@42861 ` 342` ``` with indep_setsD[OF indep, of UNIV "bool_case a b"] ``` hoelzl@42861 ` 343` ``` show "prob (a \ b) = prob a * prob b" ``` hoelzl@42861 ` 344` ``` unfolding UNIV_bool by (simp add: ac_simps) } ``` hoelzl@42861 ` 345` ``` from indep show "A \ events" "B \ events" ``` hoelzl@42861 ` 346` ``` unfolding indep_sets_def UNIV_bool by auto ``` hoelzl@42861 ` 347` ```next ``` hoelzl@42861 ` 348` ``` assume *: "A \ events \ B \ events \ (\a\A. \b\B. prob (a \ b) = prob a * prob b)" ``` hoelzl@42861 ` 349` ``` show "indep_sets (bool_case A B) UNIV" ``` hoelzl@42861 ` 350` ``` proof (rule indep_setsI) ``` hoelzl@42861 ` 351` ``` fix i show "(case i of True \ A | False \ B) \ events" ``` hoelzl@42861 ` 352` ``` using * by (auto split: bool.split) ``` hoelzl@42861 ` 353` ``` next ``` hoelzl@42861 ` 354` ``` fix J X assume "J \ {}" "J \ UNIV" and X: "\j\J. X j \ (case j of True \ A | False \ B)" ``` hoelzl@42861 ` 355` ``` then have "J = {True} \ J = {False} \ J = {True,False}" ``` hoelzl@42861 ` 356` ``` by (auto simp: UNIV_bool) ``` hoelzl@42861 ` 357` ``` then show "prob (\j\J. X j) = (\j\J. prob (X j))" ``` hoelzl@42861 ` 358` ``` using X * by auto ``` hoelzl@42861 ` 359` ``` qed ``` hoelzl@42861 ` 360` ```qed ``` hoelzl@42861 ` 361` hoelzl@42981 ` 362` ```lemma (in prob_space) indep_set_sigma_sets: ``` hoelzl@42981 ` 363` ``` assumes "indep_set A B" ``` hoelzl@42861 ` 364` ``` assumes A: "Int_stable \ space = space M, sets = A \" ``` hoelzl@42861 ` 365` ``` assumes B: "Int_stable \ space = space M, sets = B \" ``` hoelzl@42981 ` 366` ``` shows "indep_set (sigma_sets (space M) A) (sigma_sets (space M) B)" ``` hoelzl@42861 ` 367` ```proof - ``` hoelzl@42861 ` 368` ``` have "indep_sets (\i. sigma_sets (space M) (case i of True \ A | False \ B)) UNIV" ``` hoelzl@42861 ` 369` ``` proof (rule indep_sets_sigma_sets) ``` hoelzl@42861 ` 370` ``` show "indep_sets (bool_case A B) UNIV" ``` hoelzl@42981 ` 371` ``` by (rule `indep_set A B`[unfolded indep_set_def]) ``` hoelzl@42861 ` 372` ``` fix i show "Int_stable \space = space M, sets = case i of True \ A | False \ B\" ``` hoelzl@42861 ` 373` ``` using A B by (cases i) auto ``` hoelzl@42861 ` 374` ``` qed ``` hoelzl@42861 ` 375` ``` then show ?thesis ``` hoelzl@42981 ` 376` ``` unfolding indep_set_def ``` hoelzl@42861 ` 377` ``` by (rule indep_sets_mono_sets) (auto split: bool.split) ``` hoelzl@42861 ` 378` ```qed ``` hoelzl@42861 ` 379` hoelzl@42981 ` 380` ```lemma (in prob_space) indep_sets_collect_sigma: ``` hoelzl@42981 ` 381` ``` fixes I :: "'j \ 'i set" and J :: "'j set" and E :: "'i \ 'a set set" ``` hoelzl@42981 ` 382` ``` assumes indep: "indep_sets E (\j\J. I j)" ``` hoelzl@42981 ` 383` ``` assumes Int_stable: "\i j. j \ J \ i \ I j \ Int_stable \space = space M, sets = E i\" ``` hoelzl@42981 ` 384` ``` assumes disjoint: "disjoint_family_on I J" ``` hoelzl@42981 ` 385` ``` shows "indep_sets (\j. sigma_sets (space M) (\i\I j. E i)) J" ``` hoelzl@42981 ` 386` ```proof - ``` wenzelm@46731 ` 387` ``` let ?E = "\j. {\k\K. E' k| E' K. finite K \ K \ {} \ K \ I j \ (\k\K. E' k \ E k) }" ``` hoelzl@42981 ` 388` hoelzl@42983 ` 389` ``` from indep have E: "\j i. j \ J \ i \ I j \ E i \ events" ``` hoelzl@42981 ` 390` ``` unfolding indep_sets_def by auto ``` hoelzl@42981 ` 391` ``` { fix j ``` hoelzl@42981 ` 392` ``` let ?S = "sigma \ space = space M, sets = (\i\I j. E i) \" ``` hoelzl@42981 ` 393` ``` assume "j \ J" ``` hoelzl@42981 ` 394` ``` from E[OF this] interpret S: sigma_algebra ?S ``` hoelzl@42981 ` 395` ``` using sets_into_space by (intro sigma_algebra_sigma) auto ``` hoelzl@42981 ` 396` hoelzl@42981 ` 397` ``` have "sigma_sets (space M) (\i\I j. E i) = sigma_sets (space M) (?E j)" ``` hoelzl@42981 ` 398` ``` proof (rule sigma_sets_eqI) ``` hoelzl@42981 ` 399` ``` fix A assume "A \ (\i\I j. E i)" ``` hoelzl@42981 ` 400` ``` then guess i .. ``` hoelzl@42981 ` 401` ``` then show "A \ sigma_sets (space M) (?E j)" ``` hoelzl@42981 ` 402` ``` by (auto intro!: sigma_sets.intros exI[of _ "{i}"] exI[of _ "\i. A"]) ``` hoelzl@42981 ` 403` ``` next ``` hoelzl@42981 ` 404` ``` fix A assume "A \ ?E j" ``` hoelzl@42981 ` 405` ``` then obtain E' K where "finite K" "K \ {}" "K \ I j" "\k. k \ K \ E' k \ E k" ``` hoelzl@42981 ` 406` ``` and A: "A = (\k\K. E' k)" ``` hoelzl@42981 ` 407` ``` by auto ``` hoelzl@42981 ` 408` ``` then have "A \ sets ?S" unfolding A ``` hoelzl@42981 ` 409` ``` by (safe intro!: S.finite_INT) ``` hoelzl@42981 ` 410` ``` (auto simp: sets_sigma intro!: sigma_sets.Basic) ``` hoelzl@42981 ` 411` ``` then show "A \ sigma_sets (space M) (\i\I j. E i)" ``` hoelzl@42981 ` 412` ``` by (simp add: sets_sigma) ``` hoelzl@42981 ` 413` ``` qed } ``` hoelzl@42981 ` 414` ``` moreover have "indep_sets (\j. sigma_sets (space M) (?E j)) J" ``` hoelzl@42981 ` 415` ``` proof (rule indep_sets_sigma_sets) ``` hoelzl@42981 ` 416` ``` show "indep_sets ?E J" ``` hoelzl@42981 ` 417` ``` proof (intro indep_setsI) ``` hoelzl@42981 ` 418` ``` fix j assume "j \ J" with E show "?E j \ events" by (force intro!: finite_INT) ``` hoelzl@42981 ` 419` ``` next ``` hoelzl@42981 ` 420` ``` fix K A assume K: "K \ {}" "K \ J" "finite K" ``` hoelzl@42981 ` 421` ``` and "\j\K. A j \ ?E j" ``` hoelzl@42981 ` 422` ``` 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 ` 423` ``` by simp ``` hoelzl@42981 ` 424` ``` from bchoice[OF this] guess E' .. ``` hoelzl@42981 ` 425` ``` from bchoice[OF this] obtain L ``` hoelzl@42981 ` 426` ``` where A: "\j. j\K \ A j = (\l\L j. E' j l)" ``` hoelzl@42981 ` 427` ``` and L: "\j. j\K \ finite (L j)" "\j. j\K \ L j \ {}" "\j. j\K \ L j \ I j" ``` hoelzl@42981 ` 428` ``` and E': "\j l. j\K \ l \ L j \ E' j l \ E l" ``` hoelzl@42981 ` 429` ``` by auto ``` hoelzl@42981 ` 430` hoelzl@42981 ` 431` ``` { fix k l j assume "k \ K" "j \ K" "l \ L j" "l \ L k" ``` hoelzl@42981 ` 432` ``` have "k = j" ``` hoelzl@42981 ` 433` ``` proof (rule ccontr) ``` hoelzl@42981 ` 434` ``` assume "k \ j" ``` hoelzl@42981 ` 435` ``` with disjoint `K \ J` `k \ K` `j \ K` have "I k \ I j = {}" ``` hoelzl@42981 ` 436` ``` unfolding disjoint_family_on_def by auto ``` hoelzl@42981 ` 437` ``` with L(2,3)[OF `j \ K`] L(2,3)[OF `k \ K`] ``` hoelzl@42981 ` 438` ``` show False using `l \ L k` `l \ L j` by auto ``` hoelzl@42981 ` 439` ``` qed } ``` hoelzl@42981 ` 440` ``` note L_inj = this ``` hoelzl@42981 ` 441` hoelzl@42981 ` 442` ``` def k \ "\l. (SOME k. k \ K \ l \ L k)" ``` hoelzl@42981 ` 443` ``` { fix x j l assume *: "j \ K" "l \ L j" ``` hoelzl@42981 ` 444` ``` have "k l = j" unfolding k_def ``` hoelzl@42981 ` 445` ``` proof (rule some_equality) ``` hoelzl@42981 ` 446` ``` fix k assume "k \ K \ l \ L k" ``` hoelzl@42981 ` 447` ``` with * L_inj show "k = j" by auto ``` hoelzl@42981 ` 448` ``` qed (insert *, simp) } ``` hoelzl@42981 ` 449` ``` note k_simp[simp] = this ``` wenzelm@46731 ` 450` ``` let ?E' = "\l. E' (k l) l" ``` hoelzl@42981 ` 451` ``` have "prob (\j\K. A j) = prob (\l\(\k\K. L k). ?E' l)" ``` hoelzl@42981 ` 452` ``` by (auto simp: A intro!: arg_cong[where f=prob]) ``` hoelzl@42981 ` 453` ``` also have "\ = (\l\(\k\K. L k). prob (?E' l))" ``` hoelzl@42981 ` 454` ``` using L K E' by (intro indep_setsD[OF indep]) (simp_all add: UN_mono) ``` hoelzl@42981 ` 455` ``` also have "\ = (\j\K. \l\L j. prob (E' j l))" ``` hoelzl@42981 ` 456` ``` using K L L_inj by (subst setprod_UN_disjoint) auto ``` hoelzl@42981 ` 457` ``` also have "\ = (\j\K. prob (A j))" ``` hoelzl@42981 ` 458` ``` using K L E' by (auto simp add: A intro!: setprod_cong indep_setsD[OF indep, symmetric]) blast ``` hoelzl@42981 ` 459` ``` finally show "prob (\j\K. A j) = (\j\K. prob (A j))" . ``` hoelzl@42981 ` 460` ``` qed ``` hoelzl@42981 ` 461` ``` next ``` hoelzl@42981 ` 462` ``` fix j assume "j \ J" ``` hoelzl@42981 ` 463` ``` show "Int_stable \ space = space M, sets = ?E j \" ``` hoelzl@42981 ` 464` ``` proof (rule Int_stableI) ``` hoelzl@42981 ` 465` ``` fix a assume "a \ ?E j" then obtain Ka Ea ``` hoelzl@42981 ` 466` ``` where a: "a = (\k\Ka. Ea k)" "finite Ka" "Ka \ {}" "Ka \ I j" "\k. k\Ka \ Ea k \ E k" by auto ``` hoelzl@42981 ` 467` ``` fix b assume "b \ ?E j" then obtain Kb Eb ``` hoelzl@42981 ` 468` ``` where b: "b = (\k\Kb. Eb k)" "finite Kb" "Kb \ {}" "Kb \ I j" "\k. k\Kb \ Eb k \ E k" by auto ``` hoelzl@42981 ` 469` ``` 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 ` 470` ``` have "a \ b = INTER (Ka \ Kb) ?A" ``` hoelzl@42981 ` 471` ``` by (simp add: a b set_eq_iff) auto ``` hoelzl@42981 ` 472` ``` with a b `j \ J` Int_stableD[OF Int_stable] show "a \ b \ ?E j" ``` hoelzl@42981 ` 473` ``` by (intro CollectI exI[of _ "Ka \ Kb"] exI[of _ ?A]) auto ``` hoelzl@42981 ` 474` ``` qed ``` hoelzl@42981 ` 475` ``` qed ``` hoelzl@42981 ` 476` ``` ultimately show ?thesis ``` hoelzl@42981 ` 477` ``` by (simp cong: indep_sets_cong) ``` hoelzl@42981 ` 478` ```qed ``` hoelzl@42981 ` 479` hoelzl@42982 ` 480` ```definition (in prob_space) terminal_events where ``` hoelzl@42982 ` 481` ``` "terminal_events A = (\n. sigma_sets (space M) (UNION {n..} A))" ``` hoelzl@42982 ` 482` hoelzl@42982 ` 483` ```lemma (in prob_space) terminal_events_sets: ``` hoelzl@42983 ` 484` ``` assumes A: "\i. A i \ events" ``` hoelzl@42982 ` 485` ``` assumes "\i::nat. sigma_algebra \space = space M, sets = A i\" ``` hoelzl@42982 ` 486` ``` assumes X: "X \ terminal_events A" ``` hoelzl@42983 ` 487` ``` shows "X \ events" ``` hoelzl@42982 ` 488` ```proof - ``` hoelzl@42982 ` 489` ``` let ?A = "(\n. sigma_sets (space M) (UNION {n..} A))" ``` hoelzl@42982 ` 490` ``` interpret A: sigma_algebra "\space = space M, sets = A i\" for i by fact ``` hoelzl@42982 ` 491` ``` from X have "\n. X \ sigma_sets (space M) (UNION {n..} A)" by (auto simp: terminal_events_def) ``` hoelzl@42982 ` 492` ``` from this[of 0] have "X \ sigma_sets (space M) (UNION UNIV A)" by simp ``` hoelzl@42983 ` 493` ``` then show "X \ events" ``` hoelzl@42982 ` 494` ``` by induct (insert A, auto) ``` hoelzl@42982 ` 495` ```qed ``` hoelzl@42982 ` 496` hoelzl@42982 ` 497` ```lemma (in prob_space) sigma_algebra_terminal_events: ``` hoelzl@42982 ` 498` ``` assumes "\i::nat. sigma_algebra \space = space M, sets = A i\" ``` hoelzl@42982 ` 499` ``` shows "sigma_algebra \ space = space M, sets = terminal_events A \" ``` hoelzl@42982 ` 500` ``` unfolding terminal_events_def ``` hoelzl@42982 ` 501` ```proof (simp add: sigma_algebra_iff2, safe) ``` hoelzl@42982 ` 502` ``` let ?A = "(\n. sigma_sets (space M) (UNION {n..} A))" ``` hoelzl@42982 ` 503` ``` interpret A: sigma_algebra "\space = space M, sets = A i\" for i by fact ``` hoelzl@43340 ` 504` ``` { fix X x assume "X \ ?A" "x \ X" ``` hoelzl@42982 ` 505` ``` then have "\n. X \ sigma_sets (space M) (UNION {n..} A)" by auto ``` hoelzl@42982 ` 506` ``` from this[of 0] have "X \ sigma_sets (space M) (UNION UNIV A)" by simp ``` hoelzl@42982 ` 507` ``` then have "X \ space M" ``` hoelzl@42982 ` 508` ``` by induct (insert A.sets_into_space, auto) ``` hoelzl@42982 ` 509` ``` with `x \ X` show "x \ space M" by auto } ``` hoelzl@42982 ` 510` ``` { fix F :: "nat \ 'a set" and n assume "range F \ ?A" ``` hoelzl@42982 ` 511` ``` then show "(UNION UNIV F) \ sigma_sets (space M) (UNION {n..} A)" ``` hoelzl@42982 ` 512` ``` by (intro sigma_sets.Union) auto } ``` hoelzl@42982 ` 513` ```qed (auto intro!: sigma_sets.Compl sigma_sets.Empty) ``` hoelzl@42982 ` 514` hoelzl@42982 ` 515` ```lemma (in prob_space) kolmogorov_0_1_law: ``` hoelzl@42982 ` 516` ``` fixes A :: "nat \ 'a set set" ``` hoelzl@42983 ` 517` ``` assumes A: "\i. A i \ events" ``` hoelzl@42982 ` 518` ``` assumes "\i::nat. sigma_algebra \space = space M, sets = A i\" ``` hoelzl@42982 ` 519` ``` assumes indep: "indep_sets A UNIV" ``` hoelzl@42982 ` 520` ``` and X: "X \ terminal_events A" ``` hoelzl@42982 ` 521` ``` shows "prob X = 0 \ prob X = 1" ``` hoelzl@42982 ` 522` ```proof - ``` hoelzl@42983 ` 523` ``` let ?D = "\ space = space M, sets = {D \ events. prob (X \ D) = prob X * prob D} \" ``` hoelzl@42982 ` 524` ``` interpret A: sigma_algebra "\space = space M, sets = A i\" for i by fact ``` hoelzl@42982 ` 525` ``` interpret T: sigma_algebra "\ space = space M, sets = terminal_events A \" ``` hoelzl@42982 ` 526` ``` by (rule sigma_algebra_terminal_events) fact ``` hoelzl@42982 ` 527` ``` have "X \ space M" using T.space_closed X by auto ``` hoelzl@42982 ` 528` hoelzl@42983 ` 529` ``` have X_in: "X \ events" ``` hoelzl@42982 ` 530` ``` by (rule terminal_events_sets) fact+ ``` hoelzl@42982 ` 531` hoelzl@42982 ` 532` ``` interpret D: dynkin_system ?D ``` hoelzl@42982 ` 533` ``` proof (rule dynkin_systemI) ``` hoelzl@42982 ` 534` ``` fix D assume "D \ sets ?D" then show "D \ space ?D" ``` hoelzl@42982 ` 535` ``` using sets_into_space by auto ``` hoelzl@42982 ` 536` ``` next ``` hoelzl@42982 ` 537` ``` show "space ?D \ sets ?D" ``` hoelzl@42982 ` 538` ``` using prob_space `X \ space M` by (simp add: Int_absorb2) ``` hoelzl@42982 ` 539` ``` next ``` hoelzl@42982 ` 540` ``` fix A assume A: "A \ sets ?D" ``` hoelzl@42982 ` 541` ``` have "prob (X \ (space M - A)) = prob (X - (X \ A))" ``` hoelzl@42982 ` 542` ``` using `X \ space M` by (auto intro!: arg_cong[where f=prob]) ``` hoelzl@42982 ` 543` ``` also have "\ = prob X - prob (X \ A)" ``` hoelzl@42982 ` 544` ``` using X_in A by (intro finite_measure_Diff) auto ``` hoelzl@42982 ` 545` ``` also have "\ = prob X * prob (space M) - prob X * prob A" ``` hoelzl@42982 ` 546` ``` using A prob_space by auto ``` hoelzl@42982 ` 547` ``` also have "\ = prob X * prob (space M - A)" ``` hoelzl@42982 ` 548` ``` using X_in A sets_into_space ``` hoelzl@42982 ` 549` ``` by (subst finite_measure_Diff) (auto simp: field_simps) ``` hoelzl@42982 ` 550` ``` finally show "space ?D - A \ sets ?D" ``` hoelzl@42982 ` 551` ``` using A `X \ space M` by auto ``` hoelzl@42982 ` 552` ``` next ``` hoelzl@42982 ` 553` ``` fix F :: "nat \ 'a set" assume dis: "disjoint_family F" and "range F \ sets ?D" ``` hoelzl@42982 ` 554` ``` then have F: "range F \ events" "\i. prob (X \ F i) = prob X * prob (F i)" ``` hoelzl@42982 ` 555` ``` by auto ``` hoelzl@42982 ` 556` ``` have "(\i. prob (X \ F i)) sums prob (\i. X \ F i)" ``` hoelzl@42982 ` 557` ``` proof (rule finite_measure_UNION) ``` hoelzl@42982 ` 558` ``` show "range (\i. X \ F i) \ events" ``` hoelzl@42982 ` 559` ``` using F X_in by auto ``` hoelzl@42982 ` 560` ``` show "disjoint_family (\i. X \ F i)" ``` hoelzl@42982 ` 561` ``` using dis by (rule disjoint_family_on_bisimulation) auto ``` hoelzl@42982 ` 562` ``` qed ``` hoelzl@42982 ` 563` ``` with F have "(\i. prob X * prob (F i)) sums prob (X \ (\i. F i))" ``` hoelzl@42982 ` 564` ``` by simp ``` hoelzl@42982 ` 565` ``` moreover have "(\i. prob X * prob (F i)) sums (prob X * prob (\i. F i))" ``` huffman@44282 ` 566` ``` by (intro sums_mult finite_measure_UNION F dis) ``` hoelzl@42982 ` 567` ``` ultimately have "prob (X \ (\i. F i)) = prob X * prob (\i. F i)" ``` hoelzl@42982 ` 568` ``` by (auto dest!: sums_unique) ``` hoelzl@42982 ` 569` ``` with F show "(\i. F i) \ sets ?D" ``` hoelzl@42982 ` 570` ``` by auto ``` hoelzl@42982 ` 571` ``` qed ``` hoelzl@42982 ` 572` hoelzl@42982 ` 573` ``` { fix n ``` hoelzl@42982 ` 574` ``` have "indep_sets (\b. sigma_sets (space M) (\m\bool_case {..n} {Suc n..} b. A m)) UNIV" ``` hoelzl@42982 ` 575` ``` proof (rule indep_sets_collect_sigma) ``` hoelzl@42982 ` 576` ``` have *: "(\b. case b of True \ {..n} | False \ {Suc n..}) = UNIV" (is "?U = _") ``` hoelzl@42982 ` 577` ``` by (simp split: bool.split add: set_eq_iff) (metis not_less_eq_eq) ``` hoelzl@42982 ` 578` ``` with indep show "indep_sets A ?U" by simp ``` hoelzl@42982 ` 579` ``` show "disjoint_family (bool_case {..n} {Suc n..})" ``` hoelzl@42982 ` 580` ``` unfolding disjoint_family_on_def by (auto split: bool.split) ``` hoelzl@42982 ` 581` ``` fix m ``` hoelzl@42982 ` 582` ``` show "Int_stable \space = space M, sets = A m\" ``` hoelzl@42982 ` 583` ``` unfolding Int_stable_def using A.Int by auto ``` hoelzl@42982 ` 584` ``` qed ``` hoelzl@43340 ` 585` ``` also have "(\b. sigma_sets (space M) (\m\bool_case {..n} {Suc n..} b. A m)) = ``` hoelzl@42982 ` 586` ``` bool_case (sigma_sets (space M) (\m\{..n}. A m)) (sigma_sets (space M) (\m\{Suc n..}. A m))" ``` hoelzl@42982 ` 587` ``` by (auto intro!: ext split: bool.split) ``` hoelzl@42982 ` 588` ``` finally have indep: "indep_set (sigma_sets (space M) (\m\{..n}. A m)) (sigma_sets (space M) (\m\{Suc n..}. A m))" ``` hoelzl@42982 ` 589` ``` unfolding indep_set_def by simp ``` hoelzl@42982 ` 590` hoelzl@42982 ` 591` ``` have "sigma_sets (space M) (\m\{..n}. A m) \ sets ?D" ``` hoelzl@42982 ` 592` ``` proof (simp add: subset_eq, rule) ``` hoelzl@42982 ` 593` ``` fix D assume D: "D \ sigma_sets (space M) (\m\{..n}. A m)" ``` hoelzl@42982 ` 594` ``` have "X \ sigma_sets (space M) (\m\{Suc n..}. A m)" ``` hoelzl@42982 ` 595` ``` using X unfolding terminal_events_def by simp ``` hoelzl@42982 ` 596` ``` from indep_setD[OF indep D this] indep_setD_ev1[OF indep] D ``` hoelzl@42982 ` 597` ``` show "D \ events \ prob (X \ D) = prob X * prob D" ``` hoelzl@42982 ` 598` ``` by (auto simp add: ac_simps) ``` hoelzl@42982 ` 599` ``` qed } ``` hoelzl@42982 ` 600` ``` then have "(\n. sigma_sets (space M) (\m\{..n}. A m)) \ sets ?D" (is "?A \ _") ``` hoelzl@42982 ` 601` ``` by auto ``` hoelzl@42982 ` 602` hoelzl@42982 ` 603` ``` have "sigma \ space = space M, sets = ?A \ = ``` hoelzl@42982 ` 604` ``` dynkin \ space = space M, sets = ?A \" (is "sigma ?UA = dynkin ?UA") ``` hoelzl@42982 ` 605` ``` proof (rule sigma_eq_dynkin) ``` hoelzl@42982 ` 606` ``` { fix B n assume "B \ sigma_sets (space M) (\m\{..n}. A m)" ``` hoelzl@42982 ` 607` ``` then have "B \ space M" ``` hoelzl@42982 ` 608` ``` by induct (insert A sets_into_space, auto) } ``` hoelzl@42982 ` 609` ``` then show "sets ?UA \ Pow (space ?UA)" by auto ``` hoelzl@42982 ` 610` ``` show "Int_stable ?UA" ``` hoelzl@42982 ` 611` ``` proof (rule Int_stableI) ``` hoelzl@42982 ` 612` ``` fix a assume "a \ ?A" then guess n .. note a = this ``` hoelzl@42982 ` 613` ``` fix b assume "b \ ?A" then guess m .. note b = this ``` hoelzl@42982 ` 614` ``` interpret Amn: sigma_algebra "sigma \space = space M, sets = (\i\{..max m n}. A i)\" ``` hoelzl@42982 ` 615` ``` using A sets_into_space by (intro sigma_algebra_sigma) auto ``` hoelzl@42982 ` 616` ``` have "sigma_sets (space M) (\i\{..n}. A i) \ sigma_sets (space M) (\i\{..max m n}. A i)" ``` hoelzl@42982 ` 617` ``` by (intro sigma_sets_subseteq UN_mono) auto ``` hoelzl@42982 ` 618` ``` with a have "a \ sigma_sets (space M) (\i\{..max m n}. A i)" by auto ``` hoelzl@42982 ` 619` ``` moreover ``` hoelzl@42982 ` 620` ``` have "sigma_sets (space M) (\i\{..m}. A i) \ sigma_sets (space M) (\i\{..max m n}. A i)" ``` hoelzl@42982 ` 621` ``` by (intro sigma_sets_subseteq UN_mono) auto ``` hoelzl@42982 ` 622` ``` with b have "b \ sigma_sets (space M) (\i\{..max m n}. A i)" by auto ``` hoelzl@42982 ` 623` ``` ultimately have "a \ b \ sigma_sets (space M) (\i\{..max m n}. A i)" ``` hoelzl@42982 ` 624` ``` using Amn.Int[of a b] by (simp add: sets_sigma) ``` hoelzl@42982 ` 625` ``` then show "a \ b \ (\n. sigma_sets (space M) (\i\{..n}. A i))" by auto ``` hoelzl@42982 ` 626` ``` qed ``` hoelzl@42982 ` 627` ``` qed ``` hoelzl@42982 ` 628` ``` moreover have "sets (dynkin ?UA) \ sets ?D" ``` hoelzl@42982 ` 629` ``` proof (rule D.dynkin_subset) ``` hoelzl@42982 ` 630` ``` show "sets ?UA \ sets ?D" using `?A \ sets ?D` by auto ``` hoelzl@42982 ` 631` ``` qed simp ``` hoelzl@42982 ` 632` ``` ultimately have "sets (sigma ?UA) \ sets ?D" by simp ``` hoelzl@42982 ` 633` ``` moreover ``` hoelzl@42982 ` 634` ``` have "\n. sigma_sets (space M) (\i\{n..}. A i) \ sigma_sets (space M) ?A" ``` hoelzl@42982 ` 635` ``` by (intro sigma_sets_subseteq UN_mono) (auto intro: sigma_sets.Basic) ``` hoelzl@42982 ` 636` ``` then have "terminal_events A \ sets (sigma ?UA)" ``` hoelzl@42982 ` 637` ``` unfolding sets_sigma terminal_events_def by auto ``` hoelzl@42982 ` 638` ``` moreover note `X \ terminal_events A` ``` hoelzl@42982 ` 639` ``` ultimately have "X \ sets ?D" by auto ``` hoelzl@42982 ` 640` ``` then show ?thesis by auto ``` hoelzl@42982 ` 641` ```qed ``` hoelzl@42982 ` 642` hoelzl@42985 ` 643` ```lemma (in prob_space) borel_0_1_law: ``` hoelzl@42985 ` 644` ``` fixes F :: "nat \ 'a set" ``` hoelzl@42985 ` 645` ``` assumes F: "range F \ events" "indep_events F UNIV" ``` hoelzl@42985 ` 646` ``` shows "prob (\n. \m\{n..}. F m) = 0 \ prob (\n. \m\{n..}. F m) = 1" ``` hoelzl@42985 ` 647` ```proof (rule kolmogorov_0_1_law[of "\i. sigma_sets (space M) { F i }"]) ``` hoelzl@42985 ` 648` ``` show "\i. sigma_sets (space M) {F i} \ events" ``` hoelzl@42985 ` 649` ``` using F(1) sets_into_space ``` hoelzl@42985 ` 650` ``` by (subst sigma_sets_singleton) auto ``` hoelzl@42985 ` 651` ``` { fix i show "sigma_algebra \space = space M, sets = sigma_sets (space M) {F i}\" ``` hoelzl@42985 ` 652` ``` using sigma_algebra_sigma[of "\space = space M, sets = {F i}\"] F sets_into_space ``` hoelzl@42985 ` 653` ``` by (auto simp add: sigma_def) } ``` hoelzl@42985 ` 654` ``` show "indep_sets (\i. sigma_sets (space M) {F i}) UNIV" ``` hoelzl@42985 ` 655` ``` proof (rule indep_sets_sigma_sets) ``` hoelzl@42985 ` 656` ``` show "indep_sets (\i. {F i}) UNIV" ``` hoelzl@42985 ` 657` ``` unfolding indep_sets_singleton_iff_indep_events by fact ``` hoelzl@42985 ` 658` ``` fix i show "Int_stable \space = space M, sets = {F i}\" ``` hoelzl@42985 ` 659` ``` unfolding Int_stable_def by simp ``` hoelzl@42985 ` 660` ``` qed ``` wenzelm@46731 ` 661` ``` let ?Q = "\n. \i\{n..}. F i" ``` hoelzl@42985 ` 662` ``` show "(\n. \m\{n..}. F m) \ terminal_events (\i. sigma_sets (space M) {F i})" ``` hoelzl@42985 ` 663` ``` unfolding terminal_events_def ``` hoelzl@42985 ` 664` ``` proof ``` hoelzl@42985 ` 665` ``` fix j ``` hoelzl@42985 ` 666` ``` interpret S: sigma_algebra "sigma \ space = space M, sets = (\i\{j..}. sigma_sets (space M) {F i})\" ``` hoelzl@42985 ` 667` ``` using order_trans[OF F(1) space_closed] ``` hoelzl@42985 ` 668` ``` by (intro sigma_algebra_sigma) (simp add: sigma_sets_singleton subset_eq) ``` hoelzl@42985 ` 669` ``` have "(\n. ?Q n) = (\n\{j..}. ?Q n)" ``` hoelzl@42985 ` 670` ``` by (intro decseq_SucI INT_decseq_offset UN_mono) auto ``` hoelzl@42985 ` 671` ``` also have "\ \ sets (sigma \ space = space M, sets = (\i\{j..}. sigma_sets (space M) {F i})\)" ``` hoelzl@42985 ` 672` ``` using order_trans[OF F(1) space_closed] ``` hoelzl@42985 ` 673` ``` by (safe intro!: S.countable_INT S.countable_UN) ``` hoelzl@42985 ` 674` ``` (auto simp: sets_sigma sigma_sets_singleton intro!: sigma_sets.Basic bexI) ``` hoelzl@42985 ` 675` ``` finally show "(\n. ?Q n) \ sigma_sets (space M) (\i\{j..}. sigma_sets (space M) {F i})" ``` hoelzl@42985 ` 676` ``` by (simp add: sets_sigma) ``` hoelzl@42985 ` 677` ``` qed ``` hoelzl@42985 ` 678` ```qed ``` hoelzl@42985 ` 679` hoelzl@42987 ` 680` ```lemma (in prob_space) indep_sets_finite: ``` hoelzl@42987 ` 681` ``` assumes I: "I \ {}" "finite I" ``` hoelzl@42987 ` 682` ``` and F: "\i. i \ I \ F i \ events" "\i. i \ I \ space M \ F i" ``` hoelzl@42987 ` 683` ``` shows "indep_sets F I \ (\A\Pi I F. prob (\j\I. A j) = (\j\I. prob (A j)))" ``` hoelzl@42987 ` 684` ```proof ``` hoelzl@42987 ` 685` ``` assume *: "indep_sets F I" ``` hoelzl@42987 ` 686` ``` from I show "\A\Pi I F. prob (\j\I. A j) = (\j\I. prob (A j))" ``` hoelzl@42987 ` 687` ``` by (intro indep_setsD[OF *] ballI) auto ``` hoelzl@42987 ` 688` ```next ``` hoelzl@42987 ` 689` ``` assume indep: "\A\Pi I F. prob (\j\I. A j) = (\j\I. prob (A j))" ``` hoelzl@42987 ` 690` ``` show "indep_sets F I" ``` hoelzl@42987 ` 691` ``` proof (rule indep_setsI[OF F(1)]) ``` hoelzl@42987 ` 692` ``` fix A J assume J: "J \ {}" "J \ I" "finite J" ``` hoelzl@42987 ` 693` ``` assume A: "\j\J. A j \ F j" ``` wenzelm@46731 ` 694` ``` let ?A = "\j. if j \ J then A j else space M" ``` hoelzl@42987 ` 695` ``` have "prob (\j\I. ?A j) = prob (\j\J. A j)" ``` hoelzl@42987 ` 696` ``` using subset_trans[OF F(1) space_closed] J A ``` hoelzl@42987 ` 697` ``` by (auto intro!: arg_cong[where f=prob] split: split_if_asm) blast ``` hoelzl@42987 ` 698` ``` also ``` hoelzl@42987 ` 699` ``` from A F have "(\j. if j \ J then A j else space M) \ Pi I F" (is "?A \ _") ``` hoelzl@42987 ` 700` ``` by (auto split: split_if_asm) ``` hoelzl@42987 ` 701` ``` with indep have "prob (\j\I. ?A j) = (\j\I. prob (?A j))" ``` hoelzl@42987 ` 702` ``` by auto ``` hoelzl@42987 ` 703` ``` also have "\ = (\j\J. prob (A j))" ``` hoelzl@42987 ` 704` ``` unfolding if_distrib setprod.If_cases[OF `finite I`] ``` hoelzl@42987 ` 705` ``` using prob_space `J \ I` by (simp add: Int_absorb1 setprod_1) ``` hoelzl@42987 ` 706` ``` finally show "prob (\j\J. A j) = (\j\J. prob (A j))" .. ``` hoelzl@42987 ` 707` ``` qed ``` hoelzl@42987 ` 708` ```qed ``` hoelzl@42987 ` 709` hoelzl@42989 ` 710` ```lemma (in prob_space) indep_vars_finite: ``` hoelzl@42987 ` 711` ``` fixes I :: "'i set" ``` hoelzl@42987 ` 712` ``` assumes I: "I \ {}" "finite I" ``` hoelzl@42987 ` 713` ``` and rv: "\i. i \ I \ random_variable (sigma (M' i)) (X i)" ``` hoelzl@42987 ` 714` ``` and Int_stable: "\i. i \ I \ Int_stable (M' i)" ``` hoelzl@42987 ` 715` ``` and space: "\i. i \ I \ space (M' i) \ sets (M' i)" ``` hoelzl@42989 ` 716` ``` shows "indep_vars (\i. sigma (M' i)) X I \ ``` hoelzl@42988 ` 717` ``` (\A\(\ i\I. sets (M' i)). prob (\j\I. X j -` A j \ space M) = (\j\I. prob (X j -` A j \ space M)))" ``` hoelzl@42987 ` 718` ```proof - ``` hoelzl@42987 ` 719` ``` from rv have X: "\i. i \ I \ X i \ space M \ space (M' i)" ``` hoelzl@42987 ` 720` ``` unfolding measurable_def by simp ``` hoelzl@42987 ` 721` hoelzl@42987 ` 722` ``` { fix i assume "i\I" ``` hoelzl@42987 ` 723` ``` have "sigma_sets (space M) {X i -` A \ space M |A. A \ sets (sigma (M' i))} ``` hoelzl@42987 ` 724` ``` = sigma_sets (space M) {X i -` A \ space M |A. A \ sets (M' i)}" ``` hoelzl@42987 ` 725` ``` unfolding sigma_sets_vimage_commute[OF X, OF `i \ I`] ``` hoelzl@42987 ` 726` ``` by (subst sigma_sets_sigma_sets_eq) auto } ``` hoelzl@42987 ` 727` ``` note this[simp] ``` hoelzl@42987 ` 728` hoelzl@42987 ` 729` ``` { fix i assume "i\I" ``` hoelzl@42987 ` 730` ``` have "Int_stable \space = space M, sets = {X i -` A \ space M |A. A \ sets (M' i)}\" ``` hoelzl@42987 ` 731` ``` proof (rule Int_stableI) ``` hoelzl@42987 ` 732` ``` fix a assume "a \ {X i -` A \ space M |A. A \ sets (M' i)}" ``` hoelzl@42987 ` 733` ``` then obtain A where "a = X i -` A \ space M" "A \ sets (M' i)" by auto ``` hoelzl@42987 ` 734` ``` moreover ``` hoelzl@42987 ` 735` ``` fix b assume "b \ {X i -` A \ space M |A. A \ sets (M' i)}" ``` hoelzl@42987 ` 736` ``` then obtain B where "b = X i -` B \ space M" "B \ sets (M' i)" by auto ``` hoelzl@42987 ` 737` ``` moreover ``` hoelzl@42987 ` 738` ``` have "(X i -` A \ space M) \ (X i -` B \ space M) = X i -` (A \ B) \ space M" by auto ``` hoelzl@42987 ` 739` ``` moreover note Int_stable[OF `i \ I`] ``` hoelzl@42987 ` 740` ``` ultimately ``` hoelzl@42987 ` 741` ``` show "a \ b \ {X i -` A \ space M |A. A \ sets (M' i)}" ``` hoelzl@42987 ` 742` ``` by (auto simp del: vimage_Int intro!: exI[of _ "A \ B"] dest: Int_stableD) ``` hoelzl@42987 ` 743` ``` qed } ``` hoelzl@42987 ` 744` ``` note indep_sets_sigma_sets_iff[OF this, simp] ``` hoelzl@43340 ` 745` hoelzl@42987 ` 746` ``` { fix i assume "i \ I" ``` hoelzl@42987 ` 747` ``` { fix A assume "A \ sets (M' i)" ``` hoelzl@42987 ` 748` ``` then have "A \ sets (sigma (M' i))" by (auto simp: sets_sigma intro: sigma_sets.Basic) ``` hoelzl@42987 ` 749` ``` moreover ``` hoelzl@42987 ` 750` ``` from rv[OF `i\I`] have "X i \ measurable M (sigma (M' i))" by auto ``` hoelzl@42987 ` 751` ``` ultimately ``` hoelzl@42987 ` 752` ``` have "X i -` A \ space M \ sets M" by (auto intro: measurable_sets) } ``` hoelzl@42987 ` 753` ``` with X[OF `i\I`] space[OF `i\I`] ``` hoelzl@42987 ` 754` ``` have "{X i -` A \ space M |A. A \ sets (M' i)} \ events" ``` hoelzl@42987 ` 755` ``` "space M \ {X i -` A \ space M |A. A \ sets (M' i)}" ``` hoelzl@42987 ` 756` ``` by (auto intro!: exI[of _ "space (M' i)"]) } ``` hoelzl@42987 ` 757` ``` note indep_sets_finite[OF I this, simp] ``` hoelzl@43340 ` 758` hoelzl@42987 ` 759` ``` have "(\A\\ i\I. {X i -` A \ space M |A. A \ sets (M' i)}. prob (INTER I A) = (\j\I. prob (A j))) = ``` hoelzl@42987 ` 760` ``` (\A\\ i\I. sets (M' i). prob ((\j\I. X j -` A j) \ space M) = (\x\I. prob (X x -` A x \ space M)))" ``` hoelzl@42987 ` 761` ``` (is "?L = ?R") ``` hoelzl@42987 ` 762` ``` proof safe ``` hoelzl@42987 ` 763` ``` fix A assume ?L and A: "A \ (\ i\I. sets (M' i))" ``` hoelzl@42987 ` 764` ``` from `?L`[THEN bspec, of "\i. X i -` A i \ space M"] A `I \ {}` ``` hoelzl@42987 ` 765` ``` show "prob ((\j\I. X j -` A j) \ space M) = (\x\I. prob (X x -` A x \ space M))" ``` hoelzl@42987 ` 766` ``` by (auto simp add: Pi_iff) ``` hoelzl@42987 ` 767` ``` next ``` hoelzl@42987 ` 768` ``` fix A assume ?R and A: "A \ (\ i\I. {X i -` A \ space M |A. A \ sets (M' i)})" ``` hoelzl@42987 ` 769` ``` from A have "\i\I. \B. A i = X i -` B \ space M \ B \ sets (M' i)" by auto ``` hoelzl@42987 ` 770` ``` from bchoice[OF this] obtain B where B: "\i\I. A i = X i -` B i \ space M" ``` hoelzl@42987 ` 771` ``` "B \ (\ i\I. sets (M' i))" by auto ``` hoelzl@42987 ` 772` ``` from `?R`[THEN bspec, OF B(2)] B(1) `I \ {}` ``` hoelzl@42987 ` 773` ``` show "prob (INTER I A) = (\j\I. prob (A j))" ``` hoelzl@42987 ` 774` ``` by simp ``` hoelzl@42987 ` 775` ``` qed ``` hoelzl@42987 ` 776` ``` then show ?thesis using `I \ {}` ``` hoelzl@42989 ` 777` ``` by (simp add: rv indep_vars_def) ``` hoelzl@42988 ` 778` ```qed ``` hoelzl@42988 ` 779` hoelzl@42989 ` 780` ```lemma (in prob_space) indep_vars_compose: ``` hoelzl@42989 ` 781` ``` assumes "indep_vars M' X I" ``` hoelzl@42988 ` 782` ``` assumes rv: ``` hoelzl@42988 ` 783` ``` "\i. i \ I \ sigma_algebra (N i)" ``` hoelzl@42988 ` 784` ``` "\i. i \ I \ Y i \ measurable (M' i) (N i)" ``` hoelzl@42989 ` 785` ``` shows "indep_vars N (\i. Y i \ X i) I" ``` hoelzl@42989 ` 786` ``` unfolding indep_vars_def ``` hoelzl@42988 ` 787` ```proof ``` hoelzl@42989 ` 788` ``` from rv `indep_vars M' X I` ``` hoelzl@42988 ` 789` ``` show "\i\I. random_variable (N i) (Y i \ X i)" ``` hoelzl@42989 ` 790` ``` by (auto intro!: measurable_comp simp: indep_vars_def) ``` hoelzl@42988 ` 791` hoelzl@42988 ` 792` ``` have "indep_sets (\i. sigma_sets (space M) {X i -` A \ space M |A. A \ sets (M' i)}) I" ``` hoelzl@42989 ` 793` ``` using `indep_vars M' X I` by (simp add: indep_vars_def) ``` hoelzl@42988 ` 794` ``` then show "indep_sets (\i. sigma_sets (space M) {(Y i \ X i) -` A \ space M |A. A \ sets (N i)}) I" ``` hoelzl@42988 ` 795` ``` proof (rule indep_sets_mono_sets) ``` hoelzl@42988 ` 796` ``` fix i assume "i \ I" ``` hoelzl@42989 ` 797` ``` with `indep_vars M' X I` have X: "X i \ space M \ space (M' i)" ``` hoelzl@42989 ` 798` ``` unfolding indep_vars_def measurable_def by auto ``` hoelzl@42988 ` 799` ``` { fix A assume "A \ sets (N i)" ``` hoelzl@42988 ` 800` ``` then have "\B. (Y i \ X i) -` A \ space M = X i -` B \ space M \ B \ sets (M' i)" ``` hoelzl@42988 ` 801` ``` by (intro exI[of _ "Y i -` A \ space (M' i)"]) ``` hoelzl@42988 ` 802` ``` (auto simp: vimage_compose intro!: measurable_sets rv `i \ I` funcset_mem[OF X]) } ``` hoelzl@42988 ` 803` ``` then show "sigma_sets (space M) {(Y i \ X i) -` A \ space M |A. A \ sets (N i)} \ ``` hoelzl@42988 ` 804` ``` sigma_sets (space M) {X i -` A \ space M |A. A \ sets (M' i)}" ``` hoelzl@42988 ` 805` ``` by (intro sigma_sets_subseteq) (auto simp: vimage_compose) ``` hoelzl@42988 ` 806` ``` qed ``` hoelzl@42988 ` 807` ```qed ``` hoelzl@42988 ` 808` hoelzl@42989 ` 809` ```lemma (in prob_space) indep_varsD: ``` hoelzl@42989 ` 810` ``` assumes X: "indep_vars M' X I" ``` hoelzl@42988 ` 811` ``` assumes I: "I \ {}" "finite I" "\i. i \ I \ A i \ sets (M' i)" ``` hoelzl@42988 ` 812` ``` shows "prob (\i\I. X i -` A i \ space M) = (\i\I. prob (X i -` A i \ space M))" ``` hoelzl@42988 ` 813` ```proof (rule indep_setsD) ``` hoelzl@42988 ` 814` ``` show "indep_sets (\i. sigma_sets (space M) {X i -` A \ space M |A. A \ sets (M' i)}) I" ``` hoelzl@42989 ` 815` ``` using X by (auto simp: indep_vars_def) ``` hoelzl@42988 ` 816` ``` show "I \ I" "I \ {}" "finite I" using I by auto ``` hoelzl@42988 ` 817` ``` show "\i\I. X i -` A i \ space M \ sigma_sets (space M) {X i -` A \ space M |A. A \ sets (M' i)}" ``` hoelzl@42988 ` 818` ``` using I by (auto intro: sigma_sets.Basic) ``` hoelzl@42988 ` 819` ```qed ``` hoelzl@42988 ` 820` hoelzl@42988 ` 821` ```lemma (in prob_space) indep_distribution_eq_measure: ``` hoelzl@42988 ` 822` ``` assumes I: "I \ {}" "finite I" ``` hoelzl@42988 ` 823` ``` assumes rv: "\i. random_variable (M' i) (X i)" ``` hoelzl@42989 ` 824` ``` shows "indep_vars M' X I \ ``` hoelzl@43920 ` 825` ``` (\A\sets (\\<^isub>M i\I. (M' i \ measure := ereal\distribution (X i) \)). ``` hoelzl@42988 ` 826` ``` distribution (\x. \i\I. X i x) A = ``` hoelzl@43920 ` 827` ``` finite_measure.\' (\\<^isub>M i\I. (M' i \ measure := ereal\distribution (X i) \)) A)" ``` hoelzl@42988 ` 828` ``` (is "_ \ (\X\_. distribution ?D X = finite_measure.\' (Pi\<^isub>M I ?M) X)") ``` hoelzl@42988 ` 829` ```proof - ``` hoelzl@42988 ` 830` ``` interpret M': prob_space "?M i" for i ``` hoelzl@42988 ` 831` ``` using rv by (rule distribution_prob_space) ``` hoelzl@42988 ` 832` ``` interpret P: finite_product_prob_space ?M I ``` hoelzl@42988 ` 833` ``` proof qed fact ``` hoelzl@42988 ` 834` hoelzl@43920 ` 835` ``` let ?D' = "(Pi\<^isub>M I ?M) \ measure := ereal \ distribution ?D \" ``` hoelzl@42988 ` 836` ``` have "random_variable P.P ?D" ``` hoelzl@42988 ` 837` ``` using `finite I` rv by (intro random_variable_restrict) auto ``` hoelzl@42988 ` 838` ``` then interpret D: prob_space ?D' ``` hoelzl@42988 ` 839` ``` by (rule distribution_prob_space) ``` hoelzl@42988 ` 840` hoelzl@42988 ` 841` ``` show ?thesis ``` hoelzl@42988 ` 842` ``` proof (intro iffI ballI) ``` hoelzl@42989 ` 843` ``` assume "indep_vars M' X I" ``` hoelzl@42988 ` 844` ``` fix A assume "A \ sets P.P" ``` hoelzl@42988 ` 845` ``` moreover ``` hoelzl@42988 ` 846` ``` have "D.prob A = P.prob A" ``` hoelzl@42988 ` 847` ``` proof (rule prob_space_unique_Int_stable) ``` hoelzl@45777 ` 848` ``` show "prob_space ?D'" by unfold_locales ``` hoelzl@45777 ` 849` ``` show "prob_space (Pi\<^isub>M I ?M)" by unfold_locales ``` hoelzl@42988 ` 850` ``` show "Int_stable P.G" using M'.Int ``` hoelzl@42988 ` 851` ``` by (intro Int_stable_product_algebra_generator) (simp add: Int_stable_def) ``` hoelzl@42988 ` 852` ``` show "space P.G \ sets P.G" ``` hoelzl@42988 ` 853` ``` using M'.top by (simp add: product_algebra_generator_def) ``` hoelzl@42988 ` 854` ``` show "space ?D' = space P.G" "sets ?D' = sets (sigma P.G)" ``` hoelzl@42988 ` 855` ``` by (simp_all add: product_algebra_def product_algebra_generator_def sets_sigma) ``` hoelzl@42988 ` 856` ``` show "space P.P = space P.G" "sets P.P = sets (sigma P.G)" ``` hoelzl@42988 ` 857` ``` by (simp_all add: product_algebra_def) ``` hoelzl@42988 ` 858` ``` show "A \ sets (sigma P.G)" ``` hoelzl@42988 ` 859` ``` using `A \ sets P.P` by (simp add: product_algebra_def) ``` hoelzl@43340 ` 860` hoelzl@42988 ` 861` ``` fix E assume E: "E \ sets P.G" ``` hoelzl@42988 ` 862` ``` then have "E \ sets P.P" ``` hoelzl@42988 ` 863` ``` by (simp add: sets_sigma sigma_sets.Basic product_algebra_def) ``` hoelzl@42988 ` 864` ``` then have "D.prob E = distribution ?D E" ``` hoelzl@42988 ` 865` ``` unfolding D.\'_def by simp ``` hoelzl@42988 ` 866` ``` also ``` hoelzl@42988 ` 867` ``` from E obtain F where "E = Pi\<^isub>E I F" and F: "\i. i \ I \ F i \ sets (M' i)" ``` hoelzl@42988 ` 868` ``` by (auto simp: product_algebra_generator_def) ``` hoelzl@42988 ` 869` ``` with `I \ {}` have "distribution ?D E = prob (\i\I. X i -` F i \ space M)" ``` hoelzl@42988 ` 870` ``` using `I \ {}` by (auto intro!: arg_cong[where f=prob] simp: Pi_iff distribution_def) ``` hoelzl@42988 ` 871` ``` also have "\ = (\i\I. prob (X i -` F i \ space M))" ``` hoelzl@42989 ` 872` ``` using `indep_vars M' X I` I F by (rule indep_varsD) ``` hoelzl@42988 ` 873` ``` also have "\ = P.prob E" ``` hoelzl@42988 ` 874` ``` using F by (simp add: `E = Pi\<^isub>E I F` P.prob_times M'.\'_def distribution_def) ``` hoelzl@42988 ` 875` ``` finally show "D.prob E = P.prob E" . ``` hoelzl@42988 ` 876` ``` qed ``` hoelzl@42988 ` 877` ``` ultimately show "distribution ?D A = P.prob A" ``` hoelzl@42988 ` 878` ``` by (simp add: D.\'_def) ``` hoelzl@42988 ` 879` ``` next ``` hoelzl@42988 ` 880` ``` assume eq: "\A\sets P.P. distribution ?D A = P.prob A" ``` hoelzl@42988 ` 881` ``` have [simp]: "\i. sigma (M' i) = M' i" ``` hoelzl@42988 ` 882` ``` using rv by (intro sigma_algebra.sigma_eq) simp ``` hoelzl@42989 ` 883` ``` have "indep_vars (\i. sigma (M' i)) X I" ``` hoelzl@42989 ` 884` ``` proof (subst indep_vars_finite[OF I]) ``` hoelzl@42988 ` 885` ``` fix i assume [simp]: "i \ I" ``` hoelzl@42988 ` 886` ``` show "random_variable (sigma (M' i)) (X i)" ``` hoelzl@42988 ` 887` ``` using rv[of i] by simp ``` hoelzl@42988 ` 888` ``` show "Int_stable (M' i)" "space (M' i) \ sets (M' i)" ``` hoelzl@42988 ` 889` ``` using M'.Int[of _ i] M'.top by (auto simp: Int_stable_def) ``` hoelzl@42988 ` 890` ``` next ``` hoelzl@42988 ` 891` ``` show "\A\\ i\I. sets (M' i). prob (\j\I. X j -` A j \ space M) = (\j\I. prob (X j -` A j \ space M))" ``` hoelzl@42988 ` 892` ``` proof ``` hoelzl@42988 ` 893` ``` fix A assume A: "A \ (\ i\I. sets (M' i))" ``` hoelzl@42988 ` 894` ``` then have A_in_P: "(Pi\<^isub>E I A) \ sets P.P" ``` hoelzl@42988 ` 895` ``` by (auto intro!: product_algebraI) ``` hoelzl@42988 ` 896` ``` have "prob (\j\I. X j -` A j \ space M) = distribution ?D (Pi\<^isub>E I A)" ``` hoelzl@42988 ` 897` ``` using `I \ {}`by (auto intro!: arg_cong[where f=prob] simp: Pi_iff distribution_def) ``` hoelzl@42988 ` 898` ``` also have "\ = P.prob (Pi\<^isub>E I A)" using A_in_P eq by simp ``` hoelzl@42988 ` 899` ``` also have "\ = (\i\I. M'.prob i (A i))" ``` hoelzl@42988 ` 900` ``` using A by (intro P.prob_times) auto ``` hoelzl@42988 ` 901` ``` also have "\ = (\i\I. prob (X i -` A i \ space M))" ``` hoelzl@42988 ` 902` ``` using A by (auto intro!: setprod_cong simp: M'.\'_def Pi_iff distribution_def) ``` hoelzl@42988 ` 903` ``` finally show "prob (\j\I. X j -` A j \ space M) = (\j\I. prob (X j -` A j \ space M))" . ``` hoelzl@42988 ` 904` ``` qed ``` hoelzl@42988 ` 905` ``` qed ``` hoelzl@42989 ` 906` ``` then show "indep_vars M' X I" ``` hoelzl@42988 ` 907` ``` by simp ``` hoelzl@42988 ` 908` ``` qed ``` hoelzl@42987 ` 909` ```qed ``` hoelzl@42987 ` 910` hoelzl@42989 ` 911` ```lemma (in prob_space) indep_varD: ``` hoelzl@42989 ` 912` ``` assumes indep: "indep_var Ma A Mb B" ``` hoelzl@42989 ` 913` ``` assumes sets: "Xa \ sets Ma" "Xb \ sets Mb" ``` hoelzl@42989 ` 914` ``` shows "prob ((\x. (A x, B x)) -` (Xa \ Xb) \ space M) = ``` hoelzl@42989 ` 915` ``` prob (A -` Xa \ space M) * prob (B -` Xb \ space M)" ``` hoelzl@42989 ` 916` ```proof - ``` hoelzl@42989 ` 917` ``` have "prob ((\x. (A x, B x)) -` (Xa \ Xb) \ space M) = ``` hoelzl@42989 ` 918` ``` prob (\i\UNIV. (bool_case A B i -` bool_case Xa Xb i \ space M))" ``` hoelzl@42989 ` 919` ``` by (auto intro!: arg_cong[where f=prob] simp: UNIV_bool) ``` hoelzl@42989 ` 920` ``` also have "\ = (\i\UNIV. prob (bool_case A B i -` bool_case Xa Xb i \ space M))" ``` hoelzl@42989 ` 921` ``` using indep unfolding indep_var_def ``` hoelzl@42989 ` 922` ``` by (rule indep_varsD) (auto split: bool.split intro: sets) ``` hoelzl@42989 ` 923` ``` also have "\ = prob (A -` Xa \ space M) * prob (B -` Xb \ space M)" ``` hoelzl@42989 ` 924` ``` unfolding UNIV_bool by simp ``` hoelzl@42989 ` 925` ``` finally show ?thesis . ``` hoelzl@42989 ` 926` ```qed ``` hoelzl@42989 ` 927` hoelzl@43340 ` 928` ```lemma (in prob_space) ``` hoelzl@43340 ` 929` ``` assumes "indep_var S X T Y" ``` hoelzl@43340 ` 930` ``` shows indep_var_rv1: "random_variable S X" ``` hoelzl@43340 ` 931` ``` and indep_var_rv2: "random_variable T Y" ``` hoelzl@43340 ` 932` ```proof - ``` hoelzl@43340 ` 933` ``` have "\i\UNIV. random_variable (bool_case S T i) (bool_case X Y i)" ``` hoelzl@43340 ` 934` ``` using assms unfolding indep_var_def indep_vars_def by auto ``` hoelzl@43340 ` 935` ``` then show "random_variable S X" "random_variable T Y" ``` hoelzl@43340 ` 936` ``` unfolding UNIV_bool by auto ``` hoelzl@43340 ` 937` ```qed ``` hoelzl@43340 ` 938` hoelzl@42989 ` 939` ```lemma (in prob_space) indep_var_distributionD: ``` hoelzl@43340 ` 940` ``` assumes indep: "indep_var S X T Y" ``` hoelzl@43920 ` 941` ``` defines "P \ S\measure := ereal\distribution X\ \\<^isub>M T\measure := ereal\distribution Y\" ``` hoelzl@43340 ` 942` ``` assumes "A \ sets P" ``` hoelzl@43340 ` 943` ``` shows "joint_distribution X Y A = finite_measure.\' P A" ``` hoelzl@43340 ` 944` ```proof - ``` hoelzl@43340 ` 945` ``` from indep have rvs: "random_variable S X" "random_variable T Y" ``` hoelzl@43340 ` 946` ``` by (blast dest: indep_var_rv1 indep_var_rv2)+ ``` hoelzl@43340 ` 947` hoelzl@43920 ` 948` ``` let ?S = "S\measure := ereal\distribution X\" ``` hoelzl@43920 ` 949` ``` let ?T = "T\measure := ereal\distribution Y\" ``` hoelzl@43340 ` 950` ``` interpret X: prob_space ?S by (rule distribution_prob_space) fact ``` hoelzl@43340 ` 951` ``` interpret Y: prob_space ?T by (rule distribution_prob_space) fact ``` hoelzl@43340 ` 952` ``` interpret XY: pair_prob_space ?S ?T by default ``` hoelzl@43340 ` 953` hoelzl@43920 ` 954` ``` let ?J = "XY.P\ measure := ereal \ joint_distribution X Y \" ``` hoelzl@43340 ` 955` ``` interpret J: prob_space ?J ``` hoelzl@43340 ` 956` ``` by (rule joint_distribution_prob_space) (simp_all add: rvs) ``` hoelzl@43340 ` 957` hoelzl@43920 ` 958` ``` have "finite_measure.\' (XY.P\ measure := ereal \ joint_distribution X Y \) A = XY.\' A" ``` hoelzl@43340 ` 959` ``` proof (rule prob_space_unique_Int_stable) ``` hoelzl@43340 ` 960` ``` show "Int_stable (pair_measure_generator ?S ?T)" (is "Int_stable ?P") ``` hoelzl@43340 ` 961` ``` by fact ``` hoelzl@43340 ` 962` ``` show "space ?P \ sets ?P" ``` hoelzl@43340 ` 963` ``` unfolding space_pair_measure[simplified pair_measure_def space_sigma] ``` hoelzl@43340 ` 964` ``` using X.top Y.top by (auto intro!: pair_measure_generatorI) ``` hoelzl@43340 ` 965` hoelzl@45777 ` 966` ``` show "prob_space ?J" by unfold_locales ``` hoelzl@43340 ` 967` ``` show "space ?J = space ?P" ``` hoelzl@43340 ` 968` ``` by (simp add: pair_measure_generator_def space_pair_measure) ``` hoelzl@43340 ` 969` ``` show "sets ?J = sets (sigma ?P)" ``` hoelzl@43340 ` 970` ``` by (simp add: pair_measure_def) ``` hoelzl@43340 ` 971` hoelzl@45777 ` 972` ``` show "prob_space XY.P" by unfold_locales ``` hoelzl@43340 ` 973` ``` show "space XY.P = space ?P" "sets XY.P = sets (sigma ?P)" ``` hoelzl@43340 ` 974` ``` by (simp_all add: pair_measure_generator_def pair_measure_def) ``` hoelzl@43340 ` 975` hoelzl@43340 ` 976` ``` show "A \ sets (sigma ?P)" ``` hoelzl@43340 ` 977` ``` using `A \ sets P` unfolding P_def pair_measure_def by simp ``` hoelzl@43340 ` 978` hoelzl@43340 ` 979` ``` fix X assume "X \ sets ?P" ``` hoelzl@43340 ` 980` ``` then obtain A B where "A \ sets S" "B \ sets T" "X = A \ B" ``` hoelzl@43340 ` 981` ``` by (auto simp: sets_pair_measure_generator) ``` hoelzl@43340 ` 982` ``` then show "J.\' X = XY.\' X" ``` hoelzl@43340 ` 983` ``` unfolding J.\'_def XY.\'_def using indep ``` hoelzl@43340 ` 984` ``` by (simp add: XY.pair_measure_times) ``` hoelzl@43340 ` 985` ``` (simp add: distribution_def indep_varD) ``` hoelzl@43340 ` 986` ``` qed ``` hoelzl@43340 ` 987` ``` then show ?thesis ``` hoelzl@43340 ` 988` ``` using `A \ sets P` unfolding P_def J.\'_def XY.\'_def by simp ``` hoelzl@43340 ` 989` ```qed ``` hoelzl@42989 ` 990` hoelzl@42861 ` 991` ```end ```