1.1 --- a/src/HOL/Probability/Independent_Family.thy	Thu May 26 14:12:01 2011 +0200
     1.2 +++ b/src/HOL/Probability/Independent_Family.thy	Thu May 26 14:12:02 2011 +0200
     1.3 @@ -8,6 +8,20 @@
     1.4    imports Probability_Measure
     1.5  begin
     1.6  
     1.7 +lemma INT_decseq_offset:
     1.8 +  assumes "decseq F"
     1.9 +  shows "(\<Inter>i. F i) = (\<Inter>i\<in>{n..}. F i)"
    1.10 +proof safe
    1.11 +  fix x i assume x: "x \<in> (\<Inter>i\<in>{n..}. F i)"
    1.12 +  show "x \<in> F i"
    1.13 +  proof cases
    1.14 +    from x have "x \<in> F n" by auto
    1.15 +    also assume "i \<le> n" with `decseq F` have "F n \<subseteq> F i"
    1.16 +      unfolding decseq_def by simp
    1.17 +    finally show ?thesis .
    1.18 +  qed (insert x, simp)
    1.19 +qed auto
    1.20 +
    1.21  definition (in prob_space)
    1.22    "indep_events A I \<longleftrightarrow> (A`I \<subseteq> events) \<and>
    1.23      (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j)))"
    1.24 @@ -31,6 +45,11 @@
    1.25    "I = J \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> F i = G i) \<Longrightarrow> indep_sets F I \<longleftrightarrow> indep_sets G J"
    1.26    by (simp add: indep_sets_def, intro conj_cong all_cong imp_cong ball_cong) blast+
    1.27  
    1.28 +lemma (in prob_space) indep_sets_singleton_iff_indep_events:
    1.29 +  "indep_sets (\<lambda>i. {F i}) I \<longleftrightarrow> indep_events F I"
    1.30 +  unfolding indep_sets_def indep_events_def
    1.31 +  by (simp, intro conj_cong ball_cong all_cong imp_cong) (auto simp: Pi_iff)
    1.32 +
    1.33  lemma (in prob_space) indep_events_finite_index_events:
    1.34    "indep_events F I \<longleftrightarrow> (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> indep_events F J)"
    1.35    by (auto simp: indep_events_def)
    1.36 @@ -610,4 +629,41 @@
    1.37    then show ?thesis by auto
    1.38  qed
    1.39  
    1.40 +lemma (in prob_space) borel_0_1_law:
    1.41 +  fixes F :: "nat \<Rightarrow> 'a set"
    1.42 +  assumes F: "range F \<subseteq> events" "indep_events F UNIV"
    1.43 +  shows "prob (\<Inter>n. \<Union>m\<in>{n..}. F m) = 0 \<or> prob (\<Inter>n. \<Union>m\<in>{n..}. F m) = 1"
    1.44 +proof (rule kolmogorov_0_1_law[of "\<lambda>i. sigma_sets (space M) { F i }"])
    1.45 +  show "\<And>i. sigma_sets (space M) {F i} \<subseteq> events"
    1.46 +    using F(1) sets_into_space
    1.47 +    by (subst sigma_sets_singleton) auto
    1.48 +  { fix i show "sigma_algebra \<lparr>space = space M, sets = sigma_sets (space M) {F i}\<rparr>"
    1.49 +      using sigma_algebra_sigma[of "\<lparr>space = space M, sets = {F i}\<rparr>"] F sets_into_space
    1.50 +      by (auto simp add: sigma_def) }
    1.51 +  show "indep_sets (\<lambda>i. sigma_sets (space M) {F i}) UNIV"
    1.52 +  proof (rule indep_sets_sigma_sets)
    1.53 +    show "indep_sets (\<lambda>i. {F i}) UNIV"
    1.54 +      unfolding indep_sets_singleton_iff_indep_events by fact
    1.55 +    fix i show "Int_stable \<lparr>space = space M, sets = {F i}\<rparr>"
    1.56 +      unfolding Int_stable_def by simp
    1.57 +  qed
    1.58 +  let "?Q n" = "\<Union>i\<in>{n..}. F i"
    1.59 +  show "(\<Inter>n. \<Union>m\<in>{n..}. F m) \<in> terminal_events (\<lambda>i. sigma_sets (space M) {F i})"
    1.60 +    unfolding terminal_events_def
    1.61 +  proof
    1.62 +    fix j
    1.63 +    interpret S: sigma_algebra "sigma \<lparr> space = space M, sets = (\<Union>i\<in>{j..}. sigma_sets (space M) {F i})\<rparr>"
    1.64 +      using order_trans[OF F(1) space_closed]
    1.65 +      by (intro sigma_algebra_sigma) (simp add: sigma_sets_singleton subset_eq)
    1.66 +    have "(\<Inter>n. ?Q n) = (\<Inter>n\<in>{j..}. ?Q n)"
    1.67 +      by (intro decseq_SucI INT_decseq_offset UN_mono) auto
    1.68 +    also have "\<dots> \<in> sets (sigma \<lparr> space = space M, sets = (\<Union>i\<in>{j..}. sigma_sets (space M) {F i})\<rparr>)"
    1.69 +      using order_trans[OF F(1) space_closed]
    1.70 +      by (safe intro!: S.countable_INT S.countable_UN)
    1.71 +         (auto simp: sets_sigma sigma_sets_singleton intro!: sigma_sets.Basic bexI)
    1.72 +    finally show "(\<Inter>n. ?Q n) \<in> sigma_sets (space M) (\<Union>i\<in>{j..}. sigma_sets (space M) {F i})"
    1.73 +      by (simp add: sets_sigma)
    1.74 +  qed
    1.75 +qed
    1.76 +
    1.77  end