src/HOL/Probability/Independent_Family.thy
changeset 49781 59b219ca3513
parent 49776 199d1d5bb17e
child 49784 5e5b2da42a69
     1.1 --- a/src/HOL/Probability/Independent_Family.thy	Wed Oct 10 12:12:21 2012 +0200
     1.2 +++ b/src/HOL/Probability/Independent_Family.thy	Wed Oct 10 12:12:21 2012 +0200
     1.3 @@ -335,6 +335,18 @@
     1.4      by (rule indep_sets_mono_sets) (intro subsetI sigma_sets.Basic)
     1.5  qed
     1.6  
     1.7 +lemma (in prob_space)
     1.8 +  "indep_vars M' X I \<longleftrightarrow>
     1.9 +    (\<forall>i\<in>I. random_variable (M' i) (X i)) \<and>
    1.10 +    indep_sets (\<lambda>i. { X i -` A \<inter> space M | A. A \<in> sets (M' i)}) I"
    1.11 +  unfolding indep_vars_def
    1.12 +  apply (rule conj_cong[OF refl])
    1.13 +  apply (rule indep_sets_sigma_sets_iff)
    1.14 +  apply (auto simp: Int_stable_def)
    1.15 +  apply (rule_tac x="A \<inter> Aa" in exI)
    1.16 +  apply auto
    1.17 +  done
    1.18 +
    1.19  lemma (in prob_space) indep_sets2_eq:
    1.20    "indep_set A B \<longleftrightarrow> A \<subseteq> events \<and> B \<subseteq> events \<and> (\<forall>a\<in>A. \<forall>b\<in>B. prob (a \<inter> b) = prob a * prob b)"
    1.21    unfolding indep_set_def
    1.22 @@ -512,12 +524,14 @@
    1.23  
    1.24  lemma (in prob_space) kolmogorov_0_1_law:
    1.25    fixes A :: "nat \<Rightarrow> 'a set set"
    1.26 -  assumes A: "\<And>i. A i \<subseteq> events"
    1.27    assumes "\<And>i::nat. sigma_algebra (space M) (A i)"
    1.28    assumes indep: "indep_sets A UNIV"
    1.29    and X: "X \<in> tail_events A"
    1.30    shows "prob X = 0 \<or> prob X = 1"
    1.31  proof -
    1.32 +  have A: "\<And>i. A i \<subseteq> events"
    1.33 +    using indep unfolding indep_sets_def by simp
    1.34 +
    1.35    let ?D = "{D \<in> events. prob (X \<inter> D) = prob X * prob D}"
    1.36    interpret A: sigma_algebra "space M" "A i" for i by fact
    1.37    interpret T: sigma_algebra "space M" "tail_events A"
    1.38 @@ -635,14 +649,13 @@
    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 +  assumes F2: "indep_events F UNIV"
    1.44    shows "prob (\<Inter>n. \<Union>m\<in>{n..}. F m) = 0 \<or> prob (\<Inter>n. \<Union>m\<in>{n..}. F m) = 1"
    1.45  proof (rule kolmogorov_0_1_law[of "\<lambda>i. sigma_sets (space M) { F i }"])
    1.46 -  show "\<And>i. sigma_sets (space M) {F i} \<subseteq> events"
    1.47 -    using F(1) sets_into_space
    1.48 -    by (subst sigma_sets_singleton) auto
    1.49 +  have F1: "range F \<subseteq> events"
    1.50 +    using F2 by (simp add: indep_events_def subset_eq)
    1.51    { fix i show "sigma_algebra (space M) (sigma_sets (space M) {F i})"
    1.52 -      using sigma_algebra_sigma_sets[of "{F i}" "space M"] F sets_into_space
    1.53 +      using sigma_algebra_sigma_sets[of "{F i}" "space M"] F1 sets_into_space
    1.54        by auto }
    1.55    show "indep_sets (\<lambda>i. sigma_sets (space M) {F i}) UNIV"
    1.56    proof (rule indep_sets_sigma)
    1.57 @@ -657,12 +670,12 @@
    1.58    proof
    1.59      fix j
    1.60      interpret S: sigma_algebra "space M" "sigma_sets (space M) (\<Union>i\<in>{j..}. sigma_sets (space M) {F i})"
    1.61 -      using order_trans[OF F(1) space_closed]
    1.62 +      using order_trans[OF F1 space_closed]
    1.63        by (intro sigma_algebra_sigma_sets) (simp add: sigma_sets_singleton subset_eq)
    1.64      have "(\<Inter>n. ?Q n) = (\<Inter>n\<in>{j..}. ?Q n)"
    1.65        by (intro decseq_SucI INT_decseq_offset UN_mono) auto
    1.66      also have "\<dots> \<in> sigma_sets (space M) (\<Union>i\<in>{j..}. sigma_sets (space M) {F i})"
    1.67 -      using order_trans[OF F(1) space_closed]
    1.68 +      using order_trans[OF F1 space_closed]
    1.69        by (safe intro!: S.countable_INT S.countable_UN)
    1.70           (auto simp: sigma_sets_singleton intro!: sigma_sets.Basic bexI)
    1.71      finally show "(\<Inter>n. ?Q n) \<in> sigma_sets (space M) (\<Union>i\<in>{j..}. sigma_sets (space M) {F i})"