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.10
1.11  lemma emeasure_additive: "additive (sets M) (emeasure M)"
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.51 +  by (auto simp add: sets.countably_additive_iff_continuous_from_below emeasure_positive
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)
```