src/HOL/Probability/Independent_Family.thy
changeset 49772 75660d89c339
parent 47694 05663f75964c
child 49776 199d1d5bb17e
     1.1 --- a/src/HOL/Probability/Independent_Family.thy	Wed Oct 10 10:48:55 2012 +0200
     1.2 +++ b/src/HOL/Probability/Independent_Family.thy	Wed Oct 10 12:12:14 2012 +0200
     1.3 @@ -86,6 +86,15 @@
     1.4      using indep by (auto simp: indep_sets_def)
     1.5  qed
     1.6  
     1.7 +lemma (in prob_space) indep_sets_mono:
     1.8 +  assumes indep: "indep_sets F I"
     1.9 +  assumes mono: "J \<subseteq> I" "\<And>i. i\<in>J \<Longrightarrow> G i \<subseteq> F i"
    1.10 +  shows "indep_sets G J"
    1.11 +  apply (rule indep_sets_mono_sets)
    1.12 +  apply (rule indep_sets_mono_index)
    1.13 +  apply (fact +)
    1.14 +  done
    1.15 +
    1.16  lemma (in prob_space) indep_setsI:
    1.17    assumes "\<And>i. i \<in> I \<Longrightarrow> F i \<subseteq> events"
    1.18      and "\<And>A J. J \<noteq> {} \<Longrightarrow> J \<subseteq> I \<Longrightarrow> finite J \<Longrightarrow> (\<forall>j\<in>J. A j \<in> F j) \<Longrightarrow> prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))"
    1.19 @@ -468,27 +477,25 @@
    1.20      by (simp cong: indep_sets_cong)
    1.21  qed
    1.22  
    1.23 -definition (in prob_space) terminal_events where
    1.24 -  "terminal_events A = (\<Inter>n. sigma_sets (space M) (UNION {n..} A))"
    1.25 +definition (in prob_space) tail_events where
    1.26 +  "tail_events A = (\<Inter>n. sigma_sets (space M) (UNION {n..} A))"
    1.27  
    1.28 -lemma (in prob_space) terminal_events_sets:
    1.29 -  assumes A: "\<And>i. A i \<subseteq> events"
    1.30 -  assumes "\<And>i::nat. sigma_algebra (space M) (A i)"
    1.31 -  assumes X: "X \<in> terminal_events A"
    1.32 -  shows "X \<in> events"
    1.33 -proof -
    1.34 +lemma (in prob_space) tail_events_sets:
    1.35 +  assumes A: "\<And>i::nat. A i \<subseteq> events"
    1.36 +  shows "tail_events A \<subseteq> events"
    1.37 +proof
    1.38 +  fix X assume X: "X \<in> tail_events A"
    1.39    let ?A = "(\<Inter>n. sigma_sets (space M) (UNION {n..} A))"
    1.40 -  interpret A: sigma_algebra "space M" "A i" for i by fact
    1.41 -  from X have "\<And>n. X \<in> sigma_sets (space M) (UNION {n..} A)" by (auto simp: terminal_events_def)
    1.42 +  from X have "\<And>n::nat. X \<in> sigma_sets (space M) (UNION {n..} A)" by (auto simp: tail_events_def)
    1.43    from this[of 0] have "X \<in> sigma_sets (space M) (UNION UNIV A)" by simp
    1.44    then show "X \<in> events"
    1.45      by induct (insert A, auto)
    1.46  qed
    1.47  
    1.48 -lemma (in prob_space) sigma_algebra_terminal_events:
    1.49 +lemma (in prob_space) sigma_algebra_tail_events:
    1.50    assumes "\<And>i::nat. sigma_algebra (space M) (A i)"
    1.51 -  shows "sigma_algebra (space M) (terminal_events A)"
    1.52 -  unfolding terminal_events_def
    1.53 +  shows "sigma_algebra (space M) (tail_events A)"
    1.54 +  unfolding tail_events_def
    1.55  proof (simp add: sigma_algebra_iff2, safe)
    1.56    let ?A = "(\<Inter>n. sigma_sets (space M) (UNION {n..} A))"
    1.57    interpret A: sigma_algebra "space M" "A i" for i by fact
    1.58 @@ -508,17 +515,17 @@
    1.59    assumes A: "\<And>i. A i \<subseteq> events"
    1.60    assumes "\<And>i::nat. sigma_algebra (space M) (A i)"
    1.61    assumes indep: "indep_sets A UNIV"
    1.62 -  and X: "X \<in> terminal_events A"
    1.63 +  and X: "X \<in> tail_events A"
    1.64    shows "prob X = 0 \<or> prob X = 1"
    1.65  proof -
    1.66    let ?D = "{D \<in> events. prob (X \<inter> D) = prob X * prob D}"
    1.67    interpret A: sigma_algebra "space M" "A i" for i by fact
    1.68 -  interpret T: sigma_algebra "space M" "terminal_events A"
    1.69 -    by (rule sigma_algebra_terminal_events) fact
    1.70 +  interpret T: sigma_algebra "space M" "tail_events A"
    1.71 +    by (rule sigma_algebra_tail_events) fact
    1.72    have "X \<subseteq> space M" using T.space_closed X by auto
    1.73  
    1.74    have X_in: "X \<in> events"
    1.75 -    by (rule terminal_events_sets) fact+
    1.76 +    using tail_events_sets A X by auto
    1.77  
    1.78    interpret D: dynkin_system "space M" ?D
    1.79    proof (rule dynkin_systemI)
    1.80 @@ -583,7 +590,7 @@
    1.81      proof (simp add: subset_eq, rule)
    1.82        fix D assume D: "D \<in> sigma_sets (space M) (\<Union>m\<in>{..n}. A m)"
    1.83        have "X \<in> sigma_sets (space M) (\<Union>m\<in>{Suc n..}. A m)"
    1.84 -        using X unfolding terminal_events_def by simp
    1.85 +        using X unfolding tail_events_def by simp
    1.86        from indep_setD[OF indep D this] indep_setD_ev1[OF indep] D
    1.87        show "D \<in> events \<and> prob (X \<inter> D) = prob X * prob D"
    1.88          by (auto simp add: ac_simps)
    1.89 @@ -591,12 +598,12 @@
    1.90    then have "(\<Union>n. sigma_sets (space M) (\<Union>m\<in>{..n}. A m)) \<subseteq> ?D" (is "?A \<subseteq> _")
    1.91      by auto
    1.92  
    1.93 -  note `X \<in> terminal_events A`
    1.94 +  note `X \<in> tail_events A`
    1.95    also {
    1.96      have "\<And>n. sigma_sets (space M) (\<Union>i\<in>{n..}. A i) \<subseteq> sigma_sets (space M) ?A"
    1.97        by (intro sigma_sets_subseteq UN_mono) auto
    1.98 -   then have "terminal_events A \<subseteq> sigma_sets (space M) ?A"
    1.99 -      unfolding terminal_events_def by auto }
   1.100 +   then have "tail_events A \<subseteq> sigma_sets (space M) ?A"
   1.101 +      unfolding tail_events_def by auto }
   1.102    also have "sigma_sets (space M) ?A = dynkin (space M) ?A"
   1.103    proof (rule sigma_eq_dynkin)
   1.104      { fix B n assume "B \<in> sigma_sets (space M) (\<Union>m\<in>{..n}. A m)"
   1.105 @@ -645,8 +652,8 @@
   1.106        unfolding Int_stable_def by simp
   1.107    qed
   1.108    let ?Q = "\<lambda>n. \<Union>i\<in>{n..}. F i"
   1.109 -  show "(\<Inter>n. \<Union>m\<in>{n..}. F m) \<in> terminal_events (\<lambda>i. sigma_sets (space M) {F i})"
   1.110 -    unfolding terminal_events_def
   1.111 +  show "(\<Inter>n. \<Union>m\<in>{n..}. F m) \<in> tail_events (\<lambda>i. sigma_sets (space M) {F i})"
   1.112 +    unfolding tail_events_def
   1.113    proof
   1.114      fix j
   1.115      interpret S: sigma_algebra "space M" "sigma_sets (space M) (\<Union>i\<in>{j..}. sigma_sets (space M) {F i})"