src/HOL/Probability/Independent_Family.thy
changeset 42982 fa0ac7bee9ac
parent 42981 fe7f5a26e4c6
child 42983 685df9c0626d
     1.1 --- a/src/HOL/Probability/Independent_Family.thy	Thu May 26 14:11:57 2011 +0200
     1.2 +++ b/src/HOL/Probability/Independent_Family.thy	Thu May 26 14:11:58 2011 +0200
     1.3 @@ -75,6 +75,32 @@
     1.4    shows "prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))"
     1.5    using assms unfolding indep_sets_def by auto
     1.6  
     1.7 +lemma (in prob_space) indep_setI:
     1.8 +  assumes ev: "A \<subseteq> events" "B \<subseteq> events"
     1.9 +    and indep: "\<And>a b. a \<in> A \<Longrightarrow> b \<in> B \<Longrightarrow> prob (a \<inter> b) = prob a * prob b"
    1.10 +  shows "indep_set A B"
    1.11 +  unfolding indep_set_def
    1.12 +proof (rule indep_setsI)
    1.13 +  fix F J assume "J \<noteq> {}" "J \<subseteq> UNIV"
    1.14 +    and F: "\<forall>j\<in>J. F j \<in> (case j of True \<Rightarrow> A | False \<Rightarrow> B)"
    1.15 +  have "J \<in> Pow UNIV" by auto
    1.16 +  with F `J \<noteq> {}` indep[of "F True" "F False"]
    1.17 +  show "prob (\<Inter>j\<in>J. F j) = (\<Prod>j\<in>J. prob (F j))"
    1.18 +    unfolding UNIV_bool Pow_insert by (auto simp: ac_simps)
    1.19 +qed (auto split: bool.split simp: ev)
    1.20 +
    1.21 +lemma (in prob_space) indep_setD:
    1.22 +  assumes indep: "indep_set A B" and ev: "a \<in> A" "b \<in> B"
    1.23 +  shows "prob (a \<inter> b) = prob a * prob b"
    1.24 +  using indep[unfolded indep_set_def, THEN indep_setsD, of UNIV "bool_case a b"] ev
    1.25 +  by (simp add: ac_simps UNIV_bool)
    1.26 +
    1.27 +lemma (in prob_space)
    1.28 +  assumes indep: "indep_set A B"
    1.29 +  shows indep_setD_ev1: "A \<subseteq> sets M"
    1.30 +    and indep_setD_ev2: "B \<subseteq> sets M"
    1.31 +  using indep unfolding indep_set_def indep_sets_def UNIV_bool by auto
    1.32 +
    1.33  lemma dynkin_systemI':
    1.34    assumes 1: "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M"
    1.35    assumes empty: "{} \<in> sets M"
    1.36 @@ -421,4 +447,167 @@
    1.37      by (simp cong: indep_sets_cong)
    1.38  qed
    1.39  
    1.40 +definition (in prob_space) terminal_events where
    1.41 +  "terminal_events A = (\<Inter>n. sigma_sets (space M) (UNION {n..} A))"
    1.42 +
    1.43 +lemma (in prob_space) terminal_events_sets:
    1.44 +  assumes A: "\<And>i. A i \<subseteq> sets M"
    1.45 +  assumes "\<And>i::nat. sigma_algebra \<lparr>space = space M, sets = A i\<rparr>"
    1.46 +  assumes X: "X \<in> terminal_events A"
    1.47 +  shows "X \<in> sets M"
    1.48 +proof -
    1.49 +  let ?A = "(\<Inter>n. sigma_sets (space M) (UNION {n..} A))"
    1.50 +  interpret A: sigma_algebra "\<lparr>space = space M, sets = A i\<rparr>" for i by fact
    1.51 +  from X have "\<And>n. X \<in> sigma_sets (space M) (UNION {n..} A)" by (auto simp: terminal_events_def)
    1.52 +  from this[of 0] have "X \<in> sigma_sets (space M) (UNION UNIV A)" by simp
    1.53 +  then show "X \<in> sets M"
    1.54 +    by induct (insert A, auto)
    1.55 +qed
    1.56 +
    1.57 +lemma (in prob_space) sigma_algebra_terminal_events:
    1.58 +  assumes "\<And>i::nat. sigma_algebra \<lparr>space = space M, sets = A i\<rparr>"
    1.59 +  shows "sigma_algebra \<lparr> space = space M, sets = terminal_events A \<rparr>"
    1.60 +  unfolding terminal_events_def
    1.61 +proof (simp add: sigma_algebra_iff2, safe)
    1.62 +  let ?A = "(\<Inter>n. sigma_sets (space M) (UNION {n..} A))"
    1.63 +  interpret A: sigma_algebra "\<lparr>space = space M, sets = A i\<rparr>" for i by fact
    1.64 +  { fix X x assume "X \<in> ?A" "x \<in> X" 
    1.65 +    then have "\<And>n. X \<in> sigma_sets (space M) (UNION {n..} A)" by auto
    1.66 +    from this[of 0] have "X \<in> sigma_sets (space M) (UNION UNIV A)" by simp
    1.67 +    then have "X \<subseteq> space M"
    1.68 +      by induct (insert A.sets_into_space, auto)
    1.69 +    with `x \<in> X` show "x \<in> space M" by auto }
    1.70 +  { fix F :: "nat \<Rightarrow> 'a set" and n assume "range F \<subseteq> ?A"
    1.71 +    then show "(UNION UNIV F) \<in> sigma_sets (space M) (UNION {n..} A)"
    1.72 +      by (intro sigma_sets.Union) auto }
    1.73 +qed (auto intro!: sigma_sets.Compl sigma_sets.Empty)
    1.74 +
    1.75 +lemma (in prob_space) kolmogorov_0_1_law:
    1.76 +  fixes A :: "nat \<Rightarrow> 'a set set"
    1.77 +  assumes A: "\<And>i. A i \<subseteq> sets M"
    1.78 +  assumes "\<And>i::nat. sigma_algebra \<lparr>space = space M, sets = A i\<rparr>"
    1.79 +  assumes indep: "indep_sets A UNIV"
    1.80 +  and X: "X \<in> terminal_events A"
    1.81 +  shows "prob X = 0 \<or> prob X = 1"
    1.82 +proof -
    1.83 +  let ?D = "\<lparr> space = space M, sets = {D \<in> sets M. prob (X \<inter> D) = prob X * prob D} \<rparr>"
    1.84 +  interpret A: sigma_algebra "\<lparr>space = space M, sets = A i\<rparr>" for i by fact
    1.85 +  interpret T: sigma_algebra "\<lparr> space = space M, sets = terminal_events A \<rparr>"
    1.86 +    by (rule sigma_algebra_terminal_events) fact
    1.87 +  have "X \<subseteq> space M" using T.space_closed X by auto
    1.88 +
    1.89 +  have X_in: "X \<in> sets M"
    1.90 +    by (rule terminal_events_sets) fact+
    1.91 +
    1.92 +  interpret D: dynkin_system ?D
    1.93 +  proof (rule dynkin_systemI)
    1.94 +    fix D assume "D \<in> sets ?D" then show "D \<subseteq> space ?D"
    1.95 +      using sets_into_space by auto
    1.96 +  next
    1.97 +    show "space ?D \<in> sets ?D"
    1.98 +      using prob_space `X \<subseteq> space M` by (simp add: Int_absorb2)
    1.99 +  next
   1.100 +    fix A assume A: "A \<in> sets ?D"
   1.101 +    have "prob (X \<inter> (space M - A)) = prob (X - (X \<inter> A))"
   1.102 +      using `X \<subseteq> space M` by (auto intro!: arg_cong[where f=prob])
   1.103 +    also have "\<dots> = prob X - prob (X \<inter> A)"
   1.104 +      using X_in A by (intro finite_measure_Diff) auto
   1.105 +    also have "\<dots> = prob X * prob (space M) - prob X * prob A"
   1.106 +      using A prob_space by auto
   1.107 +    also have "\<dots> = prob X * prob (space M - A)"
   1.108 +      using X_in A sets_into_space
   1.109 +      by (subst finite_measure_Diff) (auto simp: field_simps)
   1.110 +    finally show "space ?D - A \<in> sets ?D"
   1.111 +      using A `X \<subseteq> space M` by auto
   1.112 +  next
   1.113 +    fix F :: "nat \<Rightarrow> 'a set" assume dis: "disjoint_family F" and "range F \<subseteq> sets ?D"
   1.114 +    then have F: "range F \<subseteq> events" "\<And>i. prob (X \<inter> F i) = prob X * prob (F i)"
   1.115 +      by auto
   1.116 +    have "(\<lambda>i. prob (X \<inter> F i)) sums prob (\<Union>i. X \<inter> F i)"
   1.117 +    proof (rule finite_measure_UNION)
   1.118 +      show "range (\<lambda>i. X \<inter> F i) \<subseteq> events"
   1.119 +        using F X_in by auto
   1.120 +      show "disjoint_family (\<lambda>i. X \<inter> F i)"
   1.121 +        using dis by (rule disjoint_family_on_bisimulation) auto
   1.122 +    qed
   1.123 +    with F have "(\<lambda>i. prob X * prob (F i)) sums prob (X \<inter> (\<Union>i. F i))"
   1.124 +      by simp
   1.125 +    moreover have "(\<lambda>i. prob X * prob (F i)) sums (prob X * prob (\<Union>i. F i))"
   1.126 +      by (intro mult_right.sums finite_measure_UNION F dis)
   1.127 +    ultimately have "prob (X \<inter> (\<Union>i. F i)) = prob X * prob (\<Union>i. F i)"
   1.128 +      by (auto dest!: sums_unique)
   1.129 +    with F show "(\<Union>i. F i) \<in> sets ?D"
   1.130 +      by auto
   1.131 +  qed
   1.132 +
   1.133 +  { fix n
   1.134 +    have "indep_sets (\<lambda>b. sigma_sets (space M) (\<Union>m\<in>bool_case {..n} {Suc n..} b. A m)) UNIV"
   1.135 +    proof (rule indep_sets_collect_sigma)
   1.136 +      have *: "(\<Union>b. case b of True \<Rightarrow> {..n} | False \<Rightarrow> {Suc n..}) = UNIV" (is "?U = _")
   1.137 +        by (simp split: bool.split add: set_eq_iff) (metis not_less_eq_eq)
   1.138 +      with indep show "indep_sets A ?U" by simp
   1.139 +      show "disjoint_family (bool_case {..n} {Suc n..})"
   1.140 +        unfolding disjoint_family_on_def by (auto split: bool.split)
   1.141 +      fix m
   1.142 +      show "Int_stable \<lparr>space = space M, sets = A m\<rparr>"
   1.143 +        unfolding Int_stable_def using A.Int by auto
   1.144 +    qed
   1.145 +    also have "(\<lambda>b. sigma_sets (space M) (\<Union>m\<in>bool_case {..n} {Suc n..} b. A m)) = 
   1.146 +      bool_case (sigma_sets (space M) (\<Union>m\<in>{..n}. A m)) (sigma_sets (space M) (\<Union>m\<in>{Suc n..}. A m))"
   1.147 +      by (auto intro!: ext split: bool.split)
   1.148 +    finally have indep: "indep_set (sigma_sets (space M) (\<Union>m\<in>{..n}. A m)) (sigma_sets (space M) (\<Union>m\<in>{Suc n..}. A m))"
   1.149 +      unfolding indep_set_def by simp
   1.150 +
   1.151 +    have "sigma_sets (space M) (\<Union>m\<in>{..n}. A m) \<subseteq> sets ?D"
   1.152 +    proof (simp add: subset_eq, rule)
   1.153 +      fix D assume D: "D \<in> sigma_sets (space M) (\<Union>m\<in>{..n}. A m)"
   1.154 +      have "X \<in> sigma_sets (space M) (\<Union>m\<in>{Suc n..}. A m)"
   1.155 +        using X unfolding terminal_events_def by simp
   1.156 +      from indep_setD[OF indep D this] indep_setD_ev1[OF indep] D
   1.157 +      show "D \<in> events \<and> prob (X \<inter> D) = prob X * prob D"
   1.158 +        by (auto simp add: ac_simps)
   1.159 +    qed }
   1.160 +  then have "(\<Union>n. sigma_sets (space M) (\<Union>m\<in>{..n}. A m)) \<subseteq> sets ?D" (is "?A \<subseteq> _")
   1.161 +    by auto
   1.162 +
   1.163 +  have "sigma \<lparr> space = space M, sets = ?A \<rparr> =
   1.164 +    dynkin \<lparr> space = space M, sets = ?A \<rparr>" (is "sigma ?UA = dynkin ?UA")
   1.165 +  proof (rule sigma_eq_dynkin)
   1.166 +    { fix B n assume "B \<in> sigma_sets (space M) (\<Union>m\<in>{..n}. A m)"
   1.167 +      then have "B \<subseteq> space M"
   1.168 +        by induct (insert A sets_into_space, auto) }
   1.169 +    then show "sets ?UA \<subseteq> Pow (space ?UA)" by auto
   1.170 +    show "Int_stable ?UA"
   1.171 +    proof (rule Int_stableI)
   1.172 +      fix a assume "a \<in> ?A" then guess n .. note a = this
   1.173 +      fix b assume "b \<in> ?A" then guess m .. note b = this
   1.174 +      interpret Amn: sigma_algebra "sigma \<lparr>space = space M, sets = (\<Union>i\<in>{..max m n}. A i)\<rparr>"
   1.175 +        using A sets_into_space by (intro sigma_algebra_sigma) auto
   1.176 +      have "sigma_sets (space M) (\<Union>i\<in>{..n}. A i) \<subseteq> sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)"
   1.177 +        by (intro sigma_sets_subseteq UN_mono) auto
   1.178 +      with a have "a \<in> sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)" by auto
   1.179 +      moreover
   1.180 +      have "sigma_sets (space M) (\<Union>i\<in>{..m}. A i) \<subseteq> sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)"
   1.181 +        by (intro sigma_sets_subseteq UN_mono) auto
   1.182 +      with b have "b \<in> sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)" by auto
   1.183 +      ultimately have "a \<inter> b \<in> sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)"
   1.184 +        using Amn.Int[of a b] by (simp add: sets_sigma)
   1.185 +      then show "a \<inter> b \<in> (\<Union>n. sigma_sets (space M) (\<Union>i\<in>{..n}. A i))" by auto
   1.186 +    qed
   1.187 +  qed
   1.188 +  moreover have "sets (dynkin ?UA) \<subseteq> sets ?D"
   1.189 +  proof (rule D.dynkin_subset)
   1.190 +    show "sets ?UA \<subseteq> sets ?D" using `?A \<subseteq> sets ?D` by auto
   1.191 +  qed simp
   1.192 +  ultimately have "sets (sigma ?UA) \<subseteq> sets ?D" by simp
   1.193 +  moreover
   1.194 +  have "\<And>n. sigma_sets (space M) (\<Union>i\<in>{n..}. A i) \<subseteq> sigma_sets (space M) ?A"
   1.195 +    by (intro sigma_sets_subseteq UN_mono) (auto intro: sigma_sets.Basic)
   1.196 +  then have "terminal_events A \<subseteq> sets (sigma ?UA)"
   1.197 +    unfolding sets_sigma terminal_events_def by auto
   1.198 +  moreover note `X \<in> terminal_events A`
   1.199 +  ultimately have "X \<in> sets ?D" by auto
   1.200 +  then show ?thesis by auto
   1.201 +qed
   1.202 +
   1.203  end