Caratheodory: cleanup and modernisation
authorhoelzl
Mon Sep 28 17:29:01 2015 +0200 (2015-09-28)
changeset 61273542a4d9bac96
parent 61272 f49644098959
child 61274 0261eec37233
Caratheodory: cleanup and modernisation
src/HOL/Probability/Caratheodory.thy
     1.1 --- a/src/HOL/Probability/Caratheodory.thy	Fri Sep 25 23:01:34 2015 +0200
     1.2 +++ b/src/HOL/Probability/Caratheodory.thy	Mon Sep 28 17:29:01 2015 +0200
     1.3 @@ -41,49 +41,43 @@
     1.4    ultimately
     1.5    show ?thesis unfolding g_def using pos
     1.6      by (auto intro!: SUP_eq  simp: setsum.cartesian_product reindex SUP_upper2
     1.7 -                     setsum_nonneg suminf_ereal_eq_SUP SUP_pair
     1.8 +                     suminf_ereal_eq_SUP SUP_pair
     1.9                       SUP_ereal_setsum[symmetric] incseq_setsumI setsum_nonneg)
    1.10  qed
    1.11  
    1.12  subsection {* Characterizations of Measures *}
    1.13  
    1.14 -definition subadditive where "subadditive M f \<longleftrightarrow>
    1.15 -  (\<forall>x\<in>M. \<forall>y\<in>M. x \<inter> y = {} \<longrightarrow> f (x \<union> y) \<le> f x + f y)"
    1.16 -
    1.17 -definition countably_subadditive where "countably_subadditive M f \<longleftrightarrow>
    1.18 -  (\<forall>A. range A \<subseteq> M \<longrightarrow> disjoint_family A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow>
    1.19 -    (f (\<Union>i. A i) \<le> (\<Sum>i. f (A i))))"
    1.20 +definition subadditive where
    1.21 +  "subadditive M f \<longleftrightarrow> (\<forall>x\<in>M. \<forall>y\<in>M. x \<inter> y = {} \<longrightarrow> f (x \<union> y) \<le> f x + f y)"
    1.22  
    1.23 -definition outer_measure_space where "outer_measure_space M f \<longleftrightarrow>
    1.24 -  positive M f \<and> increasing M f \<and> countably_subadditive M f"
    1.25 +definition countably_subadditive where
    1.26 +  "countably_subadditive M f \<longleftrightarrow>
    1.27 +    (\<forall>A. range A \<subseteq> M \<longrightarrow> disjoint_family A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow> (f (\<Union>i. A i) \<le> (\<Sum>i. f (A i))))"
    1.28  
    1.29 -definition measure_set where "measure_set M f X = {r.
    1.30 -  \<exists>A. range A \<subseteq> M \<and> disjoint_family A \<and> X \<subseteq> (\<Union>i. A i) \<and> (\<Sum>i. f (A i)) = r}"
    1.31 +definition outer_measure_space where
    1.32 +  "outer_measure_space M f \<longleftrightarrow> positive M f \<and> increasing M f \<and> countably_subadditive M f"
    1.33  
    1.34 -lemma subadditiveD:
    1.35 -  "subadditive M f \<Longrightarrow> x \<inter> y = {} \<Longrightarrow> x \<in> M \<Longrightarrow> y \<in> M \<Longrightarrow> f (x \<union> y) \<le> f x + f y"
    1.36 +lemma subadditiveD: "subadditive M f \<Longrightarrow> x \<inter> y = {} \<Longrightarrow> x \<in> M \<Longrightarrow> y \<in> M \<Longrightarrow> f (x \<union> y) \<le> f x + f y"
    1.37    by (auto simp add: subadditive_def)
    1.38  
    1.39  subsubsection {* Lambda Systems *}
    1.40  
    1.41 -definition lambda_system where "lambda_system \<Omega> M f = {l \<in> M.
    1.42 -  \<forall>x \<in> M. f (l \<inter> x) + f ((\<Omega> - l) \<inter> x) = f x}"
    1.43 +definition lambda_system where
    1.44 +  "lambda_system \<Omega> M f = {l \<in> M. \<forall>x \<in> M. f (l \<inter> x) + f ((\<Omega> - l) \<inter> x) = f x}"
    1.45  
    1.46  lemma (in algebra) lambda_system_eq:
    1.47 -  shows "lambda_system \<Omega> M f = {l \<in> M. \<forall>x \<in> M. f (x \<inter> l) + f (x - l) = f x}"
    1.48 +  "lambda_system \<Omega> M f = {l \<in> M. \<forall>x \<in> M. f (x \<inter> l) + f (x - l) = f x}"
    1.49  proof -
    1.50 -  have [simp]: "!!l x. l \<in> M \<Longrightarrow> x \<in> M \<Longrightarrow> (\<Omega> - l) \<inter> x = x - l"
    1.51 +  have [simp]: "\<And>l x. l \<in> M \<Longrightarrow> x \<in> M \<Longrightarrow> (\<Omega> - l) \<inter> x = x - l"
    1.52      by (metis Int_Diff Int_absorb1 Int_commute sets_into_space)
    1.53    show ?thesis
    1.54      by (auto simp add: lambda_system_def) (metis Int_commute)+
    1.55  qed
    1.56  
    1.57 -lemma (in algebra) lambda_system_empty:
    1.58 -  "positive M f \<Longrightarrow> {} \<in> lambda_system \<Omega> M f"
    1.59 +lemma (in algebra) lambda_system_empty: "positive M f \<Longrightarrow> {} \<in> lambda_system \<Omega> M f"
    1.60    by (auto simp add: positive_def lambda_system_eq)
    1.61  
    1.62 -lemma lambda_system_sets:
    1.63 -  "x \<in> lambda_system \<Omega> M f \<Longrightarrow> x \<in> M"
    1.64 +lemma lambda_system_sets: "x \<in> lambda_system \<Omega> M f \<Longrightarrow> x \<in> M"
    1.65    by (simp add: lambda_system_def)
    1.66  
    1.67  lemma (in algebra) lambda_system_Compl:
    1.68 @@ -201,12 +195,10 @@
    1.69      by (auto simp add: Un o_def suminf_binaryset_eq positive_def)
    1.70  qed
    1.71  
    1.72 -lemma lambda_system_increasing:
    1.73 - "increasing M f \<Longrightarrow> increasing (lambda_system \<Omega> M f) f"
    1.74 +lemma lambda_system_increasing: "increasing M f \<Longrightarrow> increasing (lambda_system \<Omega> M f) f"
    1.75    by (simp add: increasing_def lambda_system_def)
    1.76  
    1.77 -lemma lambda_system_positive:
    1.78 -  "positive M f \<Longrightarrow> positive (lambda_system \<Omega> M f) f"
    1.79 +lemma lambda_system_positive: "positive M f \<Longrightarrow> positive (lambda_system \<Omega> M f) f"
    1.80    by (simp add: positive_def lambda_system_def)
    1.81  
    1.82  lemma (in algebra) lambda_system_strong_sum:
    1.83 @@ -258,66 +250,56 @@
    1.84      have *: "\<And>i. 0 \<le> f (A i)" using pos A'' unfolding positive_def by auto
    1.85      have dis: "\<And>N. disjoint_family_on A {..<N}" by (intro disjoint_family_on_mono[OF _ disj]) auto
    1.86      show "(\<Sum>i. f (A i)) \<le> f (\<Union>i. A i)"
    1.87 -      using ls.additive_sum [OF lambda_system_positive[OF pos] lambda_system_additive _ A' dis]
    1.88 -      using A''
    1.89 +      using ls.additive_sum [OF lambda_system_positive[OF pos] lambda_system_additive _ A' dis] A''
    1.90        by (intro suminf_bound[OF _ *]) (auto intro!: increasingD[OF inc] countable_UN)
    1.91    qed
    1.92 -  {
    1.93 -    fix a
    1.94 -    assume a [iff]: "a \<in> M"
    1.95 -    have "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) = f a"
    1.96 -    proof -
    1.97 -      show ?thesis
    1.98 -      proof (rule antisym)
    1.99 -        have "range (\<lambda>i. a \<inter> A i) \<subseteq> M" using A''
   1.100 -          by blast
   1.101 -        moreover
   1.102 -        have "disjoint_family (\<lambda>i. a \<inter> A i)" using disj
   1.103 -          by (auto simp add: disjoint_family_on_def)
   1.104 -        moreover
   1.105 -        have "a \<inter> (\<Union>i. A i) \<in> M"
   1.106 -          by (metis Int U_in a)
   1.107 -        ultimately
   1.108 -        have "f (a \<inter> (\<Union>i. A i)) \<le> (\<Sum>i. f (a \<inter> A i))"
   1.109 -          using csa[unfolded countably_subadditive_def, rule_format, of "(\<lambda>i. a \<inter> A i)"]
   1.110 -          by (simp add: o_def)
   1.111 -        hence "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le>
   1.112 -            (\<Sum>i. f (a \<inter> A i)) + f (a - (\<Union>i. A i))"
   1.113 -          by (rule add_right_mono)
   1.114 -        moreover
   1.115 -        have "(\<Sum>i. f (a \<inter> A i)) + f (a - (\<Union>i. A i)) \<le> f a"
   1.116 -          proof (intro suminf_bound_add allI)
   1.117 -            fix n
   1.118 -            have UNION_in: "(\<Union>i\<in>{0..<n}. A i) \<in> M"
   1.119 -              by (metis A'' UNION_in_sets)
   1.120 -            have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A''
   1.121 -              by (blast intro: increasingD [OF inc] A'' UNION_in_sets)
   1.122 -            have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system \<Omega> M f"
   1.123 -              using ls.UNION_in_sets by (simp add: A)
   1.124 -            hence eq_fa: "f a = f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i))"
   1.125 -              by (simp add: lambda_system_eq UNION_in)
   1.126 -            have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))"
   1.127 -              by (blast intro: increasingD [OF inc] UNION_in U_in)
   1.128 -            thus "(\<Sum>i<n. f (a \<inter> A i)) + f (a - (\<Union>i. A i)) \<le> f a"
   1.129 -              by (simp add: lambda_system_strong_sum pos A disj eq_fa add_left_mono atLeast0LessThan[symmetric])
   1.130 -          next
   1.131 -            have "\<And>i. a \<inter> A i \<in> M" using A'' by auto
   1.132 -            then show "\<And>i. 0 \<le> f (a \<inter> A i)" using pos[unfolded positive_def] by auto
   1.133 -            have "\<And>i. a - (\<Union>i. A i) \<in> M" using A'' by auto
   1.134 -            then have "\<And>i. 0 \<le> f (a - (\<Union>i. A i))" using pos[unfolded positive_def] by auto
   1.135 -            then show "f (a - (\<Union>i. A i)) \<noteq> -\<infinity>" by auto
   1.136 -          qed
   1.137 -        ultimately show "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le> f a"
   1.138 -          by (rule order_trans)
   1.139 -      next
   1.140 -        have "f a \<le> f (a \<inter> (\<Union>i. A i) \<union> (a - (\<Union>i. A i)))"
   1.141 -          by (blast intro:  increasingD [OF inc] U_in)
   1.142 -        also have "... \<le>  f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))"
   1.143 -          by (blast intro: subadditiveD [OF sa] U_in)
   1.144 -        finally show "f a \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))" .
   1.145 -        qed
   1.146 -     qed
   1.147 -  }
   1.148 +  have "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) = f a"
   1.149 +    if a [iff]: "a \<in> M" for a
   1.150 +  proof (rule antisym)
   1.151 +    have "range (\<lambda>i. a \<inter> A i) \<subseteq> M" using A''
   1.152 +      by blast
   1.153 +    moreover
   1.154 +    have "disjoint_family (\<lambda>i. a \<inter> A i)" using disj
   1.155 +      by (auto simp add: disjoint_family_on_def)
   1.156 +    moreover
   1.157 +    have "a \<inter> (\<Union>i. A i) \<in> M"
   1.158 +      by (metis Int U_in a)
   1.159 +    ultimately
   1.160 +    have "f (a \<inter> (\<Union>i. A i)) \<le> (\<Sum>i. f (a \<inter> A i))"
   1.161 +      using csa[unfolded countably_subadditive_def, rule_format, of "(\<lambda>i. a \<inter> A i)"]
   1.162 +      by (simp add: o_def)
   1.163 +    hence "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le> (\<Sum>i. f (a \<inter> A i)) + f (a - (\<Union>i. A i))"
   1.164 +      by (rule add_right_mono)
   1.165 +    also have "\<dots> \<le> f a"
   1.166 +    proof (intro suminf_bound_add allI)
   1.167 +      fix n
   1.168 +      have UNION_in: "(\<Union>i\<in>{0..<n}. A i) \<in> M"
   1.169 +        by (metis A'' UNION_in_sets)
   1.170 +      have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A''
   1.171 +        by (blast intro: increasingD [OF inc] A'' UNION_in_sets)
   1.172 +      have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system \<Omega> M f"
   1.173 +        using ls.UNION_in_sets by (simp add: A)
   1.174 +      hence eq_fa: "f a = f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i))"
   1.175 +        by (simp add: lambda_system_eq UNION_in)
   1.176 +      have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))"
   1.177 +        by (blast intro: increasingD [OF inc] UNION_in U_in)
   1.178 +      thus "(\<Sum>i<n. f (a \<inter> A i)) + f (a - (\<Union>i. A i)) \<le> f a"
   1.179 +        by (simp add: lambda_system_strong_sum pos A disj eq_fa add_left_mono atLeast0LessThan[symmetric])
   1.180 +    next
   1.181 +      have "\<And>i. a \<inter> A i \<in> M" using A'' by auto
   1.182 +      then show "\<And>i. 0 \<le> f (a \<inter> A i)" using pos[unfolded positive_def] by auto
   1.183 +      have "\<And>i. a - (\<Union>i. A i) \<in> M" using A'' by auto
   1.184 +      then have "\<And>i. 0 \<le> f (a - (\<Union>i. A i))" using pos[unfolded positive_def] by auto
   1.185 +      then show "f (a - (\<Union>i. A i)) \<noteq> -\<infinity>" by auto
   1.186 +    qed
   1.187 +    finally show "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le> f a" .
   1.188 +  next
   1.189 +    have "f a \<le> f (a \<inter> (\<Union>i. A i) \<union> (a - (\<Union>i. A i)))"
   1.190 +      by (blast intro:  increasingD [OF inc] U_in)
   1.191 +    also have "... \<le>  f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))"
   1.192 +      by (blast intro: subadditiveD [OF sa] U_in)
   1.193 +    finally show "f a \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))" .
   1.194 +  qed
   1.195    thus  ?thesis
   1.196      by (simp add: lambda_system_eq sums_iff U_eq U_in)
   1.197  qed
   1.198 @@ -345,300 +327,186 @@
   1.199      using pos by (simp add: measure_space_def)
   1.200  qed
   1.201  
   1.202 -lemma inf_measure_nonempty:
   1.203 -  assumes f: "positive M f" and b: "b \<in> M" and a: "a \<subseteq> b" "{} \<in> M"
   1.204 -  shows "f b \<in> measure_set M f a"
   1.205 -proof -
   1.206 -  let ?A = "\<lambda>i::nat. (if i = 0 then b else {})"
   1.207 -  have "(\<Sum>i. f (?A i)) = (\<Sum>i<1::nat. f (?A i))"
   1.208 -    by (rule suminf_finite) (simp_all add: f[unfolded positive_def])
   1.209 -  also have "... = f b"
   1.210 -    by simp
   1.211 -  finally show ?thesis using assms
   1.212 -    by (auto intro!: exI [of _ ?A]
   1.213 -             simp: measure_set_def disjoint_family_on_def split_if_mem2 comp_def)
   1.214 -qed
   1.215 +definition outer_measure :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> 'a set \<Rightarrow> ereal" where
   1.216 +   "outer_measure M f X =
   1.217 +     (INF A:{A. range A \<subseteq> M \<and> disjoint_family A \<and> X \<subseteq> (\<Union>i. A i)}. \<Sum>i. f (A i))"
   1.218  
   1.219 -lemma (in ring_of_sets) inf_measure_agrees:
   1.220 -  assumes posf: "positive M f" and ca: "countably_additive M f"
   1.221 -      and s: "s \<in> M"
   1.222 -  shows "Inf (measure_set M f s) = f s"
   1.223 -proof (intro Inf_eqI)
   1.224 -  fix z
   1.225 -  assume z: "z \<in> measure_set M f s"
   1.226 -  from this obtain A where
   1.227 -    A: "range A \<subseteq> M" and disj: "disjoint_family A"
   1.228 -    and "s \<subseteq> (\<Union>x. A x)" and si: "(\<Sum>i. f (A i)) = z"
   1.229 -    by (auto simp add: measure_set_def comp_def)
   1.230 -  hence seq: "s = (\<Union>i. A i \<inter> s)" by blast
   1.231 +lemma (in ring_of_sets) outer_measure_agrees:
   1.232 +  assumes posf: "positive M f" and ca: "countably_additive M f" and s: "s \<in> M"
   1.233 +  shows "outer_measure M f s = f s"
   1.234 +  unfolding outer_measure_def
   1.235 +proof (safe intro!: antisym INF_greatest)
   1.236 +  fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> M" and dA: "disjoint_family A" and sA: "s \<subseteq> (\<Union>x. A x)"
   1.237    have inc: "increasing M f"
   1.238      by (metis additive_increasing ca countably_additive_additive posf)
   1.239 -  have sums: "(\<Sum>i. f (A i \<inter> s)) = f (\<Union>i. A i \<inter> s)"
   1.240 -    proof (rule ca[unfolded countably_additive_def, rule_format])
   1.241 -      show "range (\<lambda>n. A n \<inter> s) \<subseteq> M" using A s
   1.242 -        by blast
   1.243 -      show "disjoint_family (\<lambda>n. A n \<inter> s)" using disj
   1.244 -        by (auto simp add: disjoint_family_on_def)
   1.245 -      show "(\<Union>i. A i \<inter> s) \<in> M" using A s
   1.246 -        by (metis UN_extend_simps(4) s seq)
   1.247 -    qed
   1.248 -  hence "f s = (\<Sum>i. f (A i \<inter> s))"
   1.249 -    using seq [symmetric] by (simp add: sums_iff)
   1.250 +  have "f s = f (\<Union>i. A i \<inter> s)"
   1.251 +    using sA by (auto simp: Int_absorb1)
   1.252 +  also have "\<dots> = (\<Sum>i. f (A i \<inter> s))"
   1.253 +    using sA dA A s
   1.254 +    by (intro ca[unfolded countably_additive_def, rule_format, symmetric])
   1.255 +       (auto simp: Int_absorb1 disjoint_family_on_def)
   1.256    also have "... \<le> (\<Sum>i. f (A i))"
   1.257 -    proof (rule suminf_le_pos)
   1.258 -      fix n show "f (A n \<inter> s) \<le> f (A n)" using A s
   1.259 -        by (force intro: increasingD [OF inc])
   1.260 -      fix N have "A N \<inter> s \<in> M"  using A s by auto
   1.261 -      then show "0 \<le> f (A N \<inter> s)" using posf unfolding positive_def by auto
   1.262 -    qed
   1.263 -  also have "... = z" by (rule si)
   1.264 -  finally show "f s \<le> z" .
   1.265 -qed (blast intro: inf_measure_nonempty [of _ f, OF posf s subset_refl])
   1.266 -
   1.267 -lemma measure_set_pos:
   1.268 -  assumes posf: "positive M f" "r \<in> measure_set M f X"
   1.269 -  shows "0 \<le> r"
   1.270 -proof -
   1.271 -  obtain A where "range A \<subseteq> M" and r: "r = (\<Sum>i. f (A i))"
   1.272 -    using `r \<in> measure_set M f X` unfolding measure_set_def by auto
   1.273 -  then show "0 \<le> r" using posf unfolding r positive_def
   1.274 -    by (intro suminf_0_le) auto
   1.275 -qed
   1.276 -
   1.277 -lemma inf_measure_pos:
   1.278 -  assumes posf: "positive M f"
   1.279 -  shows "0 \<le> Inf (measure_set M f X)"
   1.280 -proof (rule complete_lattice_class.Inf_greatest)
   1.281 -  fix r assume "r \<in> measure_set M f X" with posf show "0 \<le> r"
   1.282 -    by (rule measure_set_pos)
   1.283 +    using A s by (intro suminf_le_pos increasingD[OF inc] positiveD2[OF posf]) auto
   1.284 +  finally show "f s \<le> (\<Sum>i. f (A i))" .
   1.285 +next
   1.286 +  have "(\<Sum>i. f (if i = 0 then s else {})) \<le> f s"
   1.287 +    using positiveD1[OF posf] by (subst suminf_finite[of "{0}"]) auto
   1.288 +  with s show "(INF A:{A. range A \<subseteq> M \<and> disjoint_family A \<and> s \<subseteq> UNION UNIV A}. \<Sum>i. f (A i)) \<le> f s"
   1.289 +    by (intro INF_lower2[of "\<lambda>i. if i = 0 then s else {}"])
   1.290 +       (auto simp: disjoint_family_on_def)
   1.291  qed
   1.292  
   1.293 -lemma inf_measure_empty:
   1.294 +lemma outer_measure_nonneg: "positive M f \<Longrightarrow> 0 \<le> outer_measure M f X"
   1.295 +  by (auto intro!: INF_greatest suminf_0_le intro: positiveD2 simp: outer_measure_def)
   1.296 +
   1.297 +lemma outer_measure_empty:
   1.298    assumes posf: "positive M f" and "{} \<in> M"
   1.299 -  shows "Inf (measure_set M f {}) = 0"
   1.300 +  shows "outer_measure M f {} = 0"
   1.301  proof (rule antisym)
   1.302 -  show "Inf (measure_set M f {}) \<le> 0"
   1.303 -    by (metis complete_lattice_class.Inf_lower `{} \<in> M`
   1.304 -              inf_measure_nonempty[OF posf] subset_refl posf[unfolded positive_def])
   1.305 -qed (rule inf_measure_pos[OF posf])
   1.306 +  show "outer_measure M f {} \<le> 0"
   1.307 +    using assms by (auto intro!: INF_lower2[of "\<lambda>_. {}"] simp: outer_measure_def disjoint_family_on_def positive_def)
   1.308 +qed (intro outer_measure_nonneg posf)
   1.309 +
   1.310 +lemma (in ring_of_sets) positive_outer_measure:
   1.311 +  assumes "positive M f" shows "positive (Pow \<Omega>) (outer_measure M f)"
   1.312 +  unfolding positive_def by (auto simp: assms outer_measure_empty outer_measure_nonneg)
   1.313 +
   1.314 +lemma (in ring_of_sets) increasing_outer_measure: "increasing (Pow \<Omega>) (outer_measure M f)"
   1.315 +  by (force simp: increasing_def outer_measure_def intro!: INF_greatest intro: INF_lower)
   1.316  
   1.317 -lemma (in ring_of_sets) inf_measure_positive:
   1.318 -  assumes p: "positive M f" and "{} \<in> M"
   1.319 -  shows "positive M (\<lambda>x. Inf (measure_set M f x))"
   1.320 -proof (unfold positive_def, intro conjI ballI)
   1.321 -  show "Inf (measure_set M f {}) = 0" using inf_measure_empty[OF assms] by auto
   1.322 -  fix A assume "A \<in> M"
   1.323 -qed (rule inf_measure_pos[OF p])
   1.324 +lemma (in ring_of_sets) outer_measure_le:
   1.325 +  assumes pos: "positive M f" and inc: "increasing M f" and A: "range A \<subseteq> M" and X: "X \<subseteq> (\<Union>i. A i)"
   1.326 +  shows "outer_measure M f X \<le> (\<Sum>i. f (A i))"
   1.327 +  unfolding outer_measure_def
   1.328 +proof (safe intro!: INF_lower2[of "disjointed A"] del: subsetI)
   1.329 +  show dA: "range (disjointed A) \<subseteq> M"
   1.330 +    by (auto intro!: A range_disjointed_sets)
   1.331 +  have "\<forall>n. f (disjointed A n) \<le> f (A n)"
   1.332 +    by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A)
   1.333 +  moreover have "\<forall>i. 0 \<le> f (disjointed A i)"
   1.334 +    using pos dA unfolding positive_def by auto
   1.335 +  ultimately show "(\<Sum>i. f (disjointed A i)) \<le> (\<Sum>i. f (A i))"
   1.336 +    by (blast intro!: suminf_le_pos)
   1.337 +qed (auto simp: X UN_disjointed_eq disjoint_family_disjointed)
   1.338  
   1.339 -lemma (in ring_of_sets) inf_measure_increasing:
   1.340 -  assumes posf: "positive M f"
   1.341 -  shows "increasing (Pow \<Omega>) (\<lambda>x. Inf (measure_set M f x))"
   1.342 -apply (clarsimp simp add: increasing_def)
   1.343 -apply (rule complete_lattice_class.Inf_greatest)
   1.344 -apply (rule complete_lattice_class.Inf_lower)
   1.345 -apply (clarsimp simp add: measure_set_def, rule_tac x=A in exI, blast)
   1.346 -done
   1.347 -
   1.348 -lemma (in ring_of_sets) inf_measure_le:
   1.349 -  assumes posf: "positive M f" and inc: "increasing M f"
   1.350 -      and x: "x \<in> {r . \<exists>A. range A \<subseteq> M \<and> s \<subseteq> (\<Union>i. A i) \<and> (\<Sum>i. f (A i)) = r}"
   1.351 -  shows "Inf (measure_set M f s) \<le> x"
   1.352 +lemma (in ring_of_sets) outer_measure_close:
   1.353 +  assumes posf: "positive M f" and "0 < e" and "outer_measure M f X \<noteq> \<infinity>"
   1.354 +  shows "\<exists>A. range A \<subseteq> M \<and> disjoint_family A \<and> X \<subseteq> (\<Union>i. A i) \<and> (\<Sum>i. f (A i)) \<le> outer_measure M f X + e"
   1.355  proof -
   1.356 -  obtain A where A: "range A \<subseteq> M" and ss: "s \<subseteq> (\<Union>i. A i)"
   1.357 -             and xeq: "(\<Sum>i. f (A i)) = x"
   1.358 -    using x by auto
   1.359 -  have dA: "range (disjointed A) \<subseteq> M"
   1.360 -    by (metis A range_disjointed_sets)
   1.361 -  have "\<forall>n. f (disjointed A n) \<le> f (A n)"
   1.362 -    by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A comp_def)
   1.363 -  moreover have "\<forall>i. 0 \<le> f (disjointed A i)"
   1.364 -    using posf dA unfolding positive_def by auto
   1.365 -  ultimately have sda: "(\<Sum>i. f (disjointed A i)) \<le> (\<Sum>i. f (A i))"
   1.366 -    by (blast intro!: suminf_le_pos)
   1.367 -  hence ley: "(\<Sum>i. f (disjointed A i)) \<le> x"
   1.368 -    by (metis xeq)
   1.369 -  hence y: "(\<Sum>i. f (disjointed A i)) \<in> measure_set M f s"
   1.370 -    apply (auto simp add: measure_set_def)
   1.371 -    apply (rule_tac x="disjointed A" in exI)
   1.372 -    apply (simp add: disjoint_family_disjointed UN_disjointed_eq ss dA comp_def)
   1.373 -    done
   1.374 +  from `outer_measure M f X \<noteq> \<infinity>` have fin: "\<bar>outer_measure M f X\<bar> \<noteq> \<infinity>"
   1.375 +    using outer_measure_nonneg[OF posf, of X] by auto
   1.376    show ?thesis
   1.377 -    by (blast intro: y order_trans [OF _ ley] posf complete_lattice_class.Inf_lower)
   1.378 -qed
   1.379 -
   1.380 -lemma (in ring_of_sets) inf_measure_close:
   1.381 -  fixes e :: ereal
   1.382 -  assumes posf: "positive M f" and e: "0 < e" and ss: "s \<subseteq> (\<Omega>)" and "Inf (measure_set M f s) \<noteq> \<infinity>"
   1.383 -  shows "\<exists>A. range A \<subseteq> M \<and> disjoint_family A \<and> s \<subseteq> (\<Union>i. A i) \<and>
   1.384 -               (\<Sum>i. f (A i)) \<le> Inf (measure_set M f s) + e"
   1.385 -proof -
   1.386 -  from `Inf (measure_set M f s) \<noteq> \<infinity>` have fin: "\<bar>Inf (measure_set M f s)\<bar> \<noteq> \<infinity>"
   1.387 -    using inf_measure_pos[OF posf, of s] by auto
   1.388 -  obtain l where "l \<in> measure_set M f s" "l \<le> Inf (measure_set M f s) + e"
   1.389 -    using Inf_ereal_close[OF fin e] by auto
   1.390 -  thus ?thesis
   1.391 -    by (auto intro!: exI[of _ l] simp: measure_set_def comp_def)
   1.392 +    using Inf_ereal_close[OF fin[unfolded outer_measure_def INF_def], OF \<open>0 < e\<close>]
   1.393 +    unfolding INF_def[symmetric] outer_measure_def[symmetric] by (auto intro: less_imp_le)
   1.394  qed
   1.395  
   1.396 -lemma (in ring_of_sets) inf_measure_countably_subadditive:
   1.397 +lemma (in ring_of_sets) countably_subadditive_outer_measure:
   1.398    assumes posf: "positive M f" and inc: "increasing M f"
   1.399 -  shows "countably_subadditive (Pow \<Omega>) (\<lambda>x. Inf (measure_set M f x))"
   1.400 +  shows "countably_subadditive (Pow \<Omega>) (outer_measure M f)"
   1.401  proof (simp add: countably_subadditive_def, safe)
   1.402 -  fix A :: "nat \<Rightarrow> 'a set"
   1.403 -  let ?outer = "\<lambda>B. Inf (measure_set M f B)"
   1.404 -  assume A: "range A \<subseteq> Pow (\<Omega>)"
   1.405 -     and disj: "disjoint_family A"
   1.406 -     and sb: "(\<Union>i. A i) \<subseteq> \<Omega>"
   1.407 +  fix A :: "nat \<Rightarrow> _" assume A: "range A \<subseteq> Pow (\<Omega>)" and sb: "(\<Union>i. A i) \<subseteq> \<Omega>"
   1.408 +  let ?O = "outer_measure M f"
   1.409  
   1.410 -  { fix e :: ereal assume e: "0 < e" and "\<forall>i. ?outer (A i) \<noteq> \<infinity>"
   1.411 -    hence "\<exists>BB. \<forall>n. range (BB n) \<subseteq> M \<and> disjoint_family (BB n) \<and>
   1.412 -        A n \<subseteq> (\<Union>i. BB n i) \<and> (\<Sum>i. f (BB n i)) \<le> ?outer (A n) + e * (1/2)^(Suc n)"
   1.413 -      apply (safe intro!: choice inf_measure_close [of f, OF posf])
   1.414 -      using e sb by (auto simp: ereal_zero_less_0_iff one_ereal_def)
   1.415 -    then obtain BB
   1.416 -      where BB: "\<And>n. (range (BB n) \<subseteq> M)"
   1.417 -      and disjBB: "\<And>n. disjoint_family (BB n)"
   1.418 -      and sbBB: "\<And>n. A n \<subseteq> (\<Union>i. BB n i)"
   1.419 -      and BBle: "\<And>n. (\<Sum>i. f (BB n i)) \<le> ?outer (A n) + e * (1/2)^(Suc n)"
   1.420 +  { fix e :: ereal assume e: "0 < e" and "\<forall>i. ?O (A i) \<noteq> \<infinity>"
   1.421 +    hence "\<exists>B. \<forall>n. range (B n) \<subseteq> M \<and> disjoint_family (B n) \<and> A n \<subseteq> (\<Union>i. B n i) \<and>
   1.422 +        (\<Sum>i. f (B n i)) \<le> ?O (A n) + e * (1/2)^(Suc n)"
   1.423 +      using e sb by (auto intro!: choice outer_measure_close [of f, OF posf] simp: ereal_zero_less_0_iff one_ereal_def)
   1.424 +    then obtain B
   1.425 +      where B: "\<And>n. range (B n) \<subseteq> M"
   1.426 +      and sbB: "\<And>n. A n \<subseteq> (\<Union>i. B n i)"
   1.427 +      and Ble: "\<And>n. (\<Sum>i. f (B n i)) \<le> ?O (A n) + e * (1/2)^(Suc n)"
   1.428        by auto blast
   1.429 -    have sll: "(\<Sum>n. \<Sum>i. (f (BB n i))) \<le> (\<Sum>n. ?outer (A n)) + e"
   1.430 -    proof -
   1.431 -      have sum_eq_1: "(\<Sum>n. e*(1/2) ^ Suc n) = e"
   1.432 -        using suminf_half_series_ereal e
   1.433 -        by (simp add: ereal_zero_le_0_iff zero_le_divide_ereal suminf_cmult_ereal)
   1.434 -      have "\<And>n i. 0 \<le> f (BB n i)" using posf[unfolded positive_def] BB by auto
   1.435 -      then have "\<And>n. 0 \<le> (\<Sum>i. f (BB n i))" by (rule suminf_0_le)
   1.436 -      then have "(\<Sum>n. \<Sum>i. (f (BB n i))) \<le> (\<Sum>n. ?outer (A n) + e*(1/2) ^ Suc n)"
   1.437 -        by (rule suminf_le_pos[OF BBle])
   1.438 -      also have "... = (\<Sum>n. ?outer (A n)) + e"
   1.439 -        using sum_eq_1 inf_measure_pos[OF posf] e
   1.440 -        by (subst suminf_add_ereal) (auto simp add: ereal_zero_le_0_iff)
   1.441 -      finally show ?thesis .
   1.442 -    qed
   1.443 -    def C \<equiv> "(split BB) o prod_decode"
   1.444 -    from BB have "\<And>i j. BB i j \<in> M"
   1.445 +
   1.446 +    def C \<equiv> "split B o prod_decode"
   1.447 +    from B have B_in_M: "\<And>i j. B i j \<in> M"
   1.448        by (rule range_subsetD)
   1.449 -    then have C: "\<And>n. C n \<in> M"
   1.450 -      by (simp add: C_def split_def)
   1.451 -    have sbC: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)"
   1.452 -    proof (auto simp add: C_def)
   1.453 -      fix x i
   1.454 -      assume x: "x \<in> A i"
   1.455 -      with sbBB [of i] obtain j where "x \<in> BB i j"
   1.456 -        by blast
   1.457 -      thus "\<exists>i. x \<in> split BB (prod_decode i)"
   1.458 -        by (metis prod_encode_inverse prod.case)
   1.459 -    qed
   1.460 -    have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> prod_decode"
   1.461 -      by (rule ext)  (auto simp add: C_def)
   1.462 -    moreover have "suminf ... = (\<Sum>n. \<Sum>i. f (BB n i))" using BBle
   1.463 -      using BB posf[unfolded positive_def]
   1.464 -      by (force intro!: suminf_ereal_2dimen simp: o_def)
   1.465 -    ultimately have Csums: "(\<Sum>i. f (C i)) = (\<Sum>n. \<Sum>i. f (BB n i))" by (simp add: o_def)
   1.466 -    have "?outer (\<Union>i. A i) \<le> (\<Sum>n. \<Sum>i. f (BB n i))"
   1.467 -      apply (rule inf_measure_le [OF posf(1) inc], auto)
   1.468 -      apply (rule_tac x="C" in exI)
   1.469 -      apply (auto simp add: C sbC Csums)
   1.470 -      done
   1.471 -    also have "... \<le> (\<Sum>n. ?outer (A n)) + e" using sll
   1.472 -      by blast
   1.473 -    finally have "?outer (\<Union>i. A i) \<le> (\<Sum>n. ?outer (A n)) + e" . }
   1.474 -  note for_finite_Inf = this
   1.475 +    then have C: "range C \<subseteq> M"
   1.476 +      by (auto simp add: C_def split_def)
   1.477 +    have A_C: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)"
   1.478 +      using sbB by (auto simp add: C_def subset_eq) (metis prod.case prod_encode_inverse)
   1.479  
   1.480 -  show "?outer (\<Union>i. A i) \<le> (\<Sum>n. ?outer (A n))"
   1.481 +    have "?O (\<Union>i. A i) \<le> ?O (\<Union>i. C i)"  
   1.482 +      using A_C A C by (intro increasing_outer_measure[THEN increasingD]) (auto dest!: sets_into_space)
   1.483 +    also have "\<dots> \<le> (\<Sum>i. f (C i))"
   1.484 +      using C by (intro outer_measure_le[OF posf inc]) auto
   1.485 +    also have "\<dots> = (\<Sum>n. \<Sum>i. f (B n i))"
   1.486 +      using B_in_M unfolding C_def comp_def by (intro suminf_ereal_2dimen positiveD2[OF posf]) auto
   1.487 +    also have "\<dots> \<le> (\<Sum>n. ?O (A n) + e*(1/2) ^ Suc n)"
   1.488 +      using B_in_M by (intro suminf_le_pos[OF Ble] suminf_0_le posf[THEN positiveD2]) auto
   1.489 +    also have "... = (\<Sum>n. ?O (A n)) + (\<Sum>n. e*(1/2) ^ Suc n)"
   1.490 +      using e by (subst suminf_add_ereal) (auto simp add: ereal_zero_le_0_iff outer_measure_nonneg posf)
   1.491 +    also have "(\<Sum>n. e*(1/2) ^ Suc n) = e"
   1.492 +      using suminf_half_series_ereal e by (simp add: ereal_zero_le_0_iff suminf_cmult_ereal)
   1.493 +    finally have "?O (\<Union>i. A i) \<le> (\<Sum>n. ?O (A n)) + e" . }
   1.494 +  note * = this
   1.495 +
   1.496 +  show "?O (\<Union>i. A i) \<le> (\<Sum>n. ?O (A n))"
   1.497    proof cases
   1.498 -    assume "\<forall>i. ?outer (A i) \<noteq> \<infinity>"
   1.499 -    with for_finite_Inf show ?thesis
   1.500 +    assume "\<forall>i. ?O (A i) \<noteq> \<infinity>" with * show ?thesis
   1.501        by (intro ereal_le_epsilon) auto
   1.502 -  next
   1.503 -    assume "\<not> (\<forall>i. ?outer (A i) \<noteq> \<infinity>)"
   1.504 -    then have "\<exists>i. ?outer (A i) = \<infinity>"
   1.505 -      by auto
   1.506 -    then have "(\<Sum>n. ?outer (A n)) = \<infinity>"
   1.507 -      using suminf_PInfty[OF inf_measure_pos, OF posf]
   1.508 -      by metis
   1.509 -    then show ?thesis by simp
   1.510 -  qed
   1.511 +  qed (metis suminf_PInfty[OF outer_measure_nonneg, OF posf] ereal_less_eq(1))
   1.512  qed
   1.513  
   1.514 -lemma (in ring_of_sets) inf_measure_outer:
   1.515 -  "\<lbrakk> positive M f ; increasing M f \<rbrakk> \<Longrightarrow>
   1.516 -    outer_measure_space (Pow \<Omega>) (\<lambda>x. Inf (measure_set M f x))"
   1.517 -  using inf_measure_pos[of M f]
   1.518 -  by (simp add: outer_measure_space_def inf_measure_empty
   1.519 -                inf_measure_increasing inf_measure_countably_subadditive positive_def)
   1.520 +lemma (in ring_of_sets) outer_measure_space_outer_measure:
   1.521 +  "positive M f \<Longrightarrow> increasing M f \<Longrightarrow> outer_measure_space (Pow \<Omega>) (outer_measure M f)"
   1.522 +  by (simp add: outer_measure_space_def
   1.523 +    positive_outer_measure increasing_outer_measure countably_subadditive_outer_measure)
   1.524  
   1.525  lemma (in ring_of_sets) algebra_subset_lambda_system:
   1.526    assumes posf: "positive M f" and inc: "increasing M f"
   1.527        and add: "additive M f"
   1.528 -  shows "M \<subseteq> lambda_system \<Omega> (Pow \<Omega>) (\<lambda>x. Inf (measure_set M f x))"
   1.529 +  shows "M \<subseteq> lambda_system \<Omega> (Pow \<Omega>) (outer_measure M f)"
   1.530  proof (auto dest: sets_into_space
   1.531              simp add: algebra.lambda_system_eq [OF algebra_Pow])
   1.532 -  fix x s
   1.533 -  assume x: "x \<in> M"
   1.534 -     and s: "s \<subseteq> \<Omega>"
   1.535 -  have [simp]: "!!x. x \<in> M \<Longrightarrow> s \<inter> (\<Omega> - x) = s-x" using s
   1.536 +  fix x s assume x: "x \<in> M" and s: "s \<subseteq> \<Omega>"
   1.537 +  have [simp]: "\<And>x. x \<in> M \<Longrightarrow> s \<inter> (\<Omega> - x) = s - x" using s
   1.538      by blast
   1.539 -  have "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
   1.540 -        \<le> Inf (measure_set M f s)"
   1.541 -  proof cases
   1.542 -    assume "Inf (measure_set M f s) = \<infinity>" then show ?thesis by simp
   1.543 -  next
   1.544 -    assume fin: "Inf (measure_set M f s) \<noteq> \<infinity>"
   1.545 -    then have "measure_set M f s \<noteq> {}"
   1.546 -      by (auto simp: top_ereal_def)
   1.547 -    show ?thesis
   1.548 -    proof (rule complete_lattice_class.Inf_greatest)
   1.549 -      fix r assume "r \<in> measure_set M f s"
   1.550 -      then obtain A where A: "disjoint_family A" "range A \<subseteq> M" "s \<subseteq> (\<Union>i. A i)"
   1.551 -        and r: "r = (\<Sum>i. f (A i))" unfolding measure_set_def by auto
   1.552 -      have "Inf (measure_set M f (s \<inter> x)) \<le> (\<Sum>i. f (A i \<inter> x))"
   1.553 -        unfolding measure_set_def
   1.554 -      proof (safe intro!: complete_lattice_class.Inf_lower exI[of _ "\<lambda>i. A i \<inter> x"])
   1.555 -        from A(1) show "disjoint_family (\<lambda>i. A i \<inter> x)"
   1.556 -          by (rule disjoint_family_on_bisimulation) auto
   1.557 -      qed (insert x A, auto)
   1.558 -      moreover
   1.559 -      have "Inf (measure_set M f (s - x)) \<le> (\<Sum>i. f (A i - x))"
   1.560 -        unfolding measure_set_def
   1.561 -      proof (safe intro!: complete_lattice_class.Inf_lower exI[of _ "\<lambda>i. A i - x"])
   1.562 -        from A(1) show "disjoint_family (\<lambda>i. A i - x)"
   1.563 -          by (rule disjoint_family_on_bisimulation) auto
   1.564 -      qed (insert x A, auto)
   1.565 -      ultimately have "Inf (measure_set M f (s \<inter> x)) + Inf (measure_set M f (s - x)) \<le>
   1.566 -          (\<Sum>i. f (A i \<inter> x)) + (\<Sum>i. f (A i - x))" by (rule add_mono)
   1.567 -      also have "\<dots> = (\<Sum>i. f (A i \<inter> x) + f (A i - x))"
   1.568 -        using A(2) x posf by (subst suminf_add_ereal) (auto simp: positive_def)
   1.569 -      also have "\<dots> = (\<Sum>i. f (A i))"
   1.570 -        using A x
   1.571 -        by (subst add[THEN additiveD, symmetric])
   1.572 -           (auto intro!: arg_cong[where f=suminf] arg_cong[where f=f])
   1.573 -      finally show "Inf (measure_set M f (s \<inter> x)) + Inf (measure_set M f (s - x)) \<le> r"
   1.574 -        using r by simp
   1.575 -    qed
   1.576 +  have "outer_measure M f (s \<inter> x) + outer_measure M f (s - x) \<le> outer_measure M f s"
   1.577 +    unfolding outer_measure_def[of M f s]
   1.578 +  proof (safe intro!: INF_greatest)
   1.579 +    fix A :: "nat \<Rightarrow> 'a set" assume A: "disjoint_family A" "range A \<subseteq> M" "s \<subseteq> (\<Union>i. A i)"
   1.580 +    have "outer_measure M f (s \<inter> x) \<le> (\<Sum>i. f (A i \<inter> x))"
   1.581 +      unfolding outer_measure_def
   1.582 +    proof (safe intro!: INF_lower2[of "\<lambda>i. A i \<inter> x"])
   1.583 +      from A(1) show "disjoint_family (\<lambda>i. A i \<inter> x)"
   1.584 +        by (rule disjoint_family_on_bisimulation) auto
   1.585 +    qed (insert x A, auto)
   1.586 +    moreover
   1.587 +    have "outer_measure M f (s - x) \<le> (\<Sum>i. f (A i - x))"
   1.588 +      unfolding outer_measure_def
   1.589 +    proof (safe intro!: INF_lower2[of "\<lambda>i. A i - x"])
   1.590 +      from A(1) show "disjoint_family (\<lambda>i. A i - x)"
   1.591 +        by (rule disjoint_family_on_bisimulation) auto
   1.592 +    qed (insert x A, auto)
   1.593 +    ultimately have "outer_measure M f (s \<inter> x) + outer_measure M f (s - x) \<le>
   1.594 +        (\<Sum>i. f (A i \<inter> x)) + (\<Sum>i. f (A i - x))" by (rule add_mono)
   1.595 +    also have "\<dots> = (\<Sum>i. f (A i \<inter> x) + f (A i - x))"
   1.596 +      using A(2) x posf by (subst suminf_add_ereal) (auto simp: positive_def)
   1.597 +    also have "\<dots> = (\<Sum>i. f (A i))"
   1.598 +      using A x
   1.599 +      by (subst add[THEN additiveD, symmetric])
   1.600 +         (auto intro!: arg_cong[where f=suminf] arg_cong[where f=f])
   1.601 +    finally show "outer_measure M f (s \<inter> x) + outer_measure M f (s - x) \<le> (\<Sum>i. f (A i))" .
   1.602    qed
   1.603    moreover
   1.604 -  have "Inf (measure_set M f s)
   1.605 -       \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))"
   1.606 +  have "outer_measure M f s \<le> outer_measure M f (s \<inter> x) + outer_measure M f (s - x)"
   1.607    proof -
   1.608 -    have "Inf (measure_set M f s) = Inf (measure_set M f ((s\<inter>x) \<union> (s-x)))"
   1.609 +    have "outer_measure M f s = outer_measure M f ((s \<inter> x) \<union> (s - x))"
   1.610        by (metis Un_Diff_Int Un_commute)
   1.611 -    also have "... \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))"
   1.612 +    also have "... \<le> outer_measure M f (s \<inter> x) + outer_measure M f (s - x)"
   1.613        apply (rule subadditiveD)
   1.614        apply (rule ring_of_sets.countably_subadditive_subadditive [OF ring_of_sets_Pow])
   1.615 -      apply (simp add: positive_def inf_measure_empty[OF posf] inf_measure_pos[OF posf])
   1.616 -      apply (rule inf_measure_countably_subadditive)
   1.617 +      apply (simp add: positive_def outer_measure_empty[OF posf] outer_measure_nonneg[OF posf])
   1.618 +      apply (rule countably_subadditive_outer_measure)
   1.619        using s by (auto intro!: posf inc)
   1.620      finally show ?thesis .
   1.621    qed
   1.622    ultimately
   1.623 -  show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
   1.624 -        = Inf (measure_set M f s)"
   1.625 +  show "outer_measure M f (s \<inter> x) + outer_measure M f (s - x) = outer_measure M f s"
   1.626      by (rule order_antisym)
   1.627  qed
   1.628  
   1.629 -lemma measure_down:
   1.630 -  "measure_space \<Omega> N \<mu> \<Longrightarrow> sigma_algebra \<Omega> M \<Longrightarrow> M \<subseteq> N \<Longrightarrow> measure_space \<Omega> M \<mu>"
   1.631 +lemma measure_down: "measure_space \<Omega> N \<mu> \<Longrightarrow> sigma_algebra \<Omega> M \<Longrightarrow> M \<subseteq> N \<Longrightarrow> measure_space \<Omega> M \<mu>"
   1.632    by (auto simp add: measure_space_def positive_def countably_additive_def subset_eq)
   1.633  
   1.634  subsection {* Caratheodory's theorem *}
   1.635 @@ -649,11 +517,11 @@
   1.636  proof -
   1.637    have inc: "increasing M f"
   1.638      by (metis additive_increasing ca countably_additive_additive posf)
   1.639 -  let ?infm = "(\<lambda>x. Inf (measure_set M f x))"
   1.640 -  def ls \<equiv> "lambda_system \<Omega> (Pow \<Omega>) ?infm"
   1.641 -  have mls: "measure_space \<Omega> ls ?infm"
   1.642 +  let ?O = "outer_measure M f"
   1.643 +  def ls \<equiv> "lambda_system \<Omega> (Pow \<Omega>) ?O"
   1.644 +  have mls: "measure_space \<Omega> ls ?O"
   1.645      using sigma_algebra.caratheodory_lemma
   1.646 -            [OF sigma_algebra_Pow  inf_measure_outer [OF posf inc]]
   1.647 +            [OF sigma_algebra_Pow outer_measure_space_outer_measure [OF posf inc]]
   1.648      by (simp add: ls_def)
   1.649    hence sls: "sigma_algebra \<Omega> ls"
   1.650      by (simp add: measure_space_def)
   1.651 @@ -663,11 +531,11 @@
   1.652    hence sgs_sb: "sigma_sets (\<Omega>) (M) \<subseteq> ls"
   1.653      using sigma_algebra.sigma_sets_subset [OF sls, of "M"]
   1.654      by simp
   1.655 -  have "measure_space \<Omega> (sigma_sets \<Omega> M) ?infm"
   1.656 +  have "measure_space \<Omega> (sigma_sets \<Omega> M) ?O"
   1.657      by (rule measure_down [OF mls], rule sigma_algebra_sigma_sets)
   1.658         (simp_all add: sgs_sb space_closed)
   1.659 -  thus ?thesis using inf_measure_agrees [OF posf ca]
   1.660 -    by (intro exI[of _ ?infm]) auto
   1.661 +  thus ?thesis using outer_measure_agrees [OF posf ca]
   1.662 +    by (intro exI[of _ ?O]) auto
   1.663  qed
   1.664  
   1.665  lemma (in ring_of_sets) caratheodory_empty_continuous:
   1.666 @@ -1069,5 +937,4 @@
   1.667    then show ?thesis by simp
   1.668  qed
   1.669  
   1.670 -
   1.671  end