src/HOL/Probability/Measure_Space.thy
changeset 50244 de72bbe42190
parent 50104 de19856feb54
child 50387 3d8863c41fe8
     1.1 --- a/src/HOL/Probability/Measure_Space.thy	Thu Nov 22 10:09:54 2012 +0100
     1.2 +++ b/src/HOL/Probability/Measure_Space.thy	Tue Nov 27 11:29:47 2012 +0100
     1.3 @@ -449,11 +449,11 @@
     1.4  
     1.5  lemma suminf_emeasure:
     1.6    "range A \<subseteq> sets M \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Sum>i. emeasure M (A i)) = emeasure M (\<Union>i. A i)"
     1.7 -  using countable_UN[of A UNIV M] emeasure_countably_additive[of M]
     1.8 +  using sets.countable_UN[of A UNIV M] emeasure_countably_additive[of M]
     1.9    by (simp add: countably_additive_def)
    1.10  
    1.11  lemma emeasure_additive: "additive (sets M) (emeasure M)"
    1.12 -  by (metis countably_additive_additive emeasure_positive emeasure_countably_additive)
    1.13 +  by (metis sets.countably_additive_additive emeasure_positive emeasure_countably_additive)
    1.14  
    1.15  lemma plus_emeasure:
    1.16    "a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<inter> b = {} \<Longrightarrow> emeasure M a + emeasure M b = emeasure M (a \<union> b)"
    1.17 @@ -462,16 +462,16 @@
    1.18  lemma setsum_emeasure:
    1.19    "F`I \<subseteq> sets M \<Longrightarrow> disjoint_family_on F I \<Longrightarrow> finite I \<Longrightarrow>
    1.20      (\<Sum>i\<in>I. emeasure M (F i)) = emeasure M (\<Union>i\<in>I. F i)"
    1.21 -  by (metis additive_sum emeasure_positive emeasure_additive)
    1.22 +  by (metis sets.additive_sum emeasure_positive emeasure_additive)
    1.23  
    1.24  lemma emeasure_mono:
    1.25    "a \<subseteq> b \<Longrightarrow> b \<in> sets M \<Longrightarrow> emeasure M a \<le> emeasure M b"
    1.26 -  by (metis additive_increasing emeasure_additive emeasure_nonneg emeasure_notin_sets
    1.27 +  by (metis sets.additive_increasing emeasure_additive emeasure_nonneg emeasure_notin_sets
    1.28              emeasure_positive increasingD)
    1.29  
    1.30  lemma emeasure_space:
    1.31    "emeasure M A \<le> emeasure M (space M)"
    1.32 -  by (metis emeasure_mono emeasure_nonneg emeasure_notin_sets sets_into_space top)
    1.33 +  by (metis emeasure_mono emeasure_nonneg emeasure_notin_sets sets.sets_into_space sets.top)
    1.34  
    1.35  lemma emeasure_compl:
    1.36    assumes s: "s \<in> sets M" and fin: "emeasure M s \<noteq> \<infinity>"
    1.37 @@ -479,7 +479,7 @@
    1.38  proof -
    1.39    from s have "0 \<le> emeasure M s" by auto
    1.40    have "emeasure M (space M) = emeasure M (s \<union> (space M - s))" using s
    1.41 -    by (metis Un_Diff_cancel Un_absorb1 s sets_into_space)
    1.42 +    by (metis Un_Diff_cancel Un_absorb1 s sets.sets_into_space)
    1.43    also have "... = emeasure M s + emeasure M (space M - s)"
    1.44      by (rule plus_emeasure[symmetric]) (auto simp add: s)
    1.45    finally have "emeasure M (space M) = emeasure M s + emeasure M (space M - s)" .
    1.46 @@ -506,7 +506,8 @@
    1.47  lemma Lim_emeasure_incseq:
    1.48    "range A \<subseteq> sets M \<Longrightarrow> incseq A \<Longrightarrow> (\<lambda>i. (emeasure M (A i))) ----> emeasure M (\<Union>i. A i)"
    1.49    using emeasure_countably_additive
    1.50 -  by (auto simp add: countably_additive_iff_continuous_from_below emeasure_positive emeasure_additive)
    1.51 +  by (auto simp add: sets.countably_additive_iff_continuous_from_below emeasure_positive
    1.52 +    emeasure_additive)
    1.53  
    1.54  lemma incseq_emeasure:
    1.55    assumes "range B \<subseteq> sets M" "incseq B"
    1.56 @@ -595,10 +596,10 @@
    1.57    have "emeasure M (\<Union>i. f i) = emeasure M (\<Union>i. disjointed f i)"
    1.58      unfolding UN_disjointed_eq ..
    1.59    also have "\<dots> = (\<Sum>i. emeasure M (disjointed f i))"
    1.60 -    using range_disjointed_sets[OF assms] suminf_emeasure[of "disjointed f"]
    1.61 +    using sets.range_disjointed_sets[OF assms] suminf_emeasure[of "disjointed f"]
    1.62      by (simp add:  disjoint_family_disjointed comp_def)
    1.63    also have "\<dots> \<le> (\<Sum>i. emeasure M (f i))"
    1.64 -    using range_disjointed_sets[OF assms] assms
    1.65 +    using sets.range_disjointed_sets[OF assms] assms
    1.66      by (auto intro!: suminf_le_pos emeasure_mono disjointed_subset)
    1.67    finally show ?thesis .
    1.68  qed
    1.69 @@ -676,7 +677,8 @@
    1.70    let ?\<mu>  = "emeasure M" and ?\<nu> = "emeasure N"
    1.71    interpret S: sigma_algebra \<Omega> "sigma_sets \<Omega> E" by (rule sigma_algebra_sigma_sets) fact
    1.72    have "space M = \<Omega>"
    1.73 -    using top[of M] space_closed[of M] S.top S.space_closed `sets M = sigma_sets \<Omega> E` by blast
    1.74 +    using sets.top[of M] sets.space_closed[of M] S.top S.space_closed `sets M = sigma_sets \<Omega> E`
    1.75 +    by blast
    1.76  
    1.77    { fix F D assume "F \<in> E" and "?\<mu> F \<noteq> \<infinity>"
    1.78      then have [intro]: "F \<in> sigma_sets \<Omega> E" by auto
    1.79 @@ -724,9 +726,9 @@
    1.80      fix F assume "F \<in> sets M"
    1.81      let ?D = "disjointed (\<lambda>i. F \<inter> A i)"
    1.82      from `space M = \<Omega>` have F_eq: "F = (\<Union>i. ?D i)"
    1.83 -      using `F \<in> sets M`[THEN sets_into_space] A(2)[symmetric] by (auto simp: UN_disjointed_eq)
    1.84 +      using `F \<in> sets M`[THEN sets.sets_into_space] A(2)[symmetric] by (auto simp: UN_disjointed_eq)
    1.85      have [simp, intro]: "\<And>i. ?D i \<in> sets M"
    1.86 -      using range_disjointed_sets[of "\<lambda>i. F \<inter> A i" M] `F \<in> sets M`
    1.87 +      using sets.range_disjointed_sets[of "\<lambda>i. F \<inter> A i" M] `F \<in> sets M`
    1.88        by (auto simp: subset_eq)
    1.89      have "disjoint_family ?D"
    1.90        by (auto simp: disjoint_family_disjointed)
    1.91 @@ -770,7 +772,7 @@
    1.92  interpretation null_sets: ring_of_sets "space M" "null_sets M" for M
    1.93  proof (rule ring_of_setsI)
    1.94    show "null_sets M \<subseteq> Pow (space M)"
    1.95 -    using sets_into_space by auto
    1.96 +    using sets.sets_into_space by auto
    1.97    show "{} \<in> null_sets M"
    1.98      by auto
    1.99    fix A B assume sets: "A \<in> null_sets M" "B \<in> null_sets M"
   1.100 @@ -904,7 +906,7 @@
   1.101  
   1.102  lemma AE_iff_null_sets:
   1.103    "N \<in> sets M \<Longrightarrow> N \<in> null_sets M \<longleftrightarrow> (AE x in M. x \<notin> N)"
   1.104 -  using Int_absorb1[OF sets_into_space, of N M]
   1.105 +  using Int_absorb1[OF sets.sets_into_space, of N M]
   1.106    by (subst AE_iff_null) (auto simp: Int_def[symmetric])
   1.107  
   1.108  lemma AE_not_in:
   1.109 @@ -1033,7 +1035,7 @@
   1.110    have "emeasure M A = emeasure M (A - N)"
   1.111      using N A by (subst emeasure_Diff_null_set) auto
   1.112    also have "emeasure M (A - N) \<le> emeasure M (B - N)"
   1.113 -    using N A B sets_into_space by (auto intro!: emeasure_mono)
   1.114 +    using N A B sets.sets_into_space by (auto intro!: emeasure_mono)
   1.115    also have "emeasure M (B - N) = emeasure M B"
   1.116      using N B by (subst emeasure_Diff_null_set) auto
   1.117    finally show ?thesis .
   1.118 @@ -1062,7 +1064,7 @@
   1.119      space: "(\<Union>i. A i) = space M" and
   1.120      measure: "\<And>i. emeasure M (A i) \<noteq> \<infinity>"
   1.121      using sigma_finite by auto
   1.122 -  note range' = range_disjointed_sets[OF range] range
   1.123 +  note range' = sets.range_disjointed_sets[OF range] range
   1.124    { fix i
   1.125      have "emeasure M (disjointed A i) \<le> emeasure M (A i)"
   1.126        using range' disjointed_subset[of A i] by (auto intro!: emeasure_mono)
   1.127 @@ -1400,7 +1402,7 @@
   1.128  lemma (in finite_measure) finite_measure_compl:
   1.129    assumes S: "S \<in> sets M"
   1.130    shows "measure M (space M - S) = measure M (space M) - measure M S"
   1.131 -  using measure_Diff[OF _ top S sets_into_space] S by simp
   1.132 +  using measure_Diff[OF _ sets.top S sets.sets_into_space] S by simp
   1.133  
   1.134  lemma (in finite_measure) finite_measure_mono_AE:
   1.135    assumes imp: "AE x in M. x \<in> A \<longrightarrow> x \<in> B" and B: "B \<in> sets M"
   1.136 @@ -1497,7 +1499,7 @@
   1.137    shows "measure M e = (\<Sum> x \<in> s. measure M (e \<inter> f x))"
   1.138  proof -
   1.139    have e: "e = (\<Union> i \<in> s. e \<inter> f i)"
   1.140 -    using `e \<in> sets M` sets_into_space upper by blast
   1.141 +    using `e \<in> sets M` sets.sets_into_space upper by blast
   1.142    hence "measure M e = measure M (\<Union> i \<in> s. e \<inter> f i)" by simp
   1.143    also have "\<dots> = (\<Sum> x \<in> s. measure M (e \<inter> f x))"
   1.144    proof (rule finite_measure_finite_Union)