Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/HOL/Probability/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 74 kB

Quelle Independent_Family.thy Sprache: Isabelle

(*  Title:      HOL/Probability/Independent_Family.thy
    Author:     Johannes Hölzl, TU München
    Author:     Sudeep Kanav, TU München
*)

section \<open>Independent families of events, event sets, and random variables\<close>

theory Independent_Family
  imports Infinite_Product_Measure
begin

definition (in prob_space)
  "indep_sets F I \ (\i\I. F i \ events) \
    (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> (\<forall>A\<in>Pi J F. prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))))"

definition (in prob_space)
  "indep_set A B \ indep_sets (case_bool 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) \
    (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>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
  done

lemma (in prob_space) indep_eventsI:
  "(\i. i \ I \ F i \ sets M) \ (\J. J \ I \ finite J \ J \ {} \ prob (\i\J. F i) = (\i\J. prob (F i))) \ indep_events F I"
  by (auto simp: indep_events_def)

definition (in prob_space)
  "indep_event A B \ indep_events (case_bool 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 auto

lemma (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)
qed

lemma (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 +)
  done

lemma (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 (\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 (\j\J. A j) = (\j\J. prob (A j))"
  using assms unfolding indep_sets_def by auto

lemma (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_def
proof (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 \<open>J \<noteq> {}\<close> indep[of "F True" "F False"]
  show "prob (\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 "case_bool 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 auto

lemma (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 define G where "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)
          \<Longrightarrow> prob ((\<Inter>i\<in>J. A i) \<inter> X) = prob X * (\<Prod>i\<in>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 (\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 (\i\J. A i) = prob ((\i\J-{j}. A i) \ X)"
                using \<open>j \<in> J\<close> \<open>A j = X\<close> by (auto intro!: arg_cong[where f=prob] split: if_split_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 \<open>J \<noteq> {j}\<close> \<open>j \<in> J\<close> 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 \<open>A j = X\<close> by simp
              also have "\ = (\i\J. prob (A i))"
                unfolding prod.insert_remove[OF \<open>finite J\<close>, symmetric, of "\<lambda>i. prob  (A i)"]
                using \<open>j \<in> J\<close> 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: if_split_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 ((\j\J. A j) \ (space M - X)) =
              prob ((\<Inter>j\<in>J. A j) - (\<Inter>i\<in>insert j J. (A(j := X)) i))"
            using A_sets sets.sets_into_space[of _ M] X \<open>J \<noteq> {}\<close>
            by (auto intro!: arg_cong[where f=prob] split: if_split_asm)
          also have "\ = prob (\j\J. A j) - prob (\i\insert j J. (A(j := X)) i)"
            using J \<open>J \<noteq> {}\<close> \<open>j \<notin> J\<close> A_sets X sets.sets_into_space
            by (auto intro!: finite_measure_Diff sets.finite_INT split: if_split_asm)
          finally have "prob ((\j\J. A j) \ (space M - X)) =
              prob (\<Inter>j\<in>J. A j) - prob (\<Inter>i\<in>insert j J. (A(j := X)) i)" .
          moreover {
            have "prob (\j\J. A j) = (\j\J. prob (A j))"
              using J A \<open>finite J\<close> by (intro indep_setsD[OF G(1)]) auto
            then have "prob (\j\J. A j) = prob (space M) * (\i\J. prob (A i))"
              using prob_space by simp }
          moreover {
            have "prob (\i\insert j J. (A(j := X)) i) = (\i\insert j J. prob ((A(j := X)) i))"
              using J A \<open>j \<in> K\<close> by (intro indep_setsD[OF G']) auto
            then have "prob (\i\insert j J. (A(j := X)) i) = prob X * (\i\J. prob (A i))"
              using \<open>finite J\<close> \<open>j \<notin> J\<close> by (auto intro!: prod.cong) }
          ultimately have "prob ((\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 ((\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 := {\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 ((\j\J. A j) \ (\k. F k)) = prob (\k. (\i\insert j J. (A(j := F k)) i))"
            using \<open>J \<noteq> {}\<close> \<open>j \<notin> J\<close> \<open>j \<in> K\<close> by (auto intro!: arg_cong[where f=prob] split: if_split_asm)
          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))"
          proof (rule finite_measure_UNION)
            show "disjoint_family (\k. \i\insert j J. (A(j := F k)) i)"
              using disj by (rule disjoint_family_on_bisimulation) auto
            show "range (\k. \i\insert j J. (A(j := F k)) i) \ events"
              using A_sets F \<open>finite J\<close> \<open>J \<noteq> {}\<close> \<open>j \<notin> J\<close> by (auto intro!: sets.Int)
          qed
          moreover { fix k
            from J A \<open>j \<in> K\<close> have "prob (\<Inter>i\<in>insert j J. (A(j := F k)) i) = prob (F k) * (\<Prod>i\<in>J. prob (A i))"
              by (subst indep_setsD[OF F(2)]) (auto intro!: prod.cong split: if_split_asm)
            also have "\ = prob (F k) * prob (\i\J. A i)"
              using J A \<open>j \<in> K\<close> by (subst indep_setsD[OF G(1)]) auto
            finally have "prob (\i\insert j J. (A(j := F k)) i) = prob (F k) * prob (\i\J. A i)" . }
          ultimately have "(\k. prob (F k) * prob (\i\J. A i)) sums (prob ((\j\J. A j) \ (\k. F k)))"
            by simp
          moreover
          have "(\k. prob (F k) * prob (\i\J. A i)) sums (prob (\k. F k) * prob (\i\J. A i))"
            using disj F(1) by (intro finite_measure_UNION sums_mult2) auto
          then have "(\k. prob (F k) * prob (\i\J. A i)) sums (prob (\k. F k) * (\i\J. prob (A i)))"
            using J A \<open>j \<in> K\<close> by (subst indep_setsD[OF G(1), symmetric]) auto
          ultimately
          show "prob ((\j\J. A j) \ (\k. F k)) = prob (\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 \<open>indep_sets G K\<close>
        show "indep_sets (G(j := {X})) K"
          by (rule indep_sets_mono_sets) (insert \<open>X \<in> G j\<close>, 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 (\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: if_split_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 \<open>j \<in> K\<close> \<open>j \<notin> J\<close>, auto simp: G_def)
    qed (insert \<open>indep_sets F K\<close>, simp) }
  from this[OF \<open>indep_sets F J\<close> \<open>finite J\<close> subset_refl]
  show "indep_sets ?F J"
    by (rule indep_sets_mono_sets) auto
qed

lemma (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
  qed
qed

lemma (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) fact
next
  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)
qed

definition (in prob_space)
  indep_vars_def2: "indep_vars M' X I \
    (\<forall>i\<in>I. random_variable (M' i) (X i)) \<and>
    indep_sets (\<lambda>i. { X i -` A \<inter> space M | A. A \<in> sets (M' i)}) I"

definition (in prob_space)
  "indep_var Ma A Mb B \ indep_vars (case_bool Ma Mb) (case_bool A B) UNIV"

lemma (in prob_space) indep_vars_def:
  "indep_vars M' X I \
    (\<forall>i\<in>I. random_variable (M' i) (X i)) \<and>
    indep_sets (\<lambda>i. sigma_sets (space M) { X i -` A \<inter> space M | A. A \<in> 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
  done

lemma (in prob_space) indep_var_eq:
  "indep_var S X T Y \
    (random_variable S X \<and> random_variable T Y) \<and>
    indep_set
      (sigma_sets (space M) { X -` A \<inter> space M | A. A \<in> sets S})
      (sigma_sets (space M) { Y -` A \<inter> space M | A. A \<in> sets T})"
  unfolding indep_var_def indep_vars_def indep_set_def UNIV_bool
  by (intro arg_cong2[where f="(\)"] 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_def
proof (intro iffI ballI conjI)
  assume indep: "indep_sets (case_bool A B) UNIV"
  { fix a b assume "a \ A" "b \ B"
    with indep_setsD[OF indep, of UNIV "case_bool 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 auto
next
  assume *: "A \ events \ B \ events \ (\a\A. \b\B. prob (a \ b) = prob a * prob b)"
  show "indep_sets (case_bool 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 (\j\J. X j) = (\j\J. prob (X j))"
      using X * by auto
  qed
qed

lemma (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 (case_bool A B) UNIV"
      by (rule \<open>indep_set A B\<close>[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)
qed

lemma (in prob_space) indep_eventsI_indep_vars:
  assumes indep: "indep_vars N X I"
  assumes P: "\i. i \ I \ {x\space (N i). P i x} \ sets (N i)"
  shows "indep_events (\i. {x\space M. P i (X i x)}) I"
proof -
  have "indep_sets (\i. {X i -` A \ space M |A. A \ sets (N i)}) I"
    using indep unfolding indep_vars_def2 by auto
  then show ?thesis
    unfolding indep_events_def_alt
  proof (rule indep_sets_mono_sets)
    fix i assume "i \ I"
    then have "{{x \ space M. P i (X i x)}} = {X i -` {x\space (N i). P i x} \ space M}"
      using indep by (auto simp: indep_vars_def dest: measurable_space)
    also have "\ \ {X i -` A \ space M |A. A \ sets (N i)}"
      using P[OF \<open>i \<in> I\<close>] by blast
    finally show "{{x \ space M. P i (X i x)}} \ {X i -` A \ space M |A. A \ sets (N i)}" .
  qed
qed

lemma (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 (\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) (\i\I j. E i)) J"
proof -
  let ?E = "\j. {\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) (\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) (\i\I j. E i) = sigma_sets (space M) (?E j)"
    proof (rule sigma_sets_eqI)
      fix A assume "A \ (\i\I j. E i)"
      then obtain i where "i \ I j" "A \ E 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 = (\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) (\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 = (\l\L. E' l) \ finite L \ L \ {} \ L \ I j \ (\l\L. E' l \ E l)"
        by simp
      from bchoice[OF this] obtain E'
        where "\x\K. \L. A x = \ (E' x ` L) \ finite L \ L \ {} \ L \ I x \ (\l\L. E' x l \ E l)"
        ..
      from bchoice[OF this] obtain L
        where A: "\j. j\K \ A j = (\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 \<open>K \<subseteq> J\<close> \<open>k \<in> K\<close> \<open>j \<in> K\<close> have "I k \<inter> I j = {}"
            unfolding disjoint_family_on_def by auto
          with L(2,3)[OF \<open>j \<in> K\<close>] L(2,3)[OF \<open>k \<in> K\<close>]
          show False using \<open>l \<in> L k\<close> \<open>l \<in> L j\<close> by auto
        qed }
      note L_inj = this

      define k where "k l = (SOME k. k \ K \ l \ L k)" for l
      { 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 (\j\K. A j) = prob (\l\(\k\K. L k). ?E' l)"
        by (auto simp: A intro!: arg_cong[where f=prob])
      also have "\ = (\l\(\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 prod.UNION_disjoint) auto
      also have "\ = (\j\K. prob (A j))"
        using K L E' by (auto simp add: A intro!: prod.cong indep_setsD[OF indep, symmetric]) blast
      finally show "prob (\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 = (\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 = (\k\Kb. Eb k)" "finite Kb" "Kb \ {}" "Kb \ I j" "\k. k\Kb \ Eb k \ E k" by auto
      let ?f = "\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 "Ka \ Kb = (Ka \ Kb) \ (Kb - Ka) \ (Ka - Kb)"
        by blast
      moreover have "(\x\Ka \ Kb. Ea x \ Eb x) \
        (\<Inter>x\<in>Kb - Ka. Eb x) \<inter> (\<Inter>x\<in>Ka - Kb. Ea x) = (\<Inter>k\<in>Ka. Ea k) \<inter> (\<Inter>k\<in>Kb. Eb k)"
        by auto
      ultimately have "(\k\Ka \ Kb. ?f k) = (\k\Ka. Ea k) \ (\k\Kb. Eb k)" (is "?lhs = ?rhs")
        by (simp only: image_Un Inter_Un_distrib) simp
      then have "a \ b = (\k\Ka \ Kb. ?f k)"
        by (simp only: a(1) b(1))
      with a b \<open>j \<in> J\<close> Int_stableD[OF Int_stable] show "a \<inter> b \<in> ?E j"
        by (intro CollectI exI[of _ "Ka \ Kb"] exI[of _ ?f]) auto
    qed
  qed
  ultimately show ?thesis
    by (simp cong: indep_sets_cong)
qed

lemma (in prob_space) indep_vars_restrict:
  assumes ind: "indep_vars M' X I" and K: "\j. j \ L \ K j \ I" and J: "disjoint_family_on K L"
  shows "indep_vars (\j. PiM (K j) M') (\j \. restrict (\i. X i \) (K j)) L"
  unfolding indep_vars_def
proof safe
  fix j assume "j \ L" then show "random_variable (Pi\<^sub>M (K j) M') (\\. \i\K j. X i \)"
    using K ind by (auto simp: indep_vars_def intro!: measurable_restrict)
next
  have X: "\i. i \ I \ X i \ measurable M (M' i)"
    using ind by (auto simp: indep_vars_def)
  let ?proj = "\j S. {(\\. \i\K j. X i \) -` A \ space M |A. A \ S}"
  let ?UN = "\j. sigma_sets (space M) (\i\K j. { X i -` A \ space M| A. A \ sets (M' i) })"
  show "indep_sets (\i. sigma_sets (space M) (?proj i (sets (Pi\<^sub>M (K i) M')))) L"
  proof (rule indep_sets_mono_sets)
    fix j assume j: "j \ L"
    have "sigma_sets (space M) (?proj j (sets (Pi\<^sub>M (K j) M'))) =
      sigma_sets (space M) (sigma_sets (space M) (?proj j (prod_algebra (K j) M')))"
      using j K X[THEN measurable_space] unfolding sets_PiM
      by (subst sigma_sets_vimage_commute) (auto simp add: Pi_iff)
    also have "\ = sigma_sets (space M) (?proj j (prod_algebra (K j) M'))"
      by (rule sigma_sets_sigma_sets_eq) auto
    also have "\ \ ?UN j"
    proof (rule sigma_sets_mono, safe del: disjE elim!: prod_algebraE)
      fix J E assume J: "finite J" "J \ {} \ K j = {}" "J \ K j" and E: "\i. i \ J \ E i \ sets (M' i)"
      show "(\\. \i\K j. X i \) -` prod_emb (K j) M' J (Pi\<^sub>E J E) \ space M \ ?UN j"
      proof cases
        assume "K j = {}" with J show ?thesis
          by (auto simp add: sigma_sets_empty_eq prod_emb_def)
      next
        assume "K j \ {}" with J have "J \ {}"
          by auto
        { interpret sigma_algebra "space M" "?UN j"
            by (rule sigma_algebra_sigma_sets) auto
          have "\A. (\i. i \ J \ A i \ ?UN j) \ \(A ` J) \ ?UN j"
            using \<open>finite J\<close> \<open>J \<noteq> {}\<close> by (rule finite_INT) blast }
        note INT = this

        from \<open>J \<noteq> {}\<close> J K E[rule_format, THEN sets.sets_into_space] j
        have "(\\. \i\K j. X i \) -` prod_emb (K j) M' J (Pi\<^sub>E J E) \ space M
          = (\<Inter>i\<in>J. X i -` E i \<inter> space M)"
          apply (subst prod_emb_PiE[OF _ ])
          apply auto []
          apply auto []
          apply (auto simp add: Pi_iff intro!: X[THEN measurable_space])
          apply (erule_tac x=i in ballE)
          apply auto
          done
        also have "\ \ ?UN j"
          apply (rule INT)
          apply (rule sigma_sets.Basic)
          using \<open>J \<subseteq> K j\<close> E
          apply auto
          done
        finally show ?thesis .
      qed
    qed
    finally show "sigma_sets (space M) (?proj j (sets (Pi\<^sub>M (K j) M'))) \ ?UN j" .
  next
    show "indep_sets ?UN L"
    proof (rule indep_sets_collect_sigma)
      show "indep_sets (\i. {X i -` A \ space M |A. A \ sets (M' i)}) (\j\L. K j)"
      proof (rule indep_sets_mono_index)
        show "indep_sets (\i. {X i -` A \ space M |A. A \ sets (M' i)}) I"
          using ind unfolding indep_vars_def2 by auto
        show "(\l\L. K l) \ I"
          using K by auto
      qed
    next
      fix l i assume "l \ L" "i \ K l"
      show "Int_stable {X i -` A \ space M |A. A \ sets (M' i)}"
        apply (auto simp: Int_stable_def)
        apply (rule_tac x="A \ Aa" in exI)
        apply auto
        done
    qed fact
  qed
qed

lemma (in prob_space) indep_var_restrict:
  assumes ind: "indep_vars M' X I" and AB: "A \ B = {}" "A \ I" "B \ I"
  shows "indep_var (PiM A M') (\\. restrict (\i. X i \) A) (PiM B M') (\\. restrict (\i. X i \) B)"
proof -
  have *:
    "case_bool (Pi\<^sub>M A M') (Pi\<^sub>M B M') = (\b. PiM (case_bool A B b) M')"
    "case_bool (\\. \i\A. X i \) (\\. \i\B. X i \) = (\b \. \i\case_bool A B b. X i \)"
    by (simp_all add: fun_eq_iff split: bool.split)
  show ?thesis
    unfolding indep_var_def * using AB
    by (intro indep_vars_restrict[OF ind]) (auto simp: disjoint_family_on_def split: bool.split)
qed

lemma (in prob_space) indep_vars_subset:
  assumes "indep_vars M' X I" "J \ I"
  shows "indep_vars M' X J"
  using assms unfolding indep_vars_def indep_sets_def
  by auto

lemma (in prob_space) indep_vars_cong:
  "I = J \ (\i. i \ I \ X i = Y i) \ (\i. i \ I \ M' i = N' i) \ indep_vars M' X I \ indep_vars N' Y J"
  unfolding indep_vars_def2 by (intro conj_cong indep_sets_cong) auto

definition (in prob_space) tail_events where
  "tail_events A = (\n. sigma_sets (space M) (\ (A ` {n..})))"

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 = "(\n. sigma_sets (space M) (\ (A ` {n..})))"
  from X have "\n::nat. X \ sigma_sets (space M) (\ (A ` {n..}))" by (auto simp: tail_events_def)
  from this[of 0] have "X \ sigma_sets (space M) (\(A ` UNIV))" by simp
  then show "X \ events"
    by induct (insert A, auto)
qed

lemma (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_def
proof (simp add: sigma_algebra_iff2, safe)
  let ?A = "(\n. sigma_sets (space M) (\ (A ` {n..})))"
  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) (\ (A ` {n..}))" by auto
    from this[of 0] have "X \ sigma_sets (space M) (\(A ` UNIV))" by simp
    then have "X \ space M"
      by induct (insert A.sets_into_space, auto)
    with \<open>x \<in> X\<close> show "x \<in> space M" by auto }
  { fix F :: "nat \ 'a set" and n assume "range F \ ?A"
    then show "(\(F ` UNIV)) \ sigma_sets (space M) (\ (A ` {n..}))"
      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 \<open>X \<subseteq> space M\<close> by (simp add: Int_absorb2)
  next
    fix A assume A: "A \ ?D"
    have "prob (X \ (space M - A)) = prob (X - (X \ A))"
      using \<open>X \<subseteq> space M\<close> 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 \<open>X \<subseteq> space M\<close> 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 (\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 \ (\i. F i))"
      by simp
    moreover have "(\i. prob X * prob (F i)) sums (prob X * prob (\i. F i))"
      by (intro sums_mult finite_measure_UNION F dis)
    ultimately have "prob (X \ (\i. F i)) = prob X * prob (\i. F i)"
      by (auto dest!: sums_unique)
    with F show "(\i. F i) \ ?D"
      by auto
  qed

  { fix n
    have "indep_sets (\b. sigma_sets (space M) (\m\case_bool {..n} {Suc n..} b. A m)) UNIV"
    proof (rule indep_sets_collect_sigma)
      have *: "(\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 (case_bool {..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) (\m\case_bool {..n} {Suc n..} b. A m)) =
      case_bool (sigma_sets (space M) (\<Union>m\<in>{..n}. A m)) (sigma_sets (space M) (\<Union>m\<in>{Suc n..}. A m))"
      by (auto intro!: ext split: bool.split)
    finally have indep: "indep_set (sigma_sets (space M) (\m\{..n}. A m)) (sigma_sets (space M) (\m\{Suc n..}. A m))"
      unfolding indep_set_def by simp

    have "sigma_sets (space M) (\m\{..n}. A m) \ ?D"
    proof (simp add: subset_eq, rule)
      fix D assume D: "D \ sigma_sets (space M) (\m\{..n}. A m)"
      have "X \ sigma_sets (space M) (\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 "(\n. sigma_sets (space M) (\m\{..n}. A m)) \ ?D" (is "?A \ _")
    by auto

  note \<open>X \<in> tail_events A\<close>
  also {
    have "\n. sigma_sets (space M) (\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) (\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 b assume "a \ ?A" "b \ ?A" then obtain n m
        where a: "n \ UNIV" "a \ sigma_sets (space M) (\ (A ` {..n}))"
          and b: "m \ UNIV" "b \ sigma_sets (space M) (\ (A ` {..m}))" by auto
      interpret Amn: sigma_algebra "space M" "sigma_sets (space M) (\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) (\i\{..n}. A i) \ sigma_sets (space M) (\i\{..max m n}. A i)"
        by (intro sigma_sets_subseteq UN_mono) auto
      with a have "a \ sigma_sets (space M) (\i\{..max m n}. A i)" by auto
      moreover
      have "sigma_sets (space M) (\i\{..m}. A i) \ sigma_sets (space M) (\i\{..max m n}. A i)"
        by (intro sigma_sets_subseteq UN_mono) auto
      with b have "b \ sigma_sets (space M) (\i\{..max m n}. A i)" by auto
      ultimately have "a \ b \ sigma_sets (space M) (\i\{..max m n}. A i)"
        using Amn.Int[of a b] by simp
      then show "a \ b \ (\n. sigma_sets (space M) (\i\{..n}. A i))" by auto
    qed
  qed
  also have "Dynkin (space M) ?A \ ?D"
    using \<open>?A \<subseteq> ?D\<close> by (auto intro!: D.Dynkin_subset)
  finally show ?thesis by auto
qed

lemma (in prob_space) borel_0_1_law:
  fixes F :: "nat \ 'a set"
  assumes F2: "indep_events F UNIV"
  shows "prob (\n. \m\{n..}. F m) = 0 \ prob (\n. \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. \i\{n..}. F i"
  show "(\n. \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) (\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 "(\n. ?Q n) = (\n\{j..}. ?Q n)"
      by (intro decseq_SucI INT_decseq_offset UN_mono) auto
    also have "\ \ sigma_sets (space M) (\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 "(\n. ?Q n) \ sigma_sets (space M) (\i\{j..}. sigma_sets (space M) {F i})"
      by simp
  qed
qed

lemma (in prob_space) borel_0_1_law_AE:
  fixes P :: "nat \ 'a \ bool"
  assumes "indep_events (\m. {x\space M. P m x}) UNIV" (is "indep_events ?P _")
  shows "(AE x in M. infinite {m. P m x}) \ (AE x in M. finite {m. P m x})"
proof -
  have [measurable]: "\m. {x\space M. P m x} \ sets M"
    using assms by (auto simp: indep_events_def)
  have *: "(\n. \m\{n..}. {x \ space M. P m x}) \ events"
    by simp
  from assms have "prob (\n. \m\{n..}. ?P m) = 0 \ prob (\n. \m\{n..}. ?P m) = 1"
    by (rule borel_0_1_law)
  also have "prob (\n. \m\{n..}. ?P m) = 1 \ (AE x in M. infinite {m. P m x})"
    using * by (simp add: prob_eq_1)
      (simp add: Bex_def infinite_nat_iff_unbounded_le)
  also have "prob (\n. \m\{n..}. ?P m) = 0 \ (AE x in M. finite {m. P m x})"
    using * by (simp add: prob_eq_0)
      (auto simp add: Ball_def finite_nat_iff_bounded not_less [symmetric])
  finally show ?thesis
    by blast
qed

lemma (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 (\j\I. A j) = (\j\I. prob (A j)))"
proof
  assume *: "indep_sets F I"
  from I show "\A\Pi I F. prob (\j\I. A j) = (\j\I. prob (A j))"
    by (intro indep_setsD[OF *] ballI) auto
next
  assume indep: "\A\Pi I F. prob (\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 (\j\I. ?A j) = prob (\j\J. A j)"
      using subset_trans[OF F(1) sets.space_closed] J A
      by (auto intro!: arg_cong[where f=prob] split: if_split_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: if_split_asm)
    with indep have "prob (\j\I. ?A j) = (\j\I. prob (?A j))"
      by auto
    also have "\ = (\j\J. prob (A j))"
      unfolding if_distrib prod.If_cases[OF \<open>finite I\<close>]
      using prob_space \<open>J \<subseteq> I\<close> by (simp add: Int_absorb1 prod.neutral_const)
    finally show "prob (\j\J. A j) = (\j\J. prob (A j))" ..
  qed
qed

lemma (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 \
    (\<forall>A\<in>(\<Pi> i\<in>I. E i). prob (\<Inter>j\<in>I. X j -` A j \<inter> space M) = (\<Prod>j\<in>I. prob (X j -` A j \<inter> 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 \<open>i \<in> I\<close>]
    have "sigma_sets (space M) {X i -` A \ space M |A. A \ sets (M' i)}
      = sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> E i}"
      unfolding sigma_sets_vimage_commute[OF X, OF \<open>i \<in> I\<close>, symmetric] M'[OF \<open>i \<in> I\<close>]
      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 \<open>i \<in> I\<close>]
      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 \<open>i\<in>I\<close>] have "X i \<in> measurable M (M' i)" by auto
      ultimately
      have "X i -` A \ space M \ sets M" by (auto intro: measurable_sets) }
    with X[OF \<open>i\<in>I\<close>] space[OF \<open>i\<in>I\<close>]
    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 (\(A ` I)) = (\j\I. prob (A j))) =
    (\<forall>A\<in>\<Pi> i\<in>I. E i. prob ((\<Inter>j\<in>I. X j -` A j) \<inter> space M) = (\<Prod>x\<in>I. prob (X x -` A x \<inter> space M)))"
    (is "?L = ?R")
  proof safe
    fix A assume ?L and A: "A \ (\ i\I. E i)"
    from \<open>?L\<close>[THEN bspec, of "\<lambda>i. X i -` A i \<inter> space M"] A \<open>I \<noteq> {}\<close>
    show "prob ((\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 \<open>?R\<close>[THEN bspec, OF B(2)] B(1) \<open>I \<noteq> {}\<close>
    show "prob (\(A ` I)) = (\j\I. prob (A j))"
      by simp
  qed
  then show ?thesis using \<open>I \<noteq> {}\<close>
    by (simp add: rv indep_vars_def indep_sets_X sigma_sets_X indep_sets_finite_X cong: indep_sets_cong)
qed

lemma (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 \ X i) I"
  unfolding indep_vars_def
proof
  from rv \<open>indep_vars M' X I\<close>
  show "\i\I. random_variable (N i) (Y i \ 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 \<open>indep_vars M' X I\<close> by (simp add: indep_vars_def)
  then show "indep_sets (\i. sigma_sets (space M) {(Y i \ X i) -` A \ space M |A. A \ sets (N i)}) I"
  proof (rule indep_sets_mono_sets)
    fix i assume "i \ I"
    with \<open>indep_vars M' X I\<close> have X: "X i \<in> space M \<rightarrow> space (M' i)"
      unfolding indep_vars_def measurable_def by auto
    { fix A assume "A \ sets (N i)"
      then have "\B. (Y i \ 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_comp intro!: measurable_sets rv \<open>i \<in> I\<close> funcset_mem[OF X]) }
    then show "sigma_sets (space M) {(Y i \ X i) -` A \ space M |A. A \ sets (N i)} \
      sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)}"
      by (intro sigma_sets_subseteq) (auto simp: vimage_comp)
  qed
qed

lemma (in prob_space) indep_vars_compose2:
  assumes "indep_vars M' X I"
  assumes rv: "\i. i \ I \ Y i \ measurable (M' i) (N i)"
  shows "indep_vars N (\i x. Y i (X i x)) I"
  using indep_vars_compose [OF assms] by (simp add: comp_def)

lemma (in prob_space) indep_var_compose:
  assumes "indep_var M1 X1 M2 X2" "Y1 \ measurable M1 N1" "Y2 \ measurable M2 N2"
  shows "indep_var N1 (Y1 \ X1) N2 (Y2 \ X2)"
proof -
  have "indep_vars (case_bool N1 N2) (\b. case_bool Y1 Y2 b \ case_bool X1 X2 b) UNIV"
    using assms
    by (intro indep_vars_compose[where M'="case_bool M1 M2"])
       (auto simp: indep_var_def split: bool.split)
  also have "(\b. case_bool Y1 Y2 b \ case_bool X1 X2 b) = case_bool (Y1 \ X1) (Y2 \ X2)"
    by (simp add: fun_eq_iff split: bool.split)
  finally show ?thesis
    unfolding indep_var_def .
qed

lemma (in prob_space) indep_vars_Min:
  fixes X :: "'i \ 'a \ real"
  assumes I: "finite I" "i \ I" and indep: "indep_vars (\_. borel) X (insert i I)"
  shows "indep_var borel (X i) borel (\\. Min ((\i. X i \)`I))"
proof -
  have "indep_var
    borel ((\<lambda>f. f i) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) {i}))
    borel ((\<lambda>f. Min (f`I)) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) I))"
    using I by (intro indep_var_compose[OF indep_var_restrict[OF indep]] borel_measurable_Min) auto
  also have "((\f. f i) \ (\\. restrict (\i. X i \) {i})) = X i"
    by auto
  also have "((\f. Min (f`I)) \ (\\. restrict (\i. X i \) I)) = (\\. Min ((\i. X i \)`I))"
    by (auto cong: rev_conj_cong)
  finally show ?thesis
    unfolding indep_var_def .
qed

lemma (in prob_space) indep_vars_sum:
  fixes X :: "'i \ 'a \ real"
  assumes I: "finite I" "i \ I" and indep: "indep_vars (\_. borel) X (insert i I)"
  shows "indep_var borel (X i) borel (\\. \i\I. X i \)"
proof -
  have "indep_var
    borel ((\<lambda>f. f i) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) {i}))
    borel ((\<lambda>f. \<Sum>i\<in>I. f i) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) I))"
    using I by (intro indep_var_compose[OF indep_var_restrict[OF indep]] ) auto
  also have "((\f. f i) \ (\\. restrict (\i. X i \) {i})) = X i"
    by auto
  also have "((\f. \i\I. f i) \ (\\. restrict (\i. X i \) I)) = (\\. \i\I. X i \)"
    by (auto cong: rev_conj_cong)
  finally show ?thesis .
qed

lemma (in prob_space) indep_vars_prod:
  fixes X :: "'i \ 'a \ real"
  assumes I: "finite I" "i \ I" and indep: "indep_vars (\_. borel) X (insert i I)"
  shows "indep_var borel (X i) borel (\\. \i\I. X i \)"
proof -
  have "indep_var
    borel ((\<lambda>f. f i) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) {i}))
    borel ((\<lambda>f. \<Prod>i\<in>I. f i) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) I))"
    using I by (intro indep_var_compose[OF indep_var_restrict[OF indep]] ) auto
  also have "((\f. f i) \ (\\. restrict (\i. X i \) {i})) = X i"
    by auto
  also have "((\f. \i\I. f i) \ (\\. restrict (\i. X i \) I)) = (\\. \i\I. X i \)"
    by (auto cong: rev_conj_cong)
  finally show ?thesis .
qed

lemma (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 (\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 auto
qed

lemma (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 (\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 auto
qed 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 (\<Pi>\<^sub>M i\<in>I. M' i) (\<lambda>x. \<lambda>i\<in>I. X i x) = (\<Pi>\<^sub>M i\<in>I. distr M (M' i) (X i))"
proof -
  let ?P = "\\<^sub>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' = "\\<^sub>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. \\<^sub>E i\I. space (M' i)"
      show "range ?A \ prod_algebra I M'" "(\i. ?A i) = space (Pi\<^sub>M I M')"
        by (auto simp: space_PiM intro!: space_in_prod_algebra cong: prod_algebra_cong)
      { fix i show "emeasure ?D (\\<^sub>E i\I. space (M' i)) \ \" by auto }
    next
      fix E assume E: "E \ prod_algebra I M'"
      from prod_algebraE[OF E] obtain J Y
        where J:
          "E = prod_emb I M' J (Pi\<^sub>E J Y)"
          "finite J"
          "J \ {} \ I = {}"
          "J \ I"
          "\i. i \ J \ Y i \ sets (M' i)"
        by auto
      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 = (\i\J. X i -` Y i \ space M)"
        using J \<open>I \<noteq> {}\<close> measurable_space[OF rv] by (auto simp: prod_emb_def PiE_iff split: if_split_asm)
      also have "emeasure M (\i\J. X i -` Y i \ space M) = (\ i\J. emeasure M (X i -` Y i \ space M))"
        using \<open>indep_vars M' X I\<close> J \<open>I \<noteq> {}\<close> using indep_varsD[of M' X I J]
        by (auto simp: emeasure_eq_measure prod_ennreal measure_nonneg prod_nonneg)
      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\<^sub>E J Y)"
      from Y have "(\j\J. Y' j) = ?X -` ?E \ space M"
        using J \<open>I \<noteq> {}\<close> measurable_space[OF rv] by (auto simp: prod_emb_def PiE_iff split: if_split_asm)
      then have "emeasure M (\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 \<open>?D = ?P'\<close> 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 (\j\J. Y' j) = (\ i\J. emeasure M (Y' i))" .
      then show "prob (\j\J. Y' j) = (\ i\J. prob (Y' i))"
        by (auto simp: emeasure_eq_measure prod_ennreal measure_nonneg prod_nonneg)
    qed
  qed
qed

lemma (in prob_space) indep_vars_iff_distr_eq_PiM':
  fixes I :: "'i set" and X :: "'i \ 'a \ 'b"
  assumes "I \ {}"
  assumes rv: "\i. i \ I \ random_variable (M' i) (X i)"
  shows "indep_vars M' X I \
           distr M (\<Pi>\<^sub>M i\<in>I. M' i) (\<lambda>x. \<lambda>i\<in>I. X i x) = (\<Pi>\<^sub>M i\<in>I. distr M (M' i) (X i))"
proof -
  from assms obtain j where j: "j \ I"
    by auto
  define N' where "N' = (\<lambda>i. if i \<in> I then M' i else M' j)"
  define Y where "Y = (\i. if i \ I then X i else X j)"
  have rv: "random_variable (N' i) (Y i)" for i
    using j by (auto simp: N'_def Y_def intro: assms)

  have "indep_vars M' X I = indep_vars N' Y I"
    by (intro indep_vars_cong) (auto simp: N'_def Y_def)
  also have "\ \ distr M (\\<^sub>M i\I. N' i) (\x. \i\I. Y i x) = (\\<^sub>M i\I. distr M (N' i) (Y i))"
    by (intro indep_vars_iff_distr_eq_PiM rv assms)
  also have "(\\<^sub>M i\I. N' i) = (\\<^sub>M i\I. M' i)"
    by (intro PiM_cong) (simp_all add: N'_def)
  also have "(\x. \i\I. Y i x) = (\x. \i\I. X i x)"
    by (simp_all add: Y_def fun_eq_iff)
  also have "(\\<^sub>M i\I. distr M (N' i) (Y i)) = (\\<^sub>M i\I. distr M (M' i) (X i))"
    by (intro PiM_cong distr_cong) (simp_all add: N'_def Y_def)
  finally show ?thesis .
qed

lemma (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 \<inter> space M) * prob (B -` Xb \<inter> space M)"
proof -
  have "prob ((\x. (A x, B x)) -` (Xa \ Xb) \ space M) =
    prob (\<Inter>i\<in>UNIV. (case_bool A B i -` case_bool Xa Xb i \<inter> space M))"
    by (auto intro!: arg_cong[where f=prob] simp: UNIV_bool)
  also have "\ = (\i\UNIV. prob (case_bool A B i -` case_bool 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 .
qed

lemma (in prob_space) prob_indep_random_variable:
  assumes ind[simp]: "indep_var N X N Y"
  assumes [simp]: "A \ sets N" "B \ sets N"
  shows "\

(x in M. X x \ A \ Y x \ B) = \

(x in M. X x \ A) * \

(x in M. Y x \ B)"
proof-
have " \

(x in M. (X x)\A \ (Y x)\ B ) = prob ((\x. (X x, Y x)) -` (A \ B) \ space M)"
    by (auto intro!: arg_cong[where f= prob])
  also have "...= prob (X -` A \ space M) * prob (Y -` B \ space M)"
    by (auto intro!: indep_varD[where Ma=N and Mb=N])
  also have "... = \

(x in M. X x \ A) * \

(x in M. Y x \ B)"
    by (auto intro!: arg_cong2[where f= "(*)"] arg_cong[where f= prob])
  finally show ?thesis .
qed

lemma (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 -
--> --------------------

--> maximum size reached

--> --------------------

quality99%

¤ Dauer der Verarbeitung: 0.30 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.