# Theory Independent_Family

Up to index of Isabelle/HOL/HOL-Multivariate_Analysis/HOL-Probability

theory Independent_Family
imports Infinite_Product_Measure
`(*  Title:      HOL/Probability/Independent_Family.thy    Author:     Johannes Hölzl, TU München*)header {* Independent families of events, event sets, and random variables *}theory Independent_Family  imports Probability_Measure Infinite_Product_Measurebegindefinition (in prob_space)  "indep_sets F I <-> (∀i∈I. F i ⊆ events) ∧    (∀J⊆I. J ≠ {} --> finite J --> (∀A∈Pi J F. prob (\<Inter>j∈J. A j) = (∏j∈J. prob (A j))))"definition (in prob_space)  "indep_set A B <-> indep_sets (bool_case A B) UNIV"definition (in prob_space)  indep_events_def_alt: "indep_events A I <-> indep_sets (λi. {A i}) I"lemma (in prob_space) indep_events_def:  "indep_events A I <-> (A`I ⊆ events) ∧    (∀J⊆I. J ≠ {} --> finite J --> prob (\<Inter>j∈J. A j) = (∏j∈J. prob (A j)))"  unfolding indep_events_def_alt indep_sets_def  apply (simp add: Ball_def Pi_iff image_subset_iff_funcset)  apply (intro conj_cong refl arg_cong[where f=All] ext imp_cong)  apply auto  donedefinition (in prob_space)  "indep_event A B <-> indep_events (bool_case A B) UNIV"lemma (in prob_space) indep_sets_cong:  "I = J ==> (!!i. i ∈ I ==> F i = G i) ==> indep_sets F I <-> indep_sets G J"  by (simp add: indep_sets_def, intro conj_cong all_cong imp_cong ball_cong) blast+lemma (in prob_space) indep_events_finite_index_events:  "indep_events F I <-> (∀J⊆I. J ≠ {} --> finite J --> indep_events F J)"  by (auto simp: indep_events_def)lemma (in prob_space) indep_sets_finite_index_sets:  "indep_sets F I <-> (∀J⊆I. J ≠ {} --> finite J --> indep_sets F J)"proof (intro iffI allI impI)  assume *: "∀J⊆I. J ≠ {} --> finite J --> indep_sets F J"  show "indep_sets F I" unfolding indep_sets_def  proof (intro conjI ballI allI impI)    fix i assume "i ∈ I"    with *[THEN spec, of "{i}"] show "F i ⊆ events"      by (auto simp: indep_sets_def)  qed (insert *, auto simp: indep_sets_def)qed (auto simp: indep_sets_def)lemma (in prob_space) indep_sets_mono_index:  "J ⊆ I ==> indep_sets F I ==> indep_sets F J"  unfolding indep_sets_def by autolemma (in prob_space) indep_sets_mono_sets:  assumes indep: "indep_sets F I"  assumes mono: "!!i. i∈I ==> G i ⊆ F i"  shows "indep_sets G I"proof -  have "(∀i∈I. F i ⊆ events) ==> (∀i∈I. G i ⊆ events)"    using mono by auto  moreover have "!!A J. J ⊆ I ==> A ∈ (Π j∈J. G j) ==> A ∈ (Π j∈J. F j)"    using mono by (auto simp: Pi_iff)  ultimately show ?thesis    using indep by (auto simp: indep_sets_def)qedlemma (in prob_space) indep_sets_mono:  assumes indep: "indep_sets F I"  assumes mono: "J ⊆ I" "!!i. i∈J ==> G i ⊆ F i"  shows "indep_sets G J"  apply (rule indep_sets_mono_sets)  apply (rule indep_sets_mono_index)  apply (fact +)  donelemma (in prob_space) indep_setsI:  assumes "!!i. i ∈ I ==> F i ⊆ events"    and "!!A J. J ≠ {} ==> J ⊆ I ==> finite J ==> (∀j∈J. A j ∈ F j) ==> prob (\<Inter>j∈J. A j) = (∏j∈J. prob (A j))"  shows "indep_sets F I"  using assms unfolding indep_sets_def by (auto simp: Pi_iff)lemma (in prob_space) indep_setsD:  assumes "indep_sets F I" and "J ⊆ I" "J ≠ {}" "finite J" "∀j∈J. A j ∈ F j"  shows "prob (\<Inter>j∈J. A j) = (∏j∈J. prob (A j))"  using assms unfolding indep_sets_def by autolemma (in prob_space) indep_setI:  assumes ev: "A ⊆ events" "B ⊆ events"    and indep: "!!a b. a ∈ A ==> b ∈ B ==> prob (a ∩ b) = prob a * prob b"  shows "indep_set A B"  unfolding indep_set_defproof (rule indep_setsI)  fix F J assume "J ≠ {}" "J ⊆ UNIV"    and F: "∀j∈J. F j ∈ (case j of True => A | False => B)"  have "J ∈ Pow UNIV" by auto  with F `J ≠ {}` indep[of "F True" "F False"]  show "prob (\<Inter>j∈J. F j) = (∏j∈J. prob (F j))"    unfolding UNIV_bool Pow_insert by (auto simp: ac_simps)qed (auto split: bool.split simp: ev)lemma (in prob_space) indep_setD:  assumes indep: "indep_set A B" and ev: "a ∈ A" "b ∈ B"  shows "prob (a ∩ b) = prob a * prob b"  using indep[unfolded indep_set_def, THEN indep_setsD, of UNIV "bool_case a b"] ev  by (simp add: ac_simps UNIV_bool)lemma (in prob_space)  assumes indep: "indep_set A B"  shows indep_setD_ev1: "A ⊆ events"    and indep_setD_ev2: "B ⊆ events"  using indep unfolding indep_set_def indep_sets_def UNIV_bool by autolemma (in prob_space) indep_sets_dynkin:  assumes indep: "indep_sets F I"  shows "indep_sets (λi. dynkin (space M) (F i)) I"    (is "indep_sets ?F I")proof (subst indep_sets_finite_index_sets, intro allI impI ballI)  fix J assume "finite J" "J ⊆ I" "J ≠ {}"  with indep have "indep_sets F J"    by (subst (asm) indep_sets_finite_index_sets) auto  { fix J K assume "indep_sets F K"    let ?G = "λS i. if i ∈ S then ?F i else F i"    assume "finite J" "J ⊆ K"    then have "indep_sets (?G J) K"    proof induct      case (insert j J)      moreover def G ≡ "?G J"      ultimately have G: "indep_sets G K" "!!i. i ∈ K ==> G i ⊆ events" and "j ∈ K"        by (auto simp: indep_sets_def)      let ?D = "{E∈events. indep_sets (G(j := {E})) K }"      { fix X assume X: "X ∈ events"        assume indep: "!!J A. J ≠ {} ==> J ⊆ K ==> finite J ==> j ∉ J ==> (∀i∈J. A i ∈ G i)          ==> prob ((\<Inter>i∈J. A i) ∩ X) = prob X * (∏i∈J. prob (A i))"        have "indep_sets (G(j := {X})) K"        proof (rule indep_setsI)          fix i assume "i ∈ K" then show "(G(j:={X})) i ⊆ events"            using G X by auto        next          fix A J assume J: "J ≠ {}" "J ⊆ K" "finite J" "∀i∈J. A i ∈ (G(j := {X})) i"          show "prob (\<Inter>j∈J. A j) = (∏j∈J. prob (A j))"          proof cases            assume "j ∈ J"            with J have "A j = X" by auto            show ?thesis            proof cases              assume "J = {j}" then show ?thesis by simp            next              assume "J ≠ {j}"              have "prob (\<Inter>i∈J. A i) = prob ((\<Inter>i∈J-{j}. A i) ∩ X)"                using `j ∈ J` `A j = X` by (auto intro!: arg_cong[where f=prob] split: split_if_asm)              also have "… = prob X * (∏i∈J-{j}. prob (A i))"              proof (rule indep)                show "J - {j} ≠ {}" "J - {j} ⊆ K" "finite (J - {j})" "j ∉ J - {j}"                  using J `J ≠ {j}` `j ∈ J` by auto                show "∀i∈J - {j}. A i ∈ G i"                  using J by auto              qed              also have "… = prob (A j) * (∏i∈J-{j}. prob (A i))"                using `A j = X` by simp              also have "… = (∏i∈J. prob (A i))"                unfolding setprod.insert_remove[OF `finite J`, symmetric, of "λi. prob  (A i)"]                using `j ∈ J` by (simp add: insert_absorb)              finally show ?thesis .            qed          next            assume "j ∉ J"            with J have "∀i∈J. A i ∈ G i" by (auto split: split_if_asm)            with J show ?thesis              by (intro indep_setsD[OF G(1)]) auto          qed        qed }      note indep_sets_insert = this      have "dynkin_system (space M) ?D"      proof (rule dynkin_systemI', simp_all cong del: indep_sets_cong, safe)        show "indep_sets (G(j := {{}})) K"          by (rule indep_sets_insert) auto      next        fix X assume X: "X ∈ events" and G': "indep_sets (G(j := {X})) K"        show "indep_sets (G(j := {space M - X})) K"        proof (rule indep_sets_insert)          fix J A assume J: "J ≠ {}" "J ⊆ K" "finite J" "j ∉ J" and A: "∀i∈J. A i ∈ G i"          then have A_sets: "!!i. i∈J ==> A i ∈ events"            using G by auto          have "prob ((\<Inter>j∈J. A j) ∩ (space M - X)) =              prob ((\<Inter>j∈J. A j) - (\<Inter>i∈insert j J. (A(j := X)) i))"            using A_sets sets.sets_into_space[of _ M] X `J ≠ {}`            by (auto intro!: arg_cong[where f=prob] split: split_if_asm)          also have "… = prob (\<Inter>j∈J. A j) - prob (\<Inter>i∈insert j J. (A(j := X)) i)"            using J `J ≠ {}` `j ∉ J` A_sets X sets.sets_into_space            by (auto intro!: finite_measure_Diff sets.finite_INT split: split_if_asm)          finally have "prob ((\<Inter>j∈J. A j) ∩ (space M - X)) =              prob (\<Inter>j∈J. A j) - prob (\<Inter>i∈insert j J. (A(j := X)) i)" .          moreover {            have "prob (\<Inter>j∈J. A j) = (∏j∈J. prob (A j))"              using J A `finite J` by (intro indep_setsD[OF G(1)]) auto            then have "prob (\<Inter>j∈J. A j) = prob (space M) * (∏i∈J. prob (A i))"              using prob_space by simp }          moreover {            have "prob (\<Inter>i∈insert j J. (A(j := X)) i) = (∏i∈insert j J. prob ((A(j := X)) i))"              using J A `j ∈ K` by (intro indep_setsD[OF G']) auto            then have "prob (\<Inter>i∈insert j J. (A(j := X)) i) = prob X * (∏i∈J. prob (A i))"              using `finite J` `j ∉ J` by (auto intro!: setprod_cong) }          ultimately have "prob ((\<Inter>j∈J. A j) ∩ (space M - X)) = (prob (space M) - prob X) * (∏i∈J. prob (A i))"            by (simp add: field_simps)          also have "… = prob (space M - X) * (∏i∈J. prob (A i))"            using X A by (simp add: finite_measure_compl)          finally show "prob ((\<Inter>j∈J. A j) ∩ (space M - X)) = prob (space M - X) * (∏i∈J. prob (A i))" .        qed (insert X, auto)      next        fix F :: "nat => 'a set" assume disj: "disjoint_family F" and "range F ⊆ ?D"        then have F: "!!i. F i ∈ events" "!!i. indep_sets (G(j:={F i})) K" by auto        show "indep_sets (G(j := {\<Union>k. F k})) K"        proof (rule indep_sets_insert)          fix J A assume J: "j ∉ J" "J ≠ {}" "J ⊆ K" "finite J" and A: "∀i∈J. A i ∈ G i"          then have A_sets: "!!i. i∈J ==> A i ∈ events"            using G by auto          have "prob ((\<Inter>j∈J. A j) ∩ (\<Union>k. F k)) = prob (\<Union>k. (\<Inter>i∈insert j J. (A(j := F k)) i))"            using `J ≠ {}` `j ∉ J` `j ∈ K` by (auto intro!: arg_cong[where f=prob] split: split_if_asm)          moreover have "(λk. prob (\<Inter>i∈insert j J. (A(j := F k)) i)) sums prob (\<Union>k. (\<Inter>i∈insert j J. (A(j := F k)) i))"          proof (rule finite_measure_UNION)            show "disjoint_family (λk. \<Inter>i∈insert j J. (A(j := F k)) i)"              using disj by (rule disjoint_family_on_bisimulation) auto            show "range (λk. \<Inter>i∈insert j J. (A(j := F k)) i) ⊆ events"              using A_sets F `finite J` `J ≠ {}` `j ∉ J` by (auto intro!: sets.Int)          qed          moreover { fix k            from J A `j ∈ K` have "prob (\<Inter>i∈insert j J. (A(j := F k)) i) = prob (F k) * (∏i∈J. prob (A i))"              by (subst indep_setsD[OF F(2)]) (auto intro!: setprod_cong split: split_if_asm)            also have "… = prob (F k) * prob (\<Inter>i∈J. A i)"              using J A `j ∈ K` by (subst indep_setsD[OF G(1)]) auto            finally have "prob (\<Inter>i∈insert j J. (A(j := F k)) i) = prob (F k) * prob (\<Inter>i∈J. A i)" . }          ultimately have "(λk. prob (F k) * prob (\<Inter>i∈J. A i)) sums (prob ((\<Inter>j∈J. A j) ∩ (\<Union>k. F k)))"            by simp          moreover          have "(λk. prob (F k) * prob (\<Inter>i∈J. A i)) sums (prob (\<Union>k. F k) * prob (\<Inter>i∈J. A i))"            using disj F(1) by (intro finite_measure_UNION sums_mult2) auto          then have "(λk. prob (F k) * prob (\<Inter>i∈J. A i)) sums (prob (\<Union>k. F k) * (∏i∈J. prob (A i)))"            using J A `j ∈ K` by (subst indep_setsD[OF G(1), symmetric]) auto          ultimately          show "prob ((\<Inter>j∈J. A j) ∩ (\<Union>k. F k)) = prob (\<Union>k. F k) * (∏j∈J. prob (A j))"            by (auto dest!: sums_unique)        qed (insert F, auto)      qed (insert sets.sets_into_space, auto)      then have mono: "dynkin (space M) (G j) ⊆ {E ∈ events. indep_sets (G(j := {E})) K}"      proof (rule dynkin_system.dynkin_subset, safe)        fix X assume "X ∈ G j"        then show "X ∈ events" using G `j ∈ K` by auto        from `indep_sets G K`        show "indep_sets (G(j := {X})) K"          by (rule indep_sets_mono_sets) (insert `X ∈ G j`, auto)      qed      have "indep_sets (G(j:=?D)) K"      proof (rule indep_setsI)        fix i assume "i ∈ K" then show "(G(j := ?D)) i ⊆ events"          using G(2) by auto      next        fix A J assume J: "J≠{}" "J ⊆ K" "finite J" and A: "∀i∈J. A i ∈ (G(j := ?D)) i"        show "prob (\<Inter>j∈J. A j) = (∏j∈J. prob (A j))"        proof cases          assume "j ∈ J"          with A have indep: "indep_sets (G(j := {A j})) K" by auto          from J A show ?thesis            by (intro indep_setsD[OF indep]) auto        next          assume "j ∉ J"          with J A have "∀i∈J. A i ∈ G i" by (auto split: split_if_asm)          with J show ?thesis            by (intro indep_setsD[OF G(1)]) auto        qed      qed      then have "indep_sets (G(j := dynkin (space M) (G j))) K"        by (rule indep_sets_mono_sets) (insert mono, auto)      then show ?case        by (rule indep_sets_mono_sets) (insert `j ∈ K` `j ∉ J`, auto simp: G_def)    qed (insert `indep_sets F K`, simp) }  from this[OF `indep_sets F J` `finite J` subset_refl]  show "indep_sets ?F J"    by (rule indep_sets_mono_sets) autoqedlemma (in prob_space) indep_sets_sigma:  assumes indep: "indep_sets F I"  assumes stable: "!!i. i ∈ I ==> Int_stable (F i)"  shows "indep_sets (λi. sigma_sets (space M) (F i)) I"proof -  from indep_sets_dynkin[OF indep]  show ?thesis  proof (rule indep_sets_mono_sets, subst sigma_eq_dynkin, simp_all add: stable)    fix i assume "i ∈ I"    with indep have "F i ⊆ events" by (auto simp: indep_sets_def)    with sets.sets_into_space show "F i ⊆ Pow (space M)" by auto  qedqedlemma (in prob_space) indep_sets_sigma_sets_iff:  assumes "!!i. i ∈ I ==> Int_stable (F i)"  shows "indep_sets (λi. sigma_sets (space M) (F i)) I <-> indep_sets F I"proof  assume "indep_sets F I" then show "indep_sets (λi. sigma_sets (space M) (F i)) I"    by (rule indep_sets_sigma) factnext  assume "indep_sets (λi. sigma_sets (space M) (F i)) I" then show "indep_sets F I"    by (rule indep_sets_mono_sets) (intro subsetI sigma_sets.Basic)qeddefinition (in prob_space)  indep_vars_def2: "indep_vars M' X I <->    (∀i∈I. random_variable (M' i) (X i)) ∧    indep_sets (λi. { X i -` A ∩ space M | A. A ∈ sets (M' i)}) I"definition (in prob_space)  "indep_var Ma A Mb B <-> indep_vars (bool_case Ma Mb) (bool_case A B) UNIV"lemma (in prob_space) indep_vars_def:  "indep_vars M' X I <->    (∀i∈I. random_variable (M' i) (X i)) ∧    indep_sets (λi. sigma_sets (space M) { X i -` A ∩ space M | A. A ∈ sets (M' i)}) I"  unfolding indep_vars_def2  apply (rule conj_cong[OF refl])  apply (rule indep_sets_sigma_sets_iff[symmetric])  apply (auto simp: Int_stable_def)  apply (rule_tac x="A ∩ Aa" in exI)  apply auto  donelemma (in prob_space) indep_var_eq:  "indep_var S X T Y <->    (random_variable S X ∧ random_variable T Y) ∧    indep_set      (sigma_sets (space M) { X -` A ∩ space M | A. A ∈ sets S})      (sigma_sets (space M) { Y -` A ∩ space M | A. A ∈ sets T})"  unfolding indep_var_def indep_vars_def indep_set_def UNIV_bool  by (intro arg_cong2[where f="op ∧"] arg_cong2[where f=indep_sets] ext)     (auto split: bool.split)lemma (in prob_space) indep_sets2_eq:  "indep_set A B <-> A ⊆ events ∧ B ⊆ events ∧ (∀a∈A. ∀b∈B. prob (a ∩ b) = prob a * prob b)"  unfolding indep_set_defproof (intro iffI ballI conjI)  assume indep: "indep_sets (bool_case A B) UNIV"  { fix a b assume "a ∈ A" "b ∈ B"    with indep_setsD[OF indep, of UNIV "bool_case a b"]    show "prob (a ∩ b) = prob a * prob b"      unfolding UNIV_bool by (simp add: ac_simps) }  from indep show "A ⊆ events" "B ⊆ events"    unfolding indep_sets_def UNIV_bool by autonext  assume *: "A ⊆ events ∧ B ⊆ events ∧ (∀a∈A. ∀b∈B. prob (a ∩ b) = prob a * prob b)"  show "indep_sets (bool_case A B) UNIV"  proof (rule indep_setsI)    fix i show "(case i of True => A | False => B) ⊆ events"      using * by (auto split: bool.split)  next    fix J X assume "J ≠ {}" "J ⊆ UNIV" and X: "∀j∈J. X j ∈ (case j of True => A | False => B)"    then have "J = {True} ∨ J = {False} ∨ J = {True,False}"      by (auto simp: UNIV_bool)    then show "prob (\<Inter>j∈J. X j) = (∏j∈J. prob (X j))"      using X * by auto  qedqedlemma (in prob_space) indep_set_sigma_sets:  assumes "indep_set A B"  assumes A: "Int_stable A" and B: "Int_stable B"  shows "indep_set (sigma_sets (space M) A) (sigma_sets (space M) B)"proof -  have "indep_sets (λi. sigma_sets (space M) (case i of True => A | False => B)) UNIV"  proof (rule indep_sets_sigma)    show "indep_sets (bool_case A B) UNIV"      by (rule `indep_set A B`[unfolded indep_set_def])    fix i show "Int_stable (case i of True => A | False => B)"      using A B by (cases i) auto  qed  then show ?thesis    unfolding indep_set_def    by (rule indep_sets_mono_sets) (auto split: bool.split)qedlemma (in prob_space) indep_sets_collect_sigma:  fixes I :: "'j => 'i set" and J :: "'j set" and E :: "'i => 'a set set"  assumes indep: "indep_sets E (\<Union>j∈J. I j)"  assumes Int_stable: "!!i j. j ∈ J ==> i ∈ I j ==> Int_stable (E i)"  assumes disjoint: "disjoint_family_on I J"  shows "indep_sets (λj. sigma_sets (space M) (\<Union>i∈I j. E i)) J"proof -  let ?E = "λj. {\<Inter>k∈K. E' k| E' K. finite K ∧ K ≠ {} ∧ K ⊆ I j ∧ (∀k∈K. E' k ∈ E k) }"  from indep have E: "!!j i. j ∈ J ==> i ∈ I j ==> E i ⊆ events"    unfolding indep_sets_def by auto  { fix j    let ?S = "sigma_sets (space M) (\<Union>i∈I j. E i)"    assume "j ∈ J"    from E[OF this] interpret S: sigma_algebra "space M" ?S      using sets.sets_into_space[of _ M] by (intro sigma_algebra_sigma_sets) auto    have "sigma_sets (space M) (\<Union>i∈I j. E i) = sigma_sets (space M) (?E j)"    proof (rule sigma_sets_eqI)      fix A assume "A ∈ (\<Union>i∈I j. E i)"      then guess i ..      then show "A ∈ sigma_sets (space M) (?E j)"        by (auto intro!: sigma_sets.intros(2-) exI[of _ "{i}"] exI[of _ "λi. A"])    next      fix A assume "A ∈ ?E j"      then obtain E' K where "finite K" "K ≠ {}" "K ⊆ I j" "!!k. k ∈ K ==> E' k ∈ E k"        and A: "A = (\<Inter>k∈K. E' k)"        by auto      then have "A ∈ ?S" unfolding A        by (safe intro!: S.finite_INT) auto      then show "A ∈ sigma_sets (space M) (\<Union>i∈I j. E i)"        by simp    qed }  moreover have "indep_sets (λj. sigma_sets (space M) (?E j)) J"  proof (rule indep_sets_sigma)    show "indep_sets ?E J"    proof (intro indep_setsI)      fix j assume "j ∈ J" with E show "?E j ⊆ events" by (force  intro!: sets.finite_INT)    next      fix K A assume K: "K ≠ {}" "K ⊆ J" "finite K"        and "∀j∈K. A j ∈ ?E j"      then have "∀j∈K. ∃E' L. A j = (\<Inter>l∈L. E' l) ∧ finite L ∧ L ≠ {} ∧ L ⊆ I j ∧ (∀l∈L. E' l ∈ E l)"        by simp      from bchoice[OF this] guess E' ..      from bchoice[OF this] obtain L        where A: "!!j. j∈K ==> A j = (\<Inter>l∈L j. E' j l)"        and L: "!!j. j∈K ==> finite (L j)" "!!j. j∈K ==> L j ≠ {}" "!!j. j∈K ==> L j ⊆ I j"        and E': "!!j l. j∈K ==> l ∈ L j ==> E' j l ∈ E l"        by auto      { fix k l j assume "k ∈ K" "j ∈ K" "l ∈ L j" "l ∈ L k"        have "k = j"        proof (rule ccontr)          assume "k ≠ j"          with disjoint `K ⊆ J` `k ∈ K` `j ∈ K` have "I k ∩ I j = {}"            unfolding disjoint_family_on_def by auto          with L(2,3)[OF `j ∈ K`] L(2,3)[OF `k ∈ K`]          show False using `l ∈ L k` `l ∈ L j` by auto        qed }      note L_inj = this      def k ≡ "λl. (SOME k. k ∈ K ∧ l ∈ L k)"      { fix x j l assume *: "j ∈ K" "l ∈ L j"        have "k l = j" unfolding k_def        proof (rule some_equality)          fix k assume "k ∈ K ∧ l ∈ L k"          with * L_inj show "k = j" by auto        qed (insert *, simp) }      note k_simp[simp] = this      let ?E' = "λl. E' (k l) l"      have "prob (\<Inter>j∈K. A j) = prob (\<Inter>l∈(\<Union>k∈K. L k). ?E' l)"        by (auto simp: A intro!: arg_cong[where f=prob])      also have "… = (∏l∈(\<Union>k∈K. L k). prob (?E' l))"        using L K E' by (intro indep_setsD[OF indep]) (simp_all add: UN_mono)      also have "… = (∏j∈K. ∏l∈L j. prob (E' j l))"        using K L L_inj by (subst setprod_UN_disjoint) auto      also have "… = (∏j∈K. prob (A j))"        using K L E' by (auto simp add: A intro!: setprod_cong indep_setsD[OF indep, symmetric]) blast      finally show "prob (\<Inter>j∈K. A j) = (∏j∈K. prob (A j))" .    qed  next    fix j assume "j ∈ J"    show "Int_stable (?E j)"    proof (rule Int_stableI)      fix a assume "a ∈ ?E j" then obtain Ka Ea        where a: "a = (\<Inter>k∈Ka. Ea k)" "finite Ka" "Ka ≠ {}" "Ka ⊆ I j" "!!k. k∈Ka ==> Ea k ∈ E k" by auto      fix b assume "b ∈ ?E j" then obtain Kb Eb        where b: "b = (\<Inter>k∈Kb. Eb k)" "finite Kb" "Kb ≠ {}" "Kb ⊆ I j" "!!k. k∈Kb ==> Eb k ∈ E k" by auto      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 {})"      have "a ∩ b = INTER (Ka ∪ Kb) ?A"        by (simp add: a b set_eq_iff) auto      with a b `j ∈ J` Int_stableD[OF Int_stable] show "a ∩ b ∈ ?E j"        by (intro CollectI exI[of _ "Ka ∪ Kb"] exI[of _ ?A]) auto    qed  qed  ultimately show ?thesis    by (simp cong: indep_sets_cong)qeddefinition (in prob_space) tail_events where  "tail_events A = (\<Inter>n. sigma_sets (space M) (UNION {n..} A))"lemma (in prob_space) tail_events_sets:  assumes A: "!!i::nat. A i ⊆ events"  shows "tail_events A ⊆ events"proof  fix X assume X: "X ∈ tail_events A"  let ?A = "(\<Inter>n. sigma_sets (space M) (UNION {n..} A))"  from X have "!!n::nat. X ∈ sigma_sets (space M) (UNION {n..} A)" by (auto simp: tail_events_def)  from this[of 0] have "X ∈ sigma_sets (space M) (UNION UNIV A)" by simp  then show "X ∈ events"    by induct (insert A, auto)qedlemma (in prob_space) sigma_algebra_tail_events:  assumes "!!i::nat. sigma_algebra (space M) (A i)"  shows "sigma_algebra (space M) (tail_events A)"  unfolding tail_events_defproof (simp add: sigma_algebra_iff2, safe)  let ?A = "(\<Inter>n. sigma_sets (space M) (UNION {n..} A))"  interpret A: sigma_algebra "space M" "A i" for i by fact  { fix X x assume "X ∈ ?A" "x ∈ X"    then have "!!n. X ∈ sigma_sets (space M) (UNION {n..} A)" by auto    from this[of 0] have "X ∈ sigma_sets (space M) (UNION UNIV A)" by simp    then have "X ⊆ space M"      by induct (insert A.sets_into_space, auto)    with `x ∈ X` show "x ∈ space M" by auto }  { fix F :: "nat => 'a set" and n assume "range F ⊆ ?A"    then show "(UNION UNIV F) ∈ sigma_sets (space M) (UNION {n..} A)"      by (intro sigma_sets.Union) auto }qed (auto intro!: sigma_sets.Compl sigma_sets.Empty)lemma (in prob_space) kolmogorov_0_1_law:  fixes A :: "nat => 'a set set"  assumes "!!i::nat. sigma_algebra (space M) (A i)"  assumes indep: "indep_sets A UNIV"  and X: "X ∈ tail_events A"  shows "prob X = 0 ∨ prob X = 1"proof -  have A: "!!i. A i ⊆ events"    using indep unfolding indep_sets_def by simp  let ?D = "{D ∈ events. prob (X ∩ D) = prob X * prob D}"  interpret A: sigma_algebra "space M" "A i" for i by fact  interpret T: sigma_algebra "space M" "tail_events A"    by (rule sigma_algebra_tail_events) fact  have "X ⊆ space M" using T.space_closed X by auto  have X_in: "X ∈ events"    using tail_events_sets A X by auto  interpret D: dynkin_system "space M" ?D  proof (rule dynkin_systemI)    fix D assume "D ∈ ?D" then show "D ⊆ space M"      using sets.sets_into_space by auto  next    show "space M ∈ ?D"      using prob_space `X ⊆ space M` by (simp add: Int_absorb2)  next    fix A assume A: "A ∈ ?D"    have "prob (X ∩ (space M - A)) = prob (X - (X ∩ A))"      using `X ⊆ space M` by (auto intro!: arg_cong[where f=prob])    also have "… = prob X - prob (X ∩ A)"      using X_in A by (intro finite_measure_Diff) auto    also have "… = prob X * prob (space M) - prob X * prob A"      using A prob_space by auto    also have "… = prob X * prob (space M - A)"      using X_in A sets.sets_into_space      by (subst finite_measure_Diff) (auto simp: field_simps)    finally show "space M - A ∈ ?D"      using A `X ⊆ space M` by auto  next    fix F :: "nat => 'a set" assume dis: "disjoint_family F" and "range F ⊆ ?D"    then have F: "range F ⊆ events" "!!i. prob (X ∩ F i) = prob X * prob (F i)"      by auto    have "(λi. prob (X ∩ F i)) sums prob (\<Union>i. X ∩ F i)"    proof (rule finite_measure_UNION)      show "range (λi. X ∩ F i) ⊆ events"        using F X_in by auto      show "disjoint_family (λi. X ∩ F i)"        using dis by (rule disjoint_family_on_bisimulation) auto    qed    with F have "(λi. prob X * prob (F i)) sums prob (X ∩ (\<Union>i. F i))"      by simp    moreover have "(λi. prob X * prob (F i)) sums (prob X * prob (\<Union>i. F i))"      by (intro sums_mult finite_measure_UNION F dis)    ultimately have "prob (X ∩ (\<Union>i. F i)) = prob X * prob (\<Union>i. F i)"      by (auto dest!: sums_unique)    with F show "(\<Union>i. F i) ∈ ?D"      by auto  qed  { fix n    have "indep_sets (λb. sigma_sets (space M) (\<Union>m∈bool_case {..n} {Suc n..} b. A m)) UNIV"    proof (rule indep_sets_collect_sigma)      have *: "(\<Union>b. case b of True => {..n} | False => {Suc n..}) = UNIV" (is "?U = _")        by (simp split: bool.split add: set_eq_iff) (metis not_less_eq_eq)      with indep show "indep_sets A ?U" by simp      show "disjoint_family (bool_case {..n} {Suc n..})"        unfolding disjoint_family_on_def by (auto split: bool.split)      fix m      show "Int_stable (A m)"        unfolding Int_stable_def using A.Int by auto    qed    also have "(λb. sigma_sets (space M) (\<Union>m∈bool_case {..n} {Suc n..} b. A m)) =      bool_case (sigma_sets (space M) (\<Union>m∈{..n}. A m)) (sigma_sets (space M) (\<Union>m∈{Suc n..}. A m))"      by (auto intro!: ext split: bool.split)    finally have indep: "indep_set (sigma_sets (space M) (\<Union>m∈{..n}. A m)) (sigma_sets (space M) (\<Union>m∈{Suc n..}. A m))"      unfolding indep_set_def by simp    have "sigma_sets (space M) (\<Union>m∈{..n}. A m) ⊆ ?D"    proof (simp add: subset_eq, rule)      fix D assume D: "D ∈ sigma_sets (space M) (\<Union>m∈{..n}. A m)"      have "X ∈ sigma_sets (space M) (\<Union>m∈{Suc n..}. A m)"        using X unfolding tail_events_def by simp      from indep_setD[OF indep D this] indep_setD_ev1[OF indep] D      show "D ∈ events ∧ prob (X ∩ D) = prob X * prob D"        by (auto simp add: ac_simps)    qed }  then have "(\<Union>n. sigma_sets (space M) (\<Union>m∈{..n}. A m)) ⊆ ?D" (is "?A ⊆ _")    by auto  note `X ∈ tail_events A`  also {    have "!!n. sigma_sets (space M) (\<Union>i∈{n..}. A i) ⊆ sigma_sets (space M) ?A"      by (intro sigma_sets_subseteq UN_mono) auto   then have "tail_events A ⊆ sigma_sets (space M) ?A"      unfolding tail_events_def by auto }  also have "sigma_sets (space M) ?A = dynkin (space M) ?A"  proof (rule sigma_eq_dynkin)    { fix B n assume "B ∈ sigma_sets (space M) (\<Union>m∈{..n}. A m)"      then have "B ⊆ space M"        by induct (insert A sets.sets_into_space[of _ M], auto) }    then show "?A ⊆ Pow (space M)" by auto    show "Int_stable ?A"    proof (rule Int_stableI)      fix a assume "a ∈ ?A" then guess n .. note a = this      fix b assume "b ∈ ?A" then guess m .. note b = this      interpret Amn: sigma_algebra "space M" "sigma_sets (space M) (\<Union>i∈{..max m n}. A i)"        using A sets.sets_into_space[of _ M] by (intro sigma_algebra_sigma_sets) auto      have "sigma_sets (space M) (\<Union>i∈{..n}. A i) ⊆ sigma_sets (space M) (\<Union>i∈{..max m n}. A i)"        by (intro sigma_sets_subseteq UN_mono) auto      with a have "a ∈ sigma_sets (space M) (\<Union>i∈{..max m n}. A i)" by auto      moreover      have "sigma_sets (space M) (\<Union>i∈{..m}. A i) ⊆ sigma_sets (space M) (\<Union>i∈{..max m n}. A i)"        by (intro sigma_sets_subseteq UN_mono) auto      with b have "b ∈ sigma_sets (space M) (\<Union>i∈{..max m n}. A i)" by auto      ultimately have "a ∩ b ∈ sigma_sets (space M) (\<Union>i∈{..max m n}. A i)"        using Amn.Int[of a b] by simp      then show "a ∩ b ∈ (\<Union>n. sigma_sets (space M) (\<Union>i∈{..n}. A i))" by auto    qed  qed  also have "dynkin (space M) ?A ⊆ ?D"    using `?A ⊆ ?D` by (auto intro!: D.dynkin_subset)  finally show ?thesis by autoqedlemma (in prob_space) borel_0_1_law:  fixes F :: "nat => 'a set"  assumes F2: "indep_events F UNIV"  shows "prob (\<Inter>n. \<Union>m∈{n..}. F m) = 0 ∨ prob (\<Inter>n. \<Union>m∈{n..}. F m) = 1"proof (rule kolmogorov_0_1_law[of "λi. sigma_sets (space M) { F i }"])  have F1: "range F ⊆ events"    using F2 by (simp add: indep_events_def subset_eq)  { fix i show "sigma_algebra (space M) (sigma_sets (space M) {F i})"      using sigma_algebra_sigma_sets[of "{F i}" "space M"] F1 sets.sets_into_space      by auto }  show "indep_sets (λi. sigma_sets (space M) {F i}) UNIV"  proof (rule indep_sets_sigma)    show "indep_sets (λi. {F i}) UNIV"      unfolding indep_events_def_alt[symmetric] by fact    fix i show "Int_stable {F i}"      unfolding Int_stable_def by simp  qed  let ?Q = "λn. \<Union>i∈{n..}. F i"  show "(\<Inter>n. \<Union>m∈{n..}. F m) ∈ tail_events (λi. sigma_sets (space M) {F i})"    unfolding tail_events_def  proof    fix j    interpret S: sigma_algebra "space M" "sigma_sets (space M) (\<Union>i∈{j..}. sigma_sets (space M) {F i})"      using order_trans[OF F1 sets.space_closed]      by (intro sigma_algebra_sigma_sets) (simp add: sigma_sets_singleton subset_eq)    have "(\<Inter>n. ?Q n) = (\<Inter>n∈{j..}. ?Q n)"      by (intro decseq_SucI INT_decseq_offset UN_mono) auto    also have "… ∈ sigma_sets (space M) (\<Union>i∈{j..}. sigma_sets (space M) {F i})"      using order_trans[OF F1 sets.space_closed]      by (safe intro!: S.countable_INT S.countable_UN)         (auto simp: sigma_sets_singleton intro!: sigma_sets.Basic bexI)    finally show "(\<Inter>n. ?Q n) ∈ sigma_sets (space M) (\<Union>i∈{j..}. sigma_sets (space M) {F i})"      by simp  qedqedlemma (in prob_space) indep_sets_finite:  assumes I: "I ≠ {}" "finite I"    and F: "!!i. i ∈ I ==> F i ⊆ events" "!!i. i ∈ I ==> space M ∈ F i"  shows "indep_sets F I <-> (∀A∈Pi I F. prob (\<Inter>j∈I. A j) = (∏j∈I. prob (A j)))"proof  assume *: "indep_sets F I"  from I show "∀A∈Pi I F. prob (\<Inter>j∈I. A j) = (∏j∈I. prob (A j))"    by (intro indep_setsD[OF *] ballI) autonext  assume indep: "∀A∈Pi I F. prob (\<Inter>j∈I. A j) = (∏j∈I. prob (A j))"  show "indep_sets F I"  proof (rule indep_setsI[OF F(1)])    fix A J assume J: "J ≠ {}" "J ⊆ I" "finite J"    assume A: "∀j∈J. A j ∈ F j"    let ?A = "λj. if j ∈ J then A j else space M"    have "prob (\<Inter>j∈I. ?A j) = prob (\<Inter>j∈J. A j)"      using subset_trans[OF F(1) sets.space_closed] J A      by (auto intro!: arg_cong[where f=prob] split: split_if_asm) blast    also    from A F have "(λj. if j ∈ J then A j else space M) ∈ Pi I F" (is "?A ∈ _")      by (auto split: split_if_asm)    with indep have "prob (\<Inter>j∈I. ?A j) = (∏j∈I. prob (?A j))"      by auto    also have "… = (∏j∈J. prob (A j))"      unfolding if_distrib setprod.If_cases[OF `finite I`]      using prob_space `J ⊆ I` by (simp add: Int_absorb1 setprod_1)    finally show "prob (\<Inter>j∈J. A j) = (∏j∈J. prob (A j))" ..  qedqedlemma (in prob_space) indep_vars_finite:  fixes I :: "'i set"  assumes I: "I ≠ {}" "finite I"    and M': "!!i. i ∈ I ==> sets (M' i) = sigma_sets (space (M' i)) (E i)"    and rv: "!!i. i ∈ I ==> random_variable (M' i) (X i)"    and Int_stable: "!!i. i ∈ I ==> Int_stable (E i)"    and space: "!!i. i ∈ I ==> space (M' i) ∈ E i" and closed: "!!i. i ∈ I ==> E i ⊆ Pow (space (M' i))"  shows "indep_vars M' X I <->    (∀A∈(Π i∈I. E i). prob (\<Inter>j∈I. X j -` A j ∩ space M) = (∏j∈I. prob (X j -` A j ∩ space M)))"proof -  from rv have X: "!!i. i ∈ I ==> X i ∈ space M -> space (M' i)"    unfolding measurable_def by simp  { fix i assume "i∈I"    from closed[OF `i ∈ I`]    have "sigma_sets (space M) {X i -` A ∩ space M |A. A ∈ sets (M' i)}      = sigma_sets (space M) {X i -` A ∩ space M |A. A ∈ E i}"      unfolding sigma_sets_vimage_commute[OF X, OF `i ∈ I`, symmetric] M'[OF `i ∈ I`]      by (subst sigma_sets_sigma_sets_eq) auto }  note sigma_sets_X = this  { fix i assume "i∈I"    have "Int_stable {X i -` A ∩ space M |A. A ∈ E i}"    proof (rule Int_stableI)      fix a assume "a ∈ {X i -` A ∩ space M |A. A ∈ E i}"      then obtain A where "a = X i -` A ∩ space M" "A ∈ E i" by auto      moreover      fix b assume "b ∈ {X i -` A ∩ space M |A. A ∈ E i}"      then obtain B where "b = X i -` B ∩ space M" "B ∈ E i" by auto      moreover      have "(X i -` A ∩ space M) ∩ (X i -` B ∩ space M) = X i -` (A ∩ B) ∩ space M" by auto      moreover note Int_stable[OF `i ∈ I`]      ultimately      show "a ∩ b ∈ {X i -` A ∩ space M |A. A ∈ E i}"        by (auto simp del: vimage_Int intro!: exI[of _ "A ∩ B"] dest: Int_stableD)    qed }  note indep_sets_X = indep_sets_sigma_sets_iff[OF this]  { fix i assume "i ∈ I"    { fix A assume "A ∈ E i"      with M'[OF `i ∈ I`] have "A ∈ sets (M' i)" by auto      moreover      from rv[OF `i∈I`] have "X i ∈ measurable M (M' i)" by auto      ultimately      have "X i -` A ∩ space M ∈ sets M" by (auto intro: measurable_sets) }    with X[OF `i∈I`] space[OF `i∈I`]    have "{X i -` A ∩ space M |A. A ∈ E i} ⊆ events"      "space M ∈ {X i -` A ∩ space M |A. A ∈ E i}"      by (auto intro!: exI[of _ "space (M' i)"]) }  note indep_sets_finite_X = indep_sets_finite[OF I this]  have "(∀A∈Π i∈I. {X i -` A ∩ space M |A. A ∈ E i}. prob (INTER I A) = (∏j∈I. prob (A j))) =    (∀A∈Π i∈I. E i. prob ((\<Inter>j∈I. X j -` A j) ∩ space M) = (∏x∈I. prob (X x -` A x ∩ space M)))"    (is "?L = ?R")  proof safe    fix A assume ?L and A: "A ∈ (Π i∈I. E i)"    from `?L`[THEN bspec, of "λi. X i -` A i ∩ space M"] A `I ≠ {}`    show "prob ((\<Inter>j∈I. X j -` A j) ∩ space M) = (∏x∈I. prob (X x -` A x ∩ space M))"      by (auto simp add: Pi_iff)  next    fix A assume ?R and A: "A ∈ (Π i∈I. {X i -` A ∩ space M |A. A ∈ E i})"    from A have "∀i∈I. ∃B. A i = X i -` B ∩ space M ∧ B ∈ E i" by auto    from bchoice[OF this] obtain B where B: "∀i∈I. A i = X i -` B i ∩ space M"      "B ∈ (Π i∈I. E i)" by auto    from `?R`[THEN bspec, OF B(2)] B(1) `I ≠ {}`    show "prob (INTER I A) = (∏j∈I. prob (A j))"      by simp  qed  then show ?thesis using `I ≠ {}`    by (simp add: rv indep_vars_def indep_sets_X sigma_sets_X indep_sets_finite_X cong: indep_sets_cong)qedlemma (in prob_space) indep_vars_compose:  assumes "indep_vars M' X I"  assumes rv: "!!i. i ∈ I ==> Y i ∈ measurable (M' i) (N i)"  shows "indep_vars N (λi. Y i o X i) I"  unfolding indep_vars_defproof  from rv `indep_vars M' X I`  show "∀i∈I. random_variable (N i) (Y i o X i)"    by (auto simp: indep_vars_def)  have "indep_sets (λi. sigma_sets (space M) {X i -` A ∩ space M |A. A ∈ sets (M' i)}) I"    using `indep_vars M' X I` by (simp add: indep_vars_def)  then show "indep_sets (λi. sigma_sets (space M) {(Y i o X i) -` A ∩ space M |A. A ∈ sets (N i)}) I"  proof (rule indep_sets_mono_sets)    fix i assume "i ∈ I"    with `indep_vars M' X I` have X: "X i ∈ space M -> space (M' i)"      unfolding indep_vars_def measurable_def by auto    { fix A assume "A ∈ sets (N i)"      then have "∃B. (Y i o X i) -` A ∩ space M = X i -` B ∩ space M ∧ B ∈ sets (M' i)"        by (intro exI[of _ "Y i -` A ∩ space (M' i)"])           (auto simp: vimage_compose intro!: measurable_sets rv `i ∈ I` funcset_mem[OF X]) }    then show "sigma_sets (space M) {(Y i o X i) -` A ∩ space M |A. A ∈ sets (N i)} ⊆      sigma_sets (space M) {X i -` A ∩ space M |A. A ∈ sets (M' i)}"      by (intro sigma_sets_subseteq) (auto simp: vimage_compose)  qedqedlemma (in prob_space) indep_varsD_finite:  assumes X: "indep_vars M' X I"  assumes I: "I ≠ {}" "finite I" "!!i. i ∈ I ==> A i ∈ sets (M' i)"  shows "prob (\<Inter>i∈I. X i -` A i ∩ space M) = (∏i∈I. prob (X i -` A i ∩ space M))"proof (rule indep_setsD)  show "indep_sets (λi. sigma_sets (space M) {X i -` A ∩ space M |A. A ∈ sets (M' i)}) I"    using X by (auto simp: indep_vars_def)  show "I ⊆ I" "I ≠ {}" "finite I" using I by auto  show "∀i∈I. X i -` A i ∩ space M ∈ sigma_sets (space M) {X i -` A ∩ space M |A. A ∈ sets (M' i)}"    using I by autoqedlemma (in prob_space) indep_varsD:  assumes X: "indep_vars M' X I"  assumes I: "J ≠ {}" "finite J" "J ⊆ I" "!!i. i ∈ J ==> A i ∈ sets (M' i)"  shows "prob (\<Inter>i∈J. X i -` A i ∩ space M) = (∏i∈J. prob (X i -` A i ∩ space M))"proof (rule indep_setsD)  show "indep_sets (λi. sigma_sets (space M) {X i -` A ∩ space M |A. A ∈ sets (M' i)}) I"    using X by (auto simp: indep_vars_def)  show "∀i∈J. X i -` A i ∩ space M ∈ sigma_sets (space M) {X i -` A ∩ space M |A. A ∈ sets (M' i)}"    using I by autoqed fact+lemma (in prob_space) indep_vars_iff_distr_eq_PiM:  fixes I :: "'i set" and X :: "'i => 'a => 'b"  assumes "I ≠ {}"  assumes rv: "!!i. random_variable (M' i) (X i)"  shows "indep_vars M' X I <->    distr M (Π⇣M i∈I. M' i) (λx. λi∈I. X i x) = (Π⇣M i∈I. distr M (M' i) (X i))"proof -  let ?P = "Π⇣M i∈I. M' i"  let ?X = "λx. λi∈I. X i x"  let ?D = "distr M ?P ?X"  have X: "random_variable ?P ?X" by (intro measurable_restrict rv)  interpret D: prob_space ?D by (intro prob_space_distr X)  let ?D' = "λi. distr M (M' i) (X i)"  let ?P' = "Π⇣M i∈I. distr M (M' i) (X i)"  interpret D': prob_space "?D' i" for i by (intro prob_space_distr rv)  interpret P: product_prob_space ?D' I ..      show ?thesis  proof    assume "indep_vars M' X I"    show "?D = ?P'"    proof (rule measure_eqI_generator_eq)      show "Int_stable (prod_algebra I M')"        by (rule Int_stable_prod_algebra)      show "prod_algebra I M' ⊆ Pow (space ?P)"        using prod_algebra_sets_into_space by (simp add: space_PiM)      show "sets ?D = sigma_sets (space ?P) (prod_algebra I M')"        by (simp add: sets_PiM space_PiM)      show "sets ?P' = sigma_sets (space ?P) (prod_algebra I M')"        by (simp add: sets_PiM space_PiM cong: prod_algebra_cong)      let ?A = "λi. Π⇣E i∈I. space (M' i)"      show "range ?A ⊆ prod_algebra I M'" "(\<Union>i. ?A i) = space (Pi⇣M I M')"        by (auto simp: space_PiM intro!: space_in_prod_algebra cong: prod_algebra_cong)      { fix i show "emeasure ?D (Π⇣E i∈I. space (M' i)) ≠ ∞" by auto }    next      fix E assume E: "E ∈ prod_algebra I M'"      from prod_algebraE[OF E] guess J Y . note J = this      from E have "E ∈ sets ?P" by (auto simp: sets_PiM)      then have "emeasure ?D E = emeasure M (?X -` E ∩ space M)"        by (simp add: emeasure_distr X)      also have "?X -` E ∩ space M = (\<Inter>i∈J. X i -` Y i ∩ space M)"        using J `I ≠ {}` measurable_space[OF rv] by (auto simp: prod_emb_def PiE_iff split: split_if_asm)      also have "emeasure M (\<Inter>i∈J. X i -` Y i ∩ space M) = (∏ i∈J. emeasure M (X i -` Y i ∩ space M))"        using `indep_vars M' X I` J `I ≠ {}` using indep_varsD[of M' X I J]        by (auto simp: emeasure_eq_measure setprod_ereal)      also have "… = (∏ i∈J. emeasure (?D' i) (Y i))"        using rv J by (simp add: emeasure_distr)      also have "… = emeasure ?P' E"        using P.emeasure_PiM_emb[of J Y] J by (simp add: prod_emb_def)      finally show "emeasure ?D E = emeasure ?P' E" .    qed  next    assume "?D = ?P'"    show "indep_vars M' X I" unfolding indep_vars_def    proof (intro conjI indep_setsI ballI rv)      fix i show "sigma_sets (space M) {X i -` A ∩ space M |A. A ∈ sets (M' i)} ⊆ events"        by (auto intro!: sets.sigma_sets_subset measurable_sets rv)    next      fix J Y' assume J: "J ≠ {}" "J ⊆ I" "finite J"      assume Y': "∀j∈J. Y' j ∈ sigma_sets (space M) {X j -` A ∩ space M |A. A ∈ sets (M' j)}"      have "∀j∈J. ∃Y. Y' j = X j -` Y ∩ space M ∧ Y ∈ sets (M' j)"      proof        fix j assume "j ∈ J"        from Y'[rule_format, OF this] rv[of j]        show "∃Y. Y' j = X j -` Y ∩ space M ∧ Y ∈ sets (M' j)"          by (subst (asm) sigma_sets_vimage_commute[symmetric, of _ _ "space (M' j)"])             (auto dest: measurable_space simp: sets.sigma_sets_eq)      qed      from bchoice[OF this] obtain Y where        Y: "!!j. j ∈ J ==> Y' j = X j -` Y j ∩ space M" "!!j. j ∈ J ==> Y j ∈ sets (M' j)" by auto      let ?E = "prod_emb I M' J (Pi⇣E J Y)"      from Y have "(\<Inter>j∈J. Y' j) = ?X -` ?E ∩ space M"        using J `I ≠ {}` measurable_space[OF rv] by (auto simp: prod_emb_def PiE_iff split: split_if_asm)      then have "emeasure M (\<Inter>j∈J. Y' j) = emeasure M (?X -` ?E ∩ space M)"        by simp      also have "… = emeasure ?D ?E"        using Y  J by (intro emeasure_distr[symmetric] X sets_PiM_I) auto      also have "… = emeasure ?P' ?E"        using `?D = ?P'` by simp      also have "… = (∏ i∈J. emeasure (?D' i) (Y i))"        using P.emeasure_PiM_emb[of J Y] J Y by (simp add: prod_emb_def)      also have "… = (∏ i∈J. emeasure M (Y' i))"        using rv J Y by (simp add: emeasure_distr)      finally have "emeasure M (\<Inter>j∈J. Y' j) = (∏ i∈J. emeasure M (Y' i))" .      then show "prob (\<Inter>j∈J. Y' j) = (∏ i∈J. prob (Y' i))"        by (auto simp: emeasure_eq_measure setprod_ereal)    qed  qedqedlemma (in prob_space) indep_varD:  assumes indep: "indep_var Ma A Mb B"  assumes sets: "Xa ∈ sets Ma" "Xb ∈ sets Mb"  shows "prob ((λx. (A x, B x)) -` (Xa × Xb) ∩ space M) =    prob (A -` Xa ∩ space M) * prob (B -` Xb ∩ space M)"proof -  have "prob ((λx. (A x, B x)) -` (Xa × Xb) ∩ space M) =    prob (\<Inter>i∈UNIV. (bool_case A B i -` bool_case Xa Xb i ∩ space M))"    by (auto intro!: arg_cong[where f=prob] simp: UNIV_bool)  also have "… = (∏i∈UNIV. prob (bool_case A B i -` bool_case Xa Xb i ∩ space M))"    using indep unfolding indep_var_def    by (rule indep_varsD) (auto split: bool.split intro: sets)  also have "… = prob (A -` Xa ∩ space M) * prob (B -` Xb ∩ space M)"    unfolding UNIV_bool by simp  finally show ?thesis .qedlemma (in prob_space)  assumes "indep_var S X T Y"  shows indep_var_rv1: "random_variable S X"    and indep_var_rv2: "random_variable T Y"proof -  have "∀i∈UNIV. random_variable (bool_case S T i) (bool_case X Y i)"    using assms unfolding indep_var_def indep_vars_def by auto  then show "random_variable S X" "random_variable T Y"    unfolding UNIV_bool by autoqedlemma (in prob_space) indep_var_distribution_eq:  "indep_var S X T Y <-> random_variable S X ∧ random_variable T Y ∧    distr M S X \<Otimes>⇣M distr M T Y = distr M (S \<Otimes>⇣M T) (λx. (X x, Y x))" (is "_ <-> _ ∧ _ ∧ ?S \<Otimes>⇣M ?T = ?J")proof safe  assume "indep_var S X T Y"  then show rvs: "random_variable S X" "random_variable T Y"    by (blast dest: indep_var_rv1 indep_var_rv2)+  then have XY: "random_variable (S \<Otimes>⇣M T) (λx. (X x, Y x))"    by (rule measurable_Pair)  interpret X: prob_space ?S by (rule prob_space_distr) fact  interpret Y: prob_space ?T by (rule prob_space_distr) fact  interpret XY: pair_prob_space ?S ?T ..  show "?S \<Otimes>⇣M ?T = ?J"  proof (rule pair_measure_eqI)    show "sigma_finite_measure ?S" ..    show "sigma_finite_measure ?T" ..    fix A B assume A: "A ∈ sets ?S" and B: "B ∈ sets ?T"    have "emeasure ?J (A × B) = emeasure M ((λx. (X x, Y x)) -` (A × B) ∩ space M)"      using A B by (intro emeasure_distr[OF XY]) auto    also have "… = emeasure M (X -` A ∩ space M) * emeasure M (Y -` B ∩ space M)"      using indep_varD[OF `indep_var S X T Y`, of A B] A B by (simp add: emeasure_eq_measure)    also have "… = emeasure ?S A * emeasure ?T B"      using rvs A B by (simp add: emeasure_distr)    finally show "emeasure ?S A * emeasure ?T B = emeasure ?J (A × B)" by simp  qed simpnext  assume rvs: "random_variable S X" "random_variable T Y"  then have XY: "random_variable (S \<Otimes>⇣M T) (λx. (X x, Y x))"    by (rule measurable_Pair)  let ?S = "distr M S X" and ?T = "distr M T Y"  interpret X: prob_space ?S by (rule prob_space_distr) fact  interpret Y: prob_space ?T by (rule prob_space_distr) fact  interpret XY: pair_prob_space ?S ?T ..  assume "?S \<Otimes>⇣M ?T = ?J"  { fix S and X    have "Int_stable {X -` A ∩ space M |A. A ∈ sets S}"    proof (safe intro!: Int_stableI)      fix A B assume "A ∈ sets S" "B ∈ sets S"      then show "∃C. (X -` A ∩ space M) ∩ (X -` B ∩ space M) = (X -` C ∩ space M) ∧ C ∈ sets S"        by (intro exI[of _ "A ∩ B"]) auto    qed }  note Int_stable = this  show "indep_var S X T Y" unfolding indep_var_eq  proof (intro conjI indep_set_sigma_sets Int_stable rvs)    show "indep_set {X -` A ∩ space M |A. A ∈ sets S} {Y -` A ∩ space M |A. A ∈ sets T}"    proof (safe intro!: indep_setI)      { fix A assume "A ∈ sets S" then show "X -` A ∩ space M ∈ sets M"        using `X ∈ measurable M S` by (auto intro: measurable_sets) }      { fix A assume "A ∈ sets T" then show "Y -` A ∩ space M ∈ sets M"        using `Y ∈ measurable M T` by (auto intro: measurable_sets) }    next      fix A B assume ab: "A ∈ sets S" "B ∈ sets T"      then have "ereal (prob ((X -` A ∩ space M) ∩ (Y -` B ∩ space M))) = emeasure ?J (A × B)"        using XY by (auto simp add: emeasure_distr emeasure_eq_measure intro!: arg_cong[where f="prob"])      also have "… = emeasure (?S \<Otimes>⇣M ?T) (A × B)"        unfolding `?S \<Otimes>⇣M ?T = ?J` ..      also have "… = emeasure ?S A * emeasure ?T B"        using ab by (simp add: Y.emeasure_pair_measure_Times)      finally show "prob ((X -` A ∩ space M) ∩ (Y -` B ∩ space M)) =        prob (X -` A ∩ space M) * prob (Y -` B ∩ space M)"        using rvs ab by (simp add: emeasure_eq_measure emeasure_distr)    qed  qedqedlemma (in prob_space) distributed_joint_indep:  assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"  assumes X: "distributed M S X Px" and Y: "distributed M T Y Py"  assumes indep: "indep_var S X T Y"  shows "distributed M (S \<Otimes>⇣M T) (λx. (X x, Y x)) (λ(x, y). Px x * Py y)"  using indep_var_distribution_eq[of S X T Y] indep  by (intro distributed_joint_indep'[OF S T X Y]) autoend`