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