# HG changeset patch
# User hoelzl
# Date 1306411918 -7200
# Node ID fa0ac7bee9ac1e5301ec286b3c914b667605491c
# Parent fe7f5a26e4c63e2e21f0221b07bec7a40d715394
add lemma kolmogorov_0_1_law
diff -r fe7f5a26e4c6 -r fa0ac7bee9ac src/HOL/Probability/Independent_Family.thy
--- a/src/HOL/Probability/Independent_Family.thy Thu May 26 14:11:57 2011 +0200
+++ b/src/HOL/Probability/Independent_Family.thy Thu May 26 14:11:58 2011 +0200
@@ -75,6 +75,32 @@
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 `J \ {}` 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 "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 \ sets M"
+ and indep_setD_ev2: "B \ sets M"
+ using indep unfolding indep_set_def indep_sets_def UNIV_bool by auto
+
lemma dynkin_systemI':
assumes 1: "\ A. A \ sets M \ A \ space M"
assumes empty: "{} \ sets M"
@@ -421,4 +447,167 @@
by (simp cong: indep_sets_cong)
qed
+definition (in prob_space) terminal_events where
+ "terminal_events A = (\n. sigma_sets (space M) (UNION {n..} A))"
+
+lemma (in prob_space) terminal_events_sets:
+ assumes A: "\i. A i \ sets M"
+ assumes "\i::nat. sigma_algebra \space = space M, sets = A i\"
+ assumes X: "X \ terminal_events A"
+ shows "X \ sets M"
+proof -
+ let ?A = "(\n. sigma_sets (space M) (UNION {n..} A))"
+ interpret A: sigma_algebra "\space = space M, sets = A i\" for i by fact
+ from X have "\n. X \ sigma_sets (space M) (UNION {n..} A)" by (auto simp: terminal_events_def)
+ from this[of 0] have "X \ sigma_sets (space M) (UNION UNIV A)" by simp
+ then show "X \ sets M"
+ by induct (insert A, auto)
+qed
+
+lemma (in prob_space) sigma_algebra_terminal_events:
+ assumes "\i::nat. sigma_algebra \space = space M, sets = A i\"
+ shows "sigma_algebra \ space = space M, sets = terminal_events A \"
+ unfolding terminal_events_def
+proof (simp add: sigma_algebra_iff2, safe)
+ let ?A = "(\n. sigma_sets (space M) (UNION {n..} A))"
+ interpret A: sigma_algebra "\space = space M, sets = 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 A: "\i. A i \ sets M"
+ assumes "\i::nat. sigma_algebra \space = space M, sets = A i\"
+ assumes indep: "indep_sets A UNIV"
+ and X: "X \ terminal_events A"
+ shows "prob X = 0 \ prob X = 1"
+proof -
+ let ?D = "\ space = space M, sets = {D \ sets M. prob (X \ D) = prob X * prob D} \"
+ interpret A: sigma_algebra "\space = space M, sets = A i\" for i by fact
+ interpret T: sigma_algebra "\ space = space M, sets = terminal_events A \"
+ by (rule sigma_algebra_terminal_events) fact
+ have "X \ space M" using T.space_closed X by auto
+
+ have X_in: "X \ sets M"
+ by (rule terminal_events_sets) fact+
+
+ interpret D: dynkin_system ?D
+ proof (rule dynkin_systemI)
+ fix D assume "D \ sets ?D" then show "D \ space ?D"
+ using sets_into_space by auto
+ next
+ show "space ?D \ sets ?D"
+ using prob_space `X \ space M` by (simp add: Int_absorb2)
+ next
+ fix A assume A: "A \ sets ?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_into_space
+ by (subst finite_measure_Diff) (auto simp: field_simps)
+ finally show "space ?D - A \ sets ?D"
+ using A `X \ space M` by auto
+ next
+ fix F :: "nat \ 'a set" assume dis: "disjoint_family F" and "range F \ sets ?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 mult_right.sums 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) \ sets ?D"
+ by auto
+ qed
+
+ { fix n
+ have "indep_sets (\b. sigma_sets (space M) (\m\bool_case {..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 (bool_case {..n} {Suc n..})"
+ unfolding disjoint_family_on_def by (auto split: bool.split)
+ fix m
+ show "Int_stable \space = space M, sets = A m\"
+ unfolding Int_stable_def using A.Int by auto
+ qed
+ also have "(\b. sigma_sets (space M) (\m\bool_case {..n} {Suc n..} b. A m)) =
+ bool_case (sigma_sets (space M) (\m\{..n}. A m)) (sigma_sets (space M) (\m\{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) \ sets ?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 terminal_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)) \ sets ?D" (is "?A \ _")
+ by auto
+
+ have "sigma \ space = space M, sets = ?A \ =
+ dynkin \ space = space M, sets = ?A \" (is "sigma ?UA = dynkin ?UA")
+ 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_into_space, auto) }
+ then show "sets ?UA \ Pow (space ?UA)" by auto
+ show "Int_stable ?UA"
+ 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 "sigma \space = space M, sets = (\i\{..max m n}. A i)\"
+ using A sets_into_space by (intro sigma_algebra_sigma) 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 add: sets_sigma)
+ then show "a \ b \ (\n. sigma_sets (space M) (\i\{..n}. A i))" by auto
+ qed
+ qed
+ moreover have "sets (dynkin ?UA) \ sets ?D"
+ proof (rule D.dynkin_subset)
+ show "sets ?UA \ sets ?D" using `?A \ sets ?D` by auto
+ qed simp
+ ultimately have "sets (sigma ?UA) \ sets ?D" by simp
+ moreover
+ have "\n. sigma_sets (space M) (\i\{n..}. A i) \ sigma_sets (space M) ?A"
+ by (intro sigma_sets_subseteq UN_mono) (auto intro: sigma_sets.Basic)
+ then have "terminal_events A \ sets (sigma ?UA)"
+ unfolding sets_sigma terminal_events_def by auto
+ moreover note `X \ terminal_events A`
+ ultimately have "X \ sets ?D" by auto
+ then show ?thesis by auto
+qed
+
end