src/HOL/Probability/Caratheodory.thy
 changeset 33271 7be66dee1a5a child 33536 fd28b7399f2b
```     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Probability/Caratheodory.thy	Wed Oct 28 11:42:31 2009 +0000
1.3 @@ -0,0 +1,993 @@
1.4 +header {*Caratheodory Extension Theorem*}
1.5 +
1.6 +theory Caratheodory
1.7 +  imports Sigma_Algebra SupInf SeriesPlus
1.8 +
1.9 +begin
1.10 +
1.11 +text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
1.12 +
1.13 +subsection {* Measure Spaces *}
1.14 +
1.15 +text {*A measure assigns a nonnegative real to every measurable set.
1.16 +       It is countably additive for disjoint sets.*}
1.17 +
1.18 +record 'a measure_space = "'a algebra" +
1.19 +  measure:: "'a set \<Rightarrow> real"
1.20 +
1.21 +definition
1.22 +  disjoint_family  where
1.23 +  "disjoint_family A \<longleftrightarrow> (\<forall>m n. m \<noteq> n \<longrightarrow> A m \<inter> A n = {})"
1.24 +
1.25 +definition
1.26 +  positive  where
1.27 +  "positive M f \<longleftrightarrow> f {} = (0::real) & (\<forall>x \<in> sets M. 0 \<le> f x)"
1.28 +
1.29 +definition
1.30 +  additive  where
1.31 +  "additive M f \<longleftrightarrow>
1.32 +    (\<forall>x \<in> sets M. \<forall>y \<in> sets M. x \<inter> y = {}
1.33 +    \<longrightarrow> f (x \<union> y) = f x + f y)"
1.34 +
1.35 +definition
1.36 +  countably_additive  where
1.37 +  "countably_additive M f \<longleftrightarrow>
1.38 +    (\<forall>A. range A \<subseteq> sets M \<longrightarrow>
1.39 +         disjoint_family A \<longrightarrow>
1.40 +         (\<Union>i. A i) \<in> sets M \<longrightarrow>
1.41 +         (\<lambda>n. f (A n))  sums  f (\<Union>i. A i))"
1.42 +
1.43 +definition
1.44 +  increasing  where
1.45 +  "increasing M f \<longleftrightarrow> (\<forall>x \<in> sets M. \<forall>y \<in> sets M. x \<subseteq> y \<longrightarrow> f x \<le> f y)"
1.46 +
1.47 +definition
1.48 +  subadditive  where
1.49 +  "subadditive M f \<longleftrightarrow>
1.50 +    (\<forall>x \<in> sets M. \<forall>y \<in> sets M. x \<inter> y = {}
1.51 +    \<longrightarrow> f (x \<union> y) \<le> f x + f y)"
1.52 +
1.53 +definition
1.54 +  countably_subadditive  where
1.55 +  "countably_subadditive M f \<longleftrightarrow>
1.56 +    (\<forall>A. range A \<subseteq> sets M \<longrightarrow>
1.57 +         disjoint_family A \<longrightarrow>
1.58 +         (\<Union>i. A i) \<in> sets M \<longrightarrow>
1.59 +         summable (f o A) \<longrightarrow>
1.60 +         f (\<Union>i. A i) \<le> suminf (\<lambda>n. f (A n)))"
1.61 +
1.62 +definition
1.63 +  lambda_system where
1.64 +  "lambda_system M f =
1.65 +    {l. l \<in> sets M & (\<forall>x \<in> sets M. f (l \<inter> x) + f ((space M - l) \<inter> x) = f x)}"
1.66 +
1.67 +definition
1.68 +  outer_measure_space where
1.69 +  "outer_measure_space M f  \<longleftrightarrow>
1.70 +     positive M f & increasing M f & countably_subadditive M f"
1.71 +
1.72 +definition
1.73 +  measure_set where
1.74 +  "measure_set M f X =
1.75 +     {r . \<exists>A. range A \<subseteq> sets M & disjoint_family A & X \<subseteq> (\<Union>i. A i) & (f \<circ> A) sums r}"
1.76 +
1.77 +
1.78 +locale measure_space = sigma_algebra +
1.79 +  assumes positive: "!!a. a \<in> sets M \<Longrightarrow> 0 \<le> measure M a"
1.80 +      and empty_measure [simp]: "measure M {} = (0::real)"
1.81 +      and ca: "countably_additive M (measure M)"
1.82 +
1.83 +subsection {* Basic Lemmas *}
1.84 +
1.85 +lemma positive_imp_0: "positive M f \<Longrightarrow> f {} = 0"
1.86 +  by (simp add: positive_def)
1.87 +
1.88 +lemma positive_imp_pos: "positive M f \<Longrightarrow> x \<in> sets M \<Longrightarrow> 0 \<le> f x"
1.89 +  by (simp add: positive_def)
1.90 +
1.91 +lemma increasingD:
1.92 +     "increasing M f \<Longrightarrow> x \<subseteq> y \<Longrightarrow> x\<in>sets M \<Longrightarrow> y\<in>sets M \<Longrightarrow> f x \<le> f y"
1.93 +  by (auto simp add: increasing_def)
1.94 +
1.96 +     "subadditive M f \<Longrightarrow> x \<inter> y = {} \<Longrightarrow> x\<in>sets M \<Longrightarrow> y\<in>sets M
1.97 +      \<Longrightarrow> f (x \<union> y) \<le> f x + f y"
1.98 +  by (auto simp add: subadditive_def)
1.99 +
1.101 +     "additive M f \<Longrightarrow> x \<inter> y = {} \<Longrightarrow> x\<in>sets M \<Longrightarrow> y\<in>sets M
1.102 +      \<Longrightarrow> f (x \<union> y) = f x + f y"
1.103 +  by (auto simp add: additive_def)
1.104 +
1.106 +  "countably_additive M f \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A
1.107 +   \<Longrightarrow> (\<Union>i. A i) \<in> sets M \<Longrightarrow> (\<lambda>n. f (A n))  sums  f (\<Union>i. A i)"
1.109 +
1.110 +lemma Int_Diff_disjoint: "A \<inter> B \<inter> (A - B) = {}"
1.111 +  by blast
1.112 +
1.113 +lemma Int_Diff_Un: "A \<inter> B \<union> (A - B) = A"
1.114 +  by blast
1.115 +
1.116 +lemma disjoint_family_subset:
1.117 +     "disjoint_family A \<Longrightarrow> (!!x. B x \<subseteq> A x) \<Longrightarrow> disjoint_family B"
1.118 +  by (force simp add: disjoint_family_def)
1.119 +
1.120 +subsection {* A Two-Element Series *}
1.121 +
1.122 +definition binaryset :: "'a set \<Rightarrow> 'a set \<Rightarrow> nat \<Rightarrow> 'a set "
1.123 +  where "binaryset A B = (\<lambda>\<^isup>x. {})(0 := A, Suc 0 := B)"
1.124 +
1.125 +lemma range_binaryset_eq: "range(binaryset A B) = {A,B,{}}"
1.126 +  apply (simp add: binaryset_def)
1.127 +  apply (rule set_ext)
1.128 +  apply (auto simp add: image_iff)
1.129 +  done
1.130 +
1.131 +lemma UN_binaryset_eq: "(\<Union>i. binaryset A B i) = A \<union> B"
1.132 +  by (simp add: UNION_eq_Union_image range_binaryset_eq)
1.133 +
1.134 +lemma LIMSEQ_binaryset:
1.135 +  assumes f: "f {} = 0"
1.136 +  shows  "(\<lambda>n. \<Sum>i = 0..<n. f (binaryset A B i)) ----> f A + f B"
1.137 +proof -
1.138 +  have "(\<lambda>n. \<Sum>i = 0..< Suc (Suc n). f (binaryset A B i)) = (\<lambda>n. f A + f B)"
1.139 +    proof
1.140 +      fix n
1.141 +      show "(\<Sum>i\<Colon>nat = 0\<Colon>nat..<Suc (Suc n). f (binaryset A B i)) = f A + f B"
1.142 +	by (induct n)  (auto simp add: binaryset_def f)
1.143 +    qed
1.144 +  moreover
1.145 +  have "... ----> f A + f B" by (rule LIMSEQ_const)
1.146 +  ultimately
1.147 +  have "(\<lambda>n. \<Sum>i = 0..< Suc (Suc n). f (binaryset A B i)) ----> f A + f B"
1.148 +    by metis
1.149 +  hence "(\<lambda>n. \<Sum>i = 0..< n+2. f (binaryset A B i)) ----> f A + f B"
1.150 +    by simp
1.151 +  thus ?thesis by (rule LIMSEQ_offset [where k=2])
1.152 +qed
1.153 +
1.154 +lemma binaryset_sums:
1.155 +  assumes f: "f {} = 0"
1.156 +  shows  "(\<lambda>n. f (binaryset A B n)) sums (f A + f B)"
1.157 +    by (simp add: sums_def LIMSEQ_binaryset [where f=f, OF f])
1.158 +
1.159 +lemma suminf_binaryset_eq:
1.160 +     "f {} = 0 \<Longrightarrow> suminf (\<lambda>n. f (binaryset A B n)) = f A + f B"
1.161 +  by (metis binaryset_sums sums_unique)
1.162 +
1.163 +
1.164 +subsection {* Lambda Systems *}
1.165 +
1.166 +lemma (in algebra) lambda_system_eq:
1.167 +    "lambda_system M f =
1.168 +        {l. l \<in> sets M & (\<forall>x \<in> sets M. f (x \<inter> l) + f (x - l) = f x)}"
1.169 +proof -
1.170 +  have [simp]: "!!l x. l \<in> sets M \<Longrightarrow> x \<in> sets M \<Longrightarrow> (space M - l) \<inter> x = x - l"
1.171 +    by (metis Diff_eq Int_Diff Int_absorb1 Int_commute sets_into_space)
1.172 +  show ?thesis
1.173 +    by (auto simp add: lambda_system_def) (metis Diff_Compl Int_commute)+
1.174 +qed
1.175 +
1.176 +lemma (in algebra) lambda_system_empty:
1.177 +    "positive M f \<Longrightarrow> {} \<in> lambda_system M f"
1.178 +  by (auto simp add: positive_def lambda_system_eq)
1.179 +
1.180 +lemma lambda_system_sets:
1.181 +    "x \<in> lambda_system M f \<Longrightarrow> x \<in> sets M"
1.182 +  by (simp add:  lambda_system_def)
1.183 +
1.184 +lemma (in algebra) lambda_system_Compl:
1.185 +  fixes f:: "'a set \<Rightarrow> real"
1.186 +  assumes x: "x \<in> lambda_system M f"
1.187 +  shows "space M - x \<in> lambda_system M f"
1.188 +  proof -
1.189 +    have "x \<subseteq> space M"
1.190 +      by (metis sets_into_space lambda_system_sets x)
1.191 +    hence "space M - (space M - x) = x"
1.192 +      by (metis double_diff equalityE)
1.193 +    with x show ?thesis
1.194 +      by (force simp add: lambda_system_def)
1.195 +  qed
1.196 +
1.197 +lemma (in algebra) lambda_system_Int:
1.198 +  fixes f:: "'a set \<Rightarrow> real"
1.199 +  assumes xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f"
1.200 +  shows "x \<inter> y \<in> lambda_system M f"
1.201 +  proof -
1.202 +    from xl yl show ?thesis
1.203 +      proof (auto simp add: positive_def lambda_system_eq Int)
1.204 +	fix u
1.205 +	assume x: "x \<in> sets M" and y: "y \<in> sets M" and u: "u \<in> sets M"
1.206 +           and fx: "\<forall>z\<in>sets M. f (z \<inter> x) + f (z - x) = f z"
1.207 +           and fy: "\<forall>z\<in>sets M. f (z \<inter> y) + f (z - y) = f z"
1.208 +	have "u - x \<inter> y \<in> sets M"
1.209 +	  by (metis Diff Diff_Int Un u x y)
1.210 +	moreover
1.211 +	have "(u - (x \<inter> y)) \<inter> y = u \<inter> y - x" by blast
1.212 +	moreover
1.213 +	have "u - x \<inter> y - y = u - y" by blast
1.214 +	ultimately
1.215 +	have ey: "f (u - x \<inter> y) = f (u \<inter> y - x) + f (u - y)" using fy
1.216 +	  by force
1.217 +	have "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y)
1.218 +              = (f (u \<inter> (x \<inter> y)) + f (u \<inter> y - x)) + f (u - y)"
1.219 +	  by (simp add: ey)
1.220 +	also have "... =  (f ((u \<inter> y) \<inter> x) + f (u \<inter> y - x)) + f (u - y)"
1.221 +	  by (simp add: Int_ac)
1.222 +	also have "... = f (u \<inter> y) + f (u - y)"
1.223 +	  using fx [THEN bspec, of "u \<inter> y"] Int y u
1.224 +	  by force
1.225 +	also have "... = f u"
1.226 +	  by (metis fy u)
1.227 +	finally show "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y) = f u" .
1.228 +      qed
1.229 +  qed
1.230 +
1.231 +
1.232 +lemma (in algebra) lambda_system_Un:
1.233 +  fixes f:: "'a set \<Rightarrow> real"
1.234 +  assumes xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f"
1.235 +  shows "x \<union> y \<in> lambda_system M f"
1.236 +proof -
1.237 +  have "(space M - x) \<inter> (space M - y) \<in> sets M"
1.238 +    by (metis Diff_Un Un compl_sets lambda_system_sets xl yl)
1.239 +  moreover
1.240 +  have "x \<union> y = space M - ((space M - x) \<inter> (space M - y))"
1.241 +    by auto  (metis subsetD lambda_system_sets sets_into_space xl yl)+
1.242 +  ultimately show ?thesis
1.243 +    by (metis lambda_system_Compl lambda_system_Int xl yl)
1.244 +qed
1.245 +
1.246 +lemma (in algebra) lambda_system_algebra:
1.247 +    "positive M f \<Longrightarrow> algebra (M (|sets := lambda_system M f|))"
1.248 +  apply (auto simp add: algebra_def)
1.249 +  apply (metis lambda_system_sets set_mp sets_into_space)
1.250 +  apply (metis lambda_system_empty)
1.251 +  apply (metis lambda_system_Compl)
1.252 +  apply (metis lambda_system_Un)
1.253 +  done
1.254 +
1.255 +lemma (in algebra) lambda_system_strong_additive:
1.256 +  assumes z: "z \<in> sets M" and disj: "x \<inter> y = {}"
1.257 +      and xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f"
1.258 +  shows "f (z \<inter> (x \<union> y)) = f (z \<inter> x) + f (z \<inter> y)"
1.259 +  proof -
1.260 +    have "z \<inter> x = (z \<inter> (x \<union> y)) \<inter> x" using disj by blast
1.261 +    moreover
1.262 +    have "z \<inter> y = (z \<inter> (x \<union> y)) - x" using disj by blast
1.263 +    moreover
1.264 +    have "(z \<inter> (x \<union> y)) \<in> sets M"
1.265 +      by (metis Int Un lambda_system_sets xl yl z)
1.266 +    ultimately show ?thesis using xl yl
1.267 +      by (simp add: lambda_system_eq)
1.268 +  qed
1.269 +
1.270 +lemma (in algebra) Int_space_eq1 [simp]: "x \<in> sets M \<Longrightarrow> space M \<inter> x = x"
1.271 +  by (metis Int_absorb1 sets_into_space)
1.272 +
1.273 +lemma (in algebra) Int_space_eq2 [simp]: "x \<in> sets M \<Longrightarrow> x \<inter> space M = x"
1.274 +  by (metis Int_absorb2 sets_into_space)
1.275 +
1.276 +lemma (in algebra) lambda_system_additive:
1.277 +     "additive (M (|sets := lambda_system M f|)) f"
1.278 +  proof (auto simp add: additive_def)
1.279 +    fix x and y
1.280 +    assume disj: "x \<inter> y = {}"
1.281 +       and xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f"
1.282 +    hence  "x \<in> sets M" "y \<in> sets M" by (blast intro: lambda_system_sets)+
1.283 +    thus "f (x \<union> y) = f x + f y"
1.284 +      using lambda_system_strong_additive [OF top disj xl yl]
1.285 +      by (simp add: Un)
1.286 +  qed
1.287 +
1.288 +
1.290 +  assumes f: "positive M f" and cs: "countably_subadditive M f"
1.291 +  shows  "subadditive M f"
1.293 +  fix x y
1.294 +  assume x: "x \<in> sets M" and y: "y \<in> sets M" and "x \<inter> y = {}"
1.295 +  hence "disjoint_family (binaryset x y)"
1.296 +    by (auto simp add: disjoint_family_def binaryset_def)
1.297 +  hence "range (binaryset x y) \<subseteq> sets M \<longrightarrow>
1.298 +         (\<Union>i. binaryset x y i) \<in> sets M \<longrightarrow>
1.299 +         summable (f o (binaryset x y)) \<longrightarrow>
1.300 +         f (\<Union>i. binaryset x y i) \<le> suminf (\<lambda>n. f (binaryset x y n))"
1.301 +    using cs by (simp add: countably_subadditive_def)
1.302 +  hence "{x,y,{}} \<subseteq> sets M \<longrightarrow> x \<union> y \<in> sets M \<longrightarrow>
1.303 +         summable (f o (binaryset x y)) \<longrightarrow>
1.304 +         f (x \<union> y) \<le> suminf (\<lambda>n. f (binaryset x y n))"
1.305 +    by (simp add: range_binaryset_eq UN_binaryset_eq)
1.306 +  thus "f (x \<union> y) \<le>  f x + f y" using f x y binaryset_sums
1.307 +    by (auto simp add: Un sums_iff positive_def o_def)
1.308 +qed
1.309 +
1.310 +
1.311 +definition disjointed :: "(nat \<Rightarrow> 'a set) \<Rightarrow> nat \<Rightarrow> 'a set "
1.312 +  where "disjointed A n = A n - (\<Union>i\<in>{0..<n}. A i)"
1.313 +
1.314 +lemma finite_UN_disjointed_eq: "(\<Union>i\<in>{0..<n}. disjointed A i) = (\<Union>i\<in>{0..<n}. A i)"
1.315 +proof (induct n)
1.316 +  case 0 show ?case by simp
1.317 +next
1.318 +  case (Suc n)
1.319 +  thus ?case by (simp add: atLeastLessThanSuc disjointed_def)
1.320 +qed
1.321 +
1.322 +lemma UN_disjointed_eq: "(\<Union>i. disjointed A i) = (\<Union>i. A i)"
1.323 +  apply (rule UN_finite2_eq [where k=0])
1.324 +  apply (simp add: finite_UN_disjointed_eq)
1.325 +  done
1.326 +
1.327 +lemma less_disjoint_disjointed: "m<n \<Longrightarrow> disjointed A m \<inter> disjointed A n = {}"
1.328 +  by (auto simp add: disjointed_def)
1.329 +
1.330 +lemma disjoint_family_disjointed: "disjoint_family (disjointed A)"
1.331 +  by (simp add: disjoint_family_def)
1.332 +     (metis neq_iff Int_commute less_disjoint_disjointed)
1.333 +
1.334 +lemma disjointed_subset: "disjointed A n \<subseteq> A n"
1.335 +  by (auto simp add: disjointed_def)
1.336 +
1.337 +
1.338 +lemma (in algebra) UNION_in_sets:
1.339 +  fixes A:: "nat \<Rightarrow> 'a set"
1.340 +  assumes A: "range A \<subseteq> sets M "
1.341 +  shows  "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
1.342 +proof (induct n)
1.343 +  case 0 show ?case by simp
1.344 +next
1.345 +  case (Suc n)
1.346 +  thus ?case
1.347 +    by (simp add: atLeastLessThanSuc) (metis A Un UNIV_I image_subset_iff)
1.348 +qed
1.349 +
1.350 +lemma (in algebra) range_disjointed_sets:
1.351 +  assumes A: "range A \<subseteq> sets M "
1.352 +  shows  "range (disjointed A) \<subseteq> sets M"
1.353 +proof (auto simp add: disjointed_def)
1.354 +  fix n
1.355 +  show "A n - (\<Union>i\<in>{0..<n}. A i) \<in> sets M" using UNION_in_sets
1.356 +    by (metis A Diff UNIV_I disjointed_def image_subset_iff)
1.357 +qed
1.358 +
1.359 +lemma sigma_algebra_disjoint_iff:
1.360 +     "sigma_algebra M \<longleftrightarrow>
1.361 +      algebra M &
1.362 +      (\<forall>A. range A \<subseteq> sets M \<longrightarrow> disjoint_family A \<longrightarrow>
1.363 +           (\<Union>i::nat. A i) \<in> sets M)"
1.364 +proof (auto simp add: sigma_algebra_iff)
1.365 +  fix A :: "nat \<Rightarrow> 'a set"
1.366 +  assume M: "algebra M"
1.367 +     and A: "range A \<subseteq> sets M"
1.368 +     and UnA: "\<forall>A. range A \<subseteq> sets M \<longrightarrow>
1.369 +               disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
1.370 +  hence "range (disjointed A) \<subseteq> sets M \<longrightarrow>
1.371 +         disjoint_family (disjointed A) \<longrightarrow>
1.372 +         (\<Union>i. disjointed A i) \<in> sets M" by blast
1.373 +  hence "(\<Union>i. disjointed A i) \<in> sets M"
1.374 +    by (simp add: algebra.range_disjointed_sets M A disjoint_family_disjointed)
1.375 +  thus "(\<Union>i::nat. A i) \<in> sets M" by (simp add: UN_disjointed_eq)
1.376 +qed
1.377 +
1.378 +
1.379 +lemma (in algebra) additive_sum:
1.380 +  fixes A:: "nat \<Rightarrow> 'a set"
1.381 +  assumes f: "positive M f" and ad: "additive M f"
1.382 +      and A: "range A \<subseteq> sets M"
1.383 +      and disj: "disjoint_family A"
1.384 +  shows  "setsum (f o A) {0..<n} = f (\<Union>i\<in>{0..<n}. A i)"
1.385 +proof (induct n)
1.386 +  case 0 show ?case using f by (simp add: positive_def)
1.387 +next
1.388 +  case (Suc n)
1.389 +  have "A n \<inter> (\<Union>i\<in>{0..<n}. A i) = {}" using disj
1.390 +    by (auto simp add: disjoint_family_def neq_iff) blast
1.391 +  moreover
1.392 +  have "A n \<in> sets M" using A by blast
1.393 +  moreover have "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
1.394 +    by (metis A UNION_in_sets atLeast0LessThan)
1.395 +  moreover
1.396 +  ultimately have "f (A n \<union> (\<Union>i\<in>{0..<n}. A i)) = f (A n) + f(\<Union>i\<in>{0..<n}. A i)"
1.397 +    using ad UNION_in_sets A by (auto simp add: additive_def)
1.398 +  with Suc.hyps show ?case using ad
1.399 +    by (auto simp add: atLeastLessThanSuc additive_def)
1.400 +qed
1.401 +
1.402 +
1.404 +  "countably_subadditive M f \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A \<Longrightarrow>
1.405 +   (\<Union>i. A i) \<in> sets M \<Longrightarrow> summable (f o A) \<Longrightarrow> f (\<Union>i. A i) \<le> suminf (f o A)"
1.406 +  by (auto simp add: countably_subadditive_def o_def)
1.407 +
1.408 +lemma (in algebra) increasing_additive_summable:
1.409 +  fixes A:: "nat \<Rightarrow> 'a set"
1.410 +  assumes f: "positive M f" and ad: "additive M f"
1.411 +      and inc: "increasing M f"
1.412 +      and A: "range A \<subseteq> sets M"
1.413 +      and disj: "disjoint_family A"
1.414 +  shows  "summable (f o A)"
1.415 +proof (rule pos_summable)
1.416 +  fix n
1.417 +  show "0 \<le> (f \<circ> A) n" using f A
1.418 +    by (force simp add: positive_def)
1.419 +  next
1.420 +  fix n
1.421 +  have "setsum (f \<circ> A) {0..<n} = f (\<Union>i\<in>{0..<n}. A i)"
1.422 +    by (rule additive_sum [OF f ad A disj])
1.423 +  also have "... \<le> f (space M)" using space_closed A
1.424 +    by (blast intro: increasingD [OF inc] UNION_in_sets top)
1.425 +  finally show "setsum (f \<circ> A) {0..<n} \<le> f (space M)" .
1.426 +qed
1.427 +
1.428 +lemma lambda_system_positive:
1.429 +     "positive M f \<Longrightarrow> positive (M (|sets := lambda_system M f|)) f"
1.430 +  by (simp add: positive_def lambda_system_def)
1.431 +
1.432 +lemma lambda_system_increasing:
1.433 +   "increasing M f \<Longrightarrow> increasing (M (|sets := lambda_system M f|)) f"
1.434 +  by (simp add: increasing_def lambda_system_def)
1.435 +
1.436 +lemma (in algebra) lambda_system_strong_sum:
1.437 +  fixes A:: "nat \<Rightarrow> 'a set"
1.438 +  assumes f: "positive M f" and a: "a \<in> sets M"
1.439 +      and A: "range A \<subseteq> lambda_system M f"
1.440 +      and disj: "disjoint_family A"
1.441 +  shows  "(\<Sum>i = 0..<n. f (a \<inter>A i)) = f (a \<inter> (\<Union>i\<in>{0..<n}. A i))"
1.442 +proof (induct n)
1.443 +  case 0 show ?case using f by (simp add: positive_def)
1.444 +next
1.445 +  case (Suc n)
1.446 +  have 2: "A n \<inter> UNION {0..<n} A = {}" using disj
1.447 +    by (force simp add: disjoint_family_def neq_iff)
1.448 +  have 3: "A n \<in> lambda_system M f" using A
1.449 +    by blast
1.450 +  have 4: "UNION {0..<n} A \<in> lambda_system M f"
1.451 +    using A algebra.UNION_in_sets [OF local.lambda_system_algebra [OF f]]
1.452 +    by simp
1.453 +  from Suc.hyps show ?case
1.454 +    by (simp add: atLeastLessThanSuc lambda_system_strong_additive [OF a 2 3 4])
1.455 +qed
1.456 +
1.457 +
1.458 +lemma (in sigma_algebra) lambda_system_caratheodory:
1.459 +  assumes oms: "outer_measure_space M f"
1.460 +      and A: "range A \<subseteq> lambda_system M f"
1.461 +      and disj: "disjoint_family A"
1.462 +  shows  "(\<Union>i. A i) \<in> lambda_system M f & (f \<circ> A)  sums  f (\<Union>i. A i)"
1.463 +proof -
1.464 +  have pos: "positive M f" and inc: "increasing M f"
1.465 +   and csa: "countably_subadditive M f"
1.466 +    by (metis oms outer_measure_space_def)+
1.467 +  have sa: "subadditive M f"
1.468 +    by (metis countably_subadditive_subadditive csa pos)
1.469 +  have A': "range A \<subseteq> sets (M(|sets := lambda_system M f|))" using A
1.470 +    by simp
1.471 +  have alg_ls: "algebra (M(|sets := lambda_system M f|))"
1.472 +    by (rule lambda_system_algebra [OF pos])
1.473 +  have A'': "range A \<subseteq> sets M"
1.474 +     by (metis A image_subset_iff lambda_system_sets)
1.475 +  have sumfA: "summable (f \<circ> A)"
1.476 +    by (metis algebra.increasing_additive_summable [OF alg_ls]
1.477 +          lambda_system_positive lambda_system_additive lambda_system_increasing
1.478 +          A' oms outer_measure_space_def disj)
1.479 +  have U_in: "(\<Union>i. A i) \<in> sets M"
1.480 +    by (metis A countable_UN image_subset_iff lambda_system_sets)
1.481 +  have U_eq: "f (\<Union>i. A i) = suminf (f o A)"
1.482 +    proof (rule antisym)
1.483 +      show "f (\<Union>i. A i) \<le> suminf (f \<circ> A)"
1.484 +	by (rule countably_subadditiveD [OF csa A'' disj U_in sumfA])
1.485 +      show "suminf (f \<circ> A) \<le> f (\<Union>i. A i)"
1.486 +	by (rule suminf_le [OF sumfA])
1.487 +           (metis algebra.additive_sum [OF alg_ls] pos disj UN_Un Un_UNIV_right
1.488 +	          lambda_system_positive lambda_system_additive
1.489 +                  subset_Un_eq increasingD [OF inc] A' A'' UNION_in_sets U_in)
1.490 +    qed
1.491 +  {
1.492 +    fix a
1.493 +    assume a [iff]: "a \<in> sets M"
1.494 +    have "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) = f a"
1.495 +    proof -
1.496 +      have summ: "summable (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)" using pos A''
1.497 +	apply -
1.498 +	apply (rule summable_comparison_test [OF _ sumfA])
1.499 +	apply (rule_tac x="0" in exI)
1.500 +	apply (simp add: positive_def)
1.501 +	apply (auto simp add: )
1.502 +	apply (subst abs_of_nonneg)
1.503 +	apply (metis A'' Int UNIV_I a image_subset_iff)
1.504 +	apply (blast intro:  increasingD [OF inc] a)
1.505 +	done
1.506 +      show ?thesis
1.507 +      proof (rule antisym)
1.508 +	have "range (\<lambda>i. a \<inter> A i) \<subseteq> sets M" using A''
1.509 +	  by blast
1.510 +	moreover
1.511 +	have "disjoint_family (\<lambda>i. a \<inter> A i)" using disj
1.512 +	  by (auto simp add: disjoint_family_def)
1.513 +	moreover
1.514 +	have "a \<inter> (\<Union>i. A i) \<in> sets M"
1.515 +	  by (metis Int U_in a)
1.516 +	ultimately
1.517 +	have "f (a \<inter> (\<Union>i. A i)) \<le> suminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)"
1.518 +	  using countably_subadditiveD [OF csa, of "(\<lambda>i. a \<inter> A i)"] summ
1.519 +	  by (simp add: o_def)
1.520 +	moreover
1.521 +	have "suminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)  \<le> f a - f (a - (\<Union>i. A i))"
1.522 +	  proof (rule suminf_le [OF summ])
1.523 +	    fix n
1.524 +	    have UNION_in: "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
1.525 +	      by (metis A'' UNION_in_sets)
1.526 +	    have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A''
1.527 +	      by (blast intro: increasingD [OF inc] A'' Int UNION_in_sets a)
1.528 +	    have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system M f"
1.529 +	      using algebra.UNION_in_sets [OF lambda_system_algebra [OF pos]]
1.530 +	      by (simp add: A)
1.531 +	    hence eq_fa: "f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i)) = f a"
1.532 +	      by (simp add: lambda_system_eq UNION_in Diff_Compl a)
1.533 +	    have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))"
1.534 +	      by (blast intro: increasingD [OF inc] Diff UNION_eq_Union_image
1.535 +                               UNION_in U_in a)
1.536 +	    thus "setsum (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) {0..<n} \<le> f a - f (a - (\<Union>i. A i))"
1.537 +	      using eq_fa
1.538 +	      by (simp add: suminf_le [OF summ] lambda_system_strong_sum pos
1.539 +                            a A disj)
1.540 +	  qed
1.541 +	ultimately show "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le> f a"
1.542 +	  by arith
1.543 +      next
1.544 +	have "f a \<le> f (a \<inter> (\<Union>i. A i) \<union> (a - (\<Union>i. A i)))"
1.545 +	  by (blast intro:  increasingD [OF inc] a U_in)
1.546 +	also have "... \<le>  f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))"
1.547 +	  by (blast intro: subadditiveD [OF sa] Int Diff U_in)
1.548 +	finally show "f a \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))" .
1.549 +        qed
1.550 +     qed
1.551 +  }
1.552 +  thus  ?thesis
1.553 +    by (simp add: lambda_system_eq sums_iff U_eq U_in sumfA)
1.554 +qed
1.555 +
1.556 +lemma (in sigma_algebra) caratheodory_lemma:
1.557 +  assumes oms: "outer_measure_space M f"
1.558 +  shows "measure_space (|space = space M, sets = lambda_system M f, measure = f|)"
1.559 +proof -
1.560 +  have pos: "positive M f"
1.561 +    by (metis oms outer_measure_space_def)
1.562 +  have alg: "algebra (|space = space M, sets = lambda_system M f, measure = f|)"
1.563 +    using lambda_system_algebra [OF pos]
1.564 +    by (simp add: algebra_def)
1.565 +  then moreover
1.566 +  have "sigma_algebra (|space = space M, sets = lambda_system M f, measure = f|)"
1.567 +    using lambda_system_caratheodory [OF oms]
1.568 +    by (simp add: sigma_algebra_disjoint_iff)
1.569 +  moreover
1.570 +  have "measure_space_axioms (|space = space M, sets = lambda_system M f, measure = f|)"
1.571 +    using pos lambda_system_caratheodory [OF oms]
1.572 +    by (simp add: measure_space_axioms_def positive_def lambda_system_sets
1.573 +                  countably_additive_def o_def)
1.574 +  ultimately
1.575 +  show ?thesis
1.576 +    by intro_locales (auto simp add: sigma_algebra_def)
1.577 +qed
1.578 +
1.579 +
1.580 +lemma (in algebra) inf_measure_nonempty:
1.581 +  assumes f: "positive M f" and b: "b \<in> sets M" and a: "a \<subseteq> b"
1.582 +  shows "f b \<in> measure_set M f a"
1.583 +proof -
1.584 +  have "(f \<circ> (\<lambda>i. {})(0 := b)) sums setsum (f \<circ> (\<lambda>i. {})(0 := b)) {0..<1::nat}"
1.585 +    by (rule series_zero)  (simp add: positive_imp_0 [OF f])
1.586 +  also have "... = f b"
1.587 +    by simp
1.588 +  finally have "(f \<circ> (\<lambda>i. {})(0 := b)) sums f b" .
1.589 +  thus ?thesis using a
1.590 +    by (auto intro!: exI [of _ "(\<lambda>i. {})(0 := b)"]
1.591 +             simp add: measure_set_def disjoint_family_def b split_if_mem2)
1.592 +qed
1.593 +
1.594 +lemma (in algebra) inf_measure_pos0:
1.595 +     "positive M f \<Longrightarrow> x \<in> measure_set M f a \<Longrightarrow> 0 \<le> x"
1.596 +apply (auto simp add: positive_def measure_set_def sums_iff intro!: suminf_ge_zero)
1.597 +apply blast
1.598 +done
1.599 +
1.600 +lemma (in algebra) inf_measure_pos:
1.601 +  shows "positive M f \<Longrightarrow> x \<subseteq> space M \<Longrightarrow> 0 \<le> Inf (measure_set M f x)"
1.602 +apply (rule Inf_greatest)
1.603 +apply (metis emptyE inf_measure_nonempty top)
1.604 +apply (metis inf_measure_pos0)
1.605 +done
1.606 +
1.607 +lemma (in algebra) additive_increasing:
1.608 +  assumes posf: "positive M f" and addf: "additive M f"
1.609 +  shows "increasing M f"
1.610 +proof (auto simp add: increasing_def)
1.611 +  fix x y
1.612 +  assume xy: "x \<in> sets M" "y \<in> sets M" "x \<subseteq> y"
1.613 +  have "f x \<le> f x + f (y-x)" using posf
1.614 +    by (simp add: positive_def) (metis Diff xy)
1.615 +  also have "... = f (x \<union> (y-x))" using addf
1.616 +    by (auto simp add: additive_def) (metis Diff_disjoint Un_Diff_cancel Diff xy)
1.617 +  also have "... = f y"
1.618 +    by (metis Un_Diff_cancel Un_absorb1 xy)
1.619 +  finally show "f x \<le> f y" .
1.620 +qed
1.621 +
1.623 +  assumes posf: "positive M f" and ca: "countably_additive M f"
1.624 +  shows "additive M f"
1.626 +  fix x y
1.627 +  assume x: "x \<in> sets M" and y: "y \<in> sets M" and "x \<inter> y = {}"
1.628 +  hence "disjoint_family (binaryset x y)"
1.629 +    by (auto simp add: disjoint_family_def binaryset_def)
1.630 +  hence "range (binaryset x y) \<subseteq> sets M \<longrightarrow>
1.631 +         (\<Union>i. binaryset x y i) \<in> sets M \<longrightarrow>
1.632 +         f (\<Union>i. binaryset x y i) = suminf (\<lambda>n. f (binaryset x y n))"
1.633 +    using ca
1.634 +    by (simp add: countably_additive_def) (metis UN_binaryset_eq sums_unique)
1.635 +  hence "{x,y,{}} \<subseteq> sets M \<longrightarrow> x \<union> y \<in> sets M \<longrightarrow>
1.636 +         f (x \<union> y) = suminf (\<lambda>n. f (binaryset x y n))"
1.637 +    by (simp add: range_binaryset_eq UN_binaryset_eq)
1.638 +  thus "f (x \<union> y) = f x + f y" using posf x y
1.639 +    by (simp add: Un suminf_binaryset_eq positive_def)
1.640 +qed
1.641 +
1.642 +lemma (in algebra) inf_measure_agrees:
1.643 +  assumes posf: "positive M f" and ca: "countably_additive M f"
1.644 +      and s: "s \<in> sets M"
1.645 +  shows "Inf (measure_set M f s) = f s"
1.646 +proof (rule Inf_eq)
1.647 +  fix z
1.648 +  assume z: "z \<in> measure_set M f s"
1.649 +  from this obtain A where
1.650 +    A: "range A \<subseteq> sets M" and disj: "disjoint_family A"
1.651 +    and "s \<subseteq> (\<Union>x. A x)" and sm: "summable (f \<circ> A)"
1.652 +    and si: "suminf (f \<circ> A) = z"
1.653 +    by (auto simp add: measure_set_def sums_iff)
1.654 +  hence seq: "s = (\<Union>i. A i \<inter> s)" by blast
1.655 +  have inc: "increasing M f"
1.657 +  have sums: "(\<lambda>i. f (A i \<inter> s)) sums f (\<Union>i. A i \<inter> s)"
1.658 +    proof (rule countably_additiveD [OF ca])
1.659 +      show "range (\<lambda>n. A n \<inter> s) \<subseteq> sets M" using A s
1.660 +	by blast
1.661 +      show "disjoint_family (\<lambda>n. A n \<inter> s)" using disj
1.662 +	by (auto simp add: disjoint_family_def)
1.663 +      show "(\<Union>i. A i \<inter> s) \<in> sets M" using A s
1.664 +	by (metis UN_extend_simps(4) s seq)
1.665 +    qed
1.666 +  hence "f s = suminf (\<lambda>i. f (A i \<inter> s))"
1.667 +    by (metis Int_commute UN_simps(4) seq sums_iff)
1.668 +  also have "... \<le> suminf (f \<circ> A)"
1.669 +    proof (rule summable_le [OF _ _ sm])
1.670 +      show "\<forall>n. f (A n \<inter> s) \<le> (f \<circ> A) n" using A s
1.671 +	by (force intro: increasingD [OF inc])
1.672 +      show "summable (\<lambda>i. f (A i \<inter> s))" using sums
1.673 +	by (simp add: sums_iff)
1.674 +    qed
1.675 +  also have "... = z" by (rule si)
1.676 +  finally show "f s \<le> z" .
1.677 +next
1.678 +  fix y
1.679 +  assume y: "!!u. u \<in> measure_set M f s \<Longrightarrow> y \<le> u"
1.680 +  thus "y \<le> f s"
1.681 +    by (blast intro: inf_measure_nonempty [OF posf s subset_refl])
1.682 +qed
1.683 +
1.684 +lemma (in algebra) inf_measure_empty:
1.685 +  assumes posf: "positive M f"
1.686 +  shows "Inf (measure_set M f {}) = 0"
1.687 +proof (rule antisym)
1.688 +  show "0 \<le> Inf (measure_set M f {})"
1.689 +    by (metis empty_subsetI inf_measure_pos posf)
1.690 +  show "Inf (measure_set M f {}) \<le> 0"
1.691 +    by (metis Inf_lower empty_sets inf_measure_pos0 inf_measure_nonempty posf
1.692 +              positive_imp_0 subset_refl)
1.693 +qed
1.694 +
1.695 +lemma (in algebra) inf_measure_positive:
1.696 +  "positive M f \<Longrightarrow>
1.697 +   positive (| space = space M, sets = Pow (space M) |)
1.698 +                  (\<lambda>x. Inf (measure_set M f x))"
1.699 +  by (simp add: positive_def inf_measure_empty inf_measure_pos)
1.700 +
1.701 +lemma (in algebra) inf_measure_increasing:
1.702 +  assumes posf: "positive M f"
1.703 +  shows "increasing (| space = space M, sets = Pow (space M) |)
1.704 +                    (\<lambda>x. Inf (measure_set M f x))"
1.705 +apply (auto simp add: increasing_def)
1.706 +apply (rule Inf_greatest, metis emptyE inf_measure_nonempty top posf)
1.707 +apply (rule Inf_lower)
1.708 +apply (clarsimp simp add: measure_set_def, blast)
1.709 +apply (blast intro: inf_measure_pos0 posf)
1.710 +done
1.711 +
1.712 +
1.713 +lemma (in algebra) inf_measure_le:
1.714 +  assumes posf: "positive M f" and inc: "increasing M f"
1.715 +      and x: "x \<in> {r . \<exists>A. range A \<subseteq> sets M & s \<subseteq> (\<Union>i. A i) & (f \<circ> A) sums r}"
1.716 +  shows "Inf (measure_set M f s) \<le> x"
1.717 +proof -
1.718 +  from x
1.719 +  obtain A where A: "range A \<subseteq> sets M" and ss: "s \<subseteq> (\<Union>i. A i)"
1.720 +             and sm: "summable (f \<circ> A)" and xeq: "suminf (f \<circ> A) = x"
1.721 +    by (auto simp add: sums_iff)
1.722 +  have dA: "range (disjointed A) \<subseteq> sets M"
1.723 +    by (metis A range_disjointed_sets)
1.724 +  have "\<forall>n. \<bar>(f o disjointed A) n\<bar> \<le> (f \<circ> A) n"
1.725 +    proof (auto)
1.726 +      fix n
1.727 +      have "\<bar>f (disjointed A n)\<bar> = f (disjointed A n)" using posf dA
1.728 +	by (auto simp add: positive_def image_subset_iff)
1.729 +      also have "... \<le> f (A n)"
1.730 +	by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A)
1.731 +      finally show "\<bar>f (disjointed A n)\<bar> \<le> f (A n)" .
1.732 +    qed
1.733 +  from Series.summable_le2 [OF this sm]
1.734 +  have sda:  "summable (f o disjointed A)"
1.735 +             "suminf (f o disjointed A) \<le> suminf (f \<circ> A)"
1.736 +    by blast+
1.737 +  hence ley: "suminf (f o disjointed A) \<le> x"
1.738 +    by (metis xeq)
1.739 +  from sda have "(f \<circ> disjointed A) sums suminf (f \<circ> disjointed A)"
1.740 +    by (simp add: sums_iff)
1.741 +  hence y: "suminf (f o disjointed A) \<in> measure_set M f s"
1.742 +    apply (auto simp add: measure_set_def)
1.743 +    apply (rule_tac x="disjointed A" in exI)
1.744 +    apply (simp add: disjoint_family_disjointed UN_disjointed_eq ss dA)
1.745 +    done
1.746 +  show ?thesis
1.747 +    by (blast intro: Inf_lower y order_trans [OF _ ley] inf_measure_pos0 posf)
1.748 +qed
1.749 +
1.750 +lemma (in algebra) inf_measure_close:
1.751 +  assumes posf: "positive M f" and e: "0 < e" and ss: "s \<subseteq> (space M)"
1.752 +  shows "\<exists>A l. range A \<subseteq> sets M & disjoint_family A & s \<subseteq> (\<Union>i. A i) &
1.753 +               (f \<circ> A) sums l & l \<le> Inf (measure_set M f s) + e"
1.754 +proof -
1.755 +  have " measure_set M f s \<noteq> {}"
1.756 +    by (metis emptyE ss inf_measure_nonempty [OF posf top])
1.757 +  hence "\<exists>l \<in> measure_set M f s. l < Inf (measure_set M f s) + e"
1.758 +    by (rule Inf_close [OF _ e])
1.759 +  thus ?thesis
1.760 +    by (auto simp add: measure_set_def, rule_tac x=" A" in exI, auto)
1.761 +qed
1.762 +
1.763 +lemma (in algebra) inf_measure_countably_subadditive:
1.764 +  assumes posf: "positive M f" and inc: "increasing M f"
1.765 +  shows "countably_subadditive (| space = space M, sets = Pow (space M) |)
1.766 +                  (\<lambda>x. Inf (measure_set M f x))"
1.767 +proof (auto simp add: countably_subadditive_def o_def, rule field_le_epsilon)
1.768 +  fix A :: "nat \<Rightarrow> 'a set" and e :: real
1.769 +    assume A: "range A \<subseteq> Pow (space M)"
1.770 +       and disj: "disjoint_family A"
1.771 +       and sb: "(\<Union>i. A i) \<subseteq> space M"
1.772 +       and sum1: "summable (\<lambda>n. Inf (measure_set M f (A n)))"
1.773 +       and e: "0 < e"
1.774 +    have "!!n. \<exists>B l. range B \<subseteq> sets M \<and> disjoint_family B \<and> A n \<subseteq> (\<Union>i. B i) \<and>
1.775 +                    (f o B) sums l \<and>
1.776 +                    l \<le> Inf (measure_set M f (A n)) + e * (1/2)^(Suc n)"
1.777 +      apply (rule inf_measure_close [OF posf])
1.778 +      apply (metis e half mult_pos_pos zero_less_power)
1.779 +      apply (metis UNIV_I UN_subset_iff sb)
1.780 +      done
1.781 +    hence "\<exists>BB ll. \<forall>n. range (BB n) \<subseteq> sets M \<and> disjoint_family (BB n) \<and>
1.782 +                       A n \<subseteq> (\<Union>i. BB n i) \<and> (f o BB n) sums ll n \<and>
1.783 +                       ll n \<le> Inf (measure_set M f (A n)) + e * (1/2)^(Suc n)"
1.784 +      by (rule choice2)
1.785 +    then obtain BB ll
1.786 +      where BB: "!!n. (range (BB n) \<subseteq> sets M)"
1.787 +        and disjBB: "!!n. disjoint_family (BB n)"
1.788 +        and sbBB: "!!n. A n \<subseteq> (\<Union>i. BB n i)"
1.789 +        and BBsums: "!!n. (f o BB n) sums ll n"
1.790 +        and ll: "!!n. ll n \<le> Inf (measure_set M f (A n)) + e * (1/2)^(Suc n)"
1.791 +      by auto blast
1.792 +    have llpos: "!!n. 0 \<le> ll n"
1.793 +	by (metis BBsums sums_iff o_apply posf positive_imp_pos suminf_ge_zero
1.794 +              range_subsetD BB)
1.795 +    have sll: "summable ll &
1.796 +               suminf ll \<le> suminf (\<lambda>n. Inf (measure_set M f (A n))) + e"
1.797 +      proof -
1.798 +	have "(\<lambda>n. e * (1/2)^(Suc n)) sums (e*1)"
1.799 +	  by (rule sums_mult [OF power_half_series])
1.800 +	hence sum0: "summable (\<lambda>n. e * (1 / 2) ^ Suc n)"
1.801 +	  and eqe:  "(\<Sum>n. e * (1 / 2) ^ n / 2) = e"
1.802 +	  by (auto simp add: sums_iff)
1.803 +	have 0: "suminf (\<lambda>n. Inf (measure_set M f (A n))) +
1.804 +                 suminf (\<lambda>n. e * (1/2)^(Suc n)) =
1.805 +                 suminf (\<lambda>n. Inf (measure_set M f (A n)) + e * (1/2)^(Suc n))"
1.806 +	  by (rule suminf_add [OF sum1 sum0])
1.807 +	have 1: "\<forall>n. \<bar>ll n\<bar> \<le> Inf (measure_set M f (A n)) + e * (1/2) ^ Suc n"
1.808 +	  by (metis ll llpos abs_of_nonneg)
1.809 +	have 2: "summable (\<lambda>n. Inf (measure_set M f (A n)) + e*(1/2)^(Suc n))"
1.810 +	  by (rule summable_add [OF sum1 sum0])
1.811 +	have "suminf ll \<le> (\<Sum>n. Inf (measure_set M f (A n)) + e*(1/2) ^ Suc n)"
1.812 +	  using Series.summable_le2 [OF 1 2] by auto
1.813 +	also have "... = (\<Sum>n. Inf (measure_set M f (A n))) +
1.814 +                         (\<Sum>n. e * (1 / 2) ^ Suc n)"
1.815 +	  by (metis 0)
1.816 +	also have "... = (\<Sum>n. Inf (measure_set M f (A n))) + e"
1.817 +	  by (simp add: eqe)
1.818 +	finally show ?thesis using  Series.summable_le2 [OF 1 2] by auto
1.819 +      qed
1.820 +    def C \<equiv> "(split BB) o nat_to_nat2"
1.821 +    have C: "!!n. C n \<in> sets M"
1.822 +      apply (rule_tac p="nat_to_nat2 n" in PairE)
1.823 +      apply (simp add: C_def)
1.824 +      apply (metis BB subsetD rangeI)
1.825 +      done
1.826 +    have sbC: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)"
1.827 +      proof (auto simp add: C_def)
1.828 +	fix x i
1.829 +	assume x: "x \<in> A i"
1.830 +	with sbBB [of i] obtain j where "x \<in> BB i j"
1.831 +	  by blast
1.832 +	thus "\<exists>i. x \<in> split BB (nat_to_nat2 i)"
1.833 +	  by (metis nat_to_nat2_surj internal_split_def prod.cases
1.834 +                prod_case_split surj_f_inv_f)
1.835 +      qed
1.836 +    have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> nat_to_nat2"
1.837 +      by (rule ext)  (auto simp add: C_def)
1.838 +    also have "... sums suminf ll"
1.839 +      proof (rule suminf_2dimen)
1.840 +	show "\<And>m n. 0 \<le> (f \<circ> (\<lambda>(x, y). BB x y)) (m, n)" using posf BB
1.841 +	  by (force simp add: positive_def)
1.842 +	show "\<And>m. (\<lambda>n. (f \<circ> (\<lambda>(x, y). BB x y)) (m, n)) sums ll m"using BBsums BB
1.843 +	  by (force simp add: o_def)
1.844 +	show "summable ll" using sll
1.845 +	  by auto
1.846 +      qed
1.847 +    finally have Csums: "(f \<circ> C) sums suminf ll" .
1.848 +    have "Inf (measure_set M f (\<Union>i. A i)) \<le> suminf ll"
1.849 +      apply (rule inf_measure_le [OF posf inc], auto)
1.850 +      apply (rule_tac x="C" in exI)
1.851 +      apply (auto simp add: C sbC Csums)
1.852 +      done
1.853 +    also have "... \<le> (\<Sum>n. Inf (measure_set M f (A n))) + e" using sll
1.854 +      by blast
1.855 +    finally show "Inf (measure_set M f (\<Union>i. A i)) \<le>
1.856 +          (\<Sum>n. Inf (measure_set M f (A n))) + e" .
1.857 +qed
1.858 +
1.859 +lemma (in algebra) inf_measure_outer:
1.860 +  "positive M f \<Longrightarrow> increasing M f
1.861 +   \<Longrightarrow> outer_measure_space (| space = space M, sets = Pow (space M) |)
1.862 +                          (\<lambda>x. Inf (measure_set M f x))"
1.863 +  by (simp add: outer_measure_space_def inf_measure_positive
1.864 +                inf_measure_increasing inf_measure_countably_subadditive)
1.865 +
1.866 +(*MOVE UP*)
1.867 +
1.868 +lemma (in algebra) algebra_subset_lambda_system:
1.869 +  assumes posf: "positive M f" and inc: "increasing M f"
1.870 +      and add: "additive M f"
1.871 +  shows "sets M \<subseteq> lambda_system (| space = space M, sets = Pow (space M) |)
1.872 +                                (\<lambda>x. Inf (measure_set M f x))"
1.873 +proof (auto dest: sets_into_space
1.874 +            simp add: algebra.lambda_system_eq [OF algebra_Pow])
1.875 +  fix x s
1.876 +  assume x: "x \<in> sets M"
1.877 +     and s: "s \<subseteq> space M"
1.878 +  have [simp]: "!!x. x \<in> sets M \<Longrightarrow> s \<inter> (space M - x) = s-x" using s
1.879 +    by blast
1.880 +  have "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
1.881 +        \<le> Inf (measure_set M f s)"
1.882 +    proof (rule field_le_epsilon)
1.883 +      fix e :: real
1.884 +      assume e: "0 < e"
1.885 +      from inf_measure_close [OF posf e s]
1.886 +      obtain A l where A: "range A \<subseteq> sets M" and disj: "disjoint_family A"
1.887 +                   and sUN: "s \<subseteq> (\<Union>i. A i)" and fsums: "(f \<circ> A) sums l"
1.888 +	           and l: "l \<le> Inf (measure_set M f s) + e"
1.889 +	by auto
1.890 +      have [simp]: "!!x. x \<in> sets M \<Longrightarrow>
1.891 +                      (f o (\<lambda>z. z \<inter> (space M - x)) o A) = (f o (\<lambda>z. z - x) o A)"
1.892 +	by (rule ext, simp, metis A Int_Diff Int_space_eq2 range_subsetD)
1.893 +      have  [simp]: "!!n. f (A n \<inter> x) + f (A n - x) = f (A n)"
1.894 +	by (subst additiveD [OF add, symmetric])
1.895 + 	   (auto simp add: x range_subsetD [OF A] Int_Diff_Un Int_Diff_disjoint)
1.896 +      have fsumb: "summable (f \<circ> A)"
1.897 +	by (metis fsums sums_iff)
1.898 +      { fix u
1.899 +	assume u: "u \<in> sets M"
1.900 +	have [simp]: "\<And>n. \<bar>f (A n \<inter> u)\<bar> \<le> f (A n)"
1.901 +	  by (simp add: positive_imp_pos [OF posf]  increasingD [OF inc]
1.902 +                        u Int  range_subsetD [OF A])
1.903 +	have 1: "summable (f o (\<lambda>z. z\<inter>u) o A)"
1.904 +          by (rule summable_comparison_test [OF _ fsumb]) simp
1.905 +	have 2: "Inf (measure_set M f (s\<inter>u)) \<le> suminf (f o (\<lambda>z. z\<inter>u) o A)"
1.906 +          proof (rule Inf_lower)
1.907 +            show "suminf (f \<circ> (\<lambda>z. z \<inter> u) \<circ> A) \<in> measure_set M f (s \<inter> u)"
1.908 +              apply (simp add: measure_set_def)
1.909 +              apply (rule_tac x="(\<lambda>z. z \<inter> u) o A" in exI)
1.910 +              apply (auto simp add: disjoint_family_subset [OF disj])
1.911 +              apply (blast intro: u range_subsetD [OF A])
1.912 +              apply (blast dest: subsetD [OF sUN])
1.913 +              apply (metis 1 o_assoc sums_iff)
1.914 +              done
1.915 +          next
1.916 +            show "\<And>x. x \<in> measure_set M f (s \<inter> u) \<Longrightarrow> 0 \<le> x"
1.917 +              by (blast intro: inf_measure_pos0 [OF posf])
1.918 +            qed
1.919 +          note 1 2
1.920 +      } note lesum = this
1.921 +      have sum1: "summable (f o (\<lambda>z. z\<inter>x) o A)"
1.922 +        and inf1: "Inf (measure_set M f (s\<inter>x)) \<le> suminf (f o (\<lambda>z. z\<inter>x) o A)"
1.923 +        and sum2: "summable (f o (\<lambda>z. z \<inter> (space M - x)) o A)"
1.924 +        and inf2: "Inf (measure_set M f (s \<inter> (space M - x)))
1.925 +                   \<le> suminf (f o (\<lambda>z. z \<inter> (space M - x)) o A)"
1.926 +	by (metis Diff lesum top x)+
1.927 +      hence "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
1.928 +           \<le> suminf (f o (\<lambda>s. s\<inter>x) o A) + suminf (f o (\<lambda>s. s-x) o A)"
1.929 +	by (simp add: x)
1.930 +      also have "... \<le> suminf (f o A)" using suminf_add [OF sum1 sum2]
1.931 +	by (simp add: x) (simp add: o_def)
1.932 +      also have "... \<le> Inf (measure_set M f s) + e"
1.933 +	by (metis fsums l sums_unique)
1.934 +      finally show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
1.935 +        \<le> Inf (measure_set M f s) + e" .
1.936 +    qed
1.937 +  moreover
1.938 +  have "Inf (measure_set M f s)
1.939 +       \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))"
1.940 +    proof -
1.941 +    have "Inf (measure_set M f s) = Inf (measure_set M f ((s\<inter>x) \<union> (s-x)))"
1.942 +      by (metis Un_Diff_Int Un_commute)
1.943 +    also have "... \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))"
1.944 +      apply (rule subadditiveD)
1.945 +      apply (iprover intro: algebra.countably_subadditive_subadditive algebra_Pow
1.946 +	       inf_measure_positive inf_measure_countably_subadditive posf inc)
1.947 +      apply (auto simp add: subsetD [OF s])
1.948 +      done
1.949 +    finally show ?thesis .
1.950 +    qed
1.951 +  ultimately
1.952 +  show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
1.953 +        = Inf (measure_set M f s)"
1.954 +    by (rule order_antisym)
1.955 +qed
1.956 +
1.957 +lemma measure_down:
1.958 +     "measure_space N \<Longrightarrow> sigma_algebra M \<Longrightarrow> sets M \<subseteq> sets N \<Longrightarrow>
1.959 +      (measure M = measure N) \<Longrightarrow> measure_space M"
1.960 +  by (simp add: measure_space_def measure_space_axioms_def positive_def
1.962 +     blast
1.963 +
1.964 +theorem (in algebra) caratheodory:
1.965 +  assumes posf: "positive M f" and ca: "countably_additive M f"
1.966 +  shows "\<exists>MS :: 'a measure_space.
1.967 +             (\<forall>s \<in> sets M. measure MS s = f s) \<and>
1.968 +             ((|space = space MS, sets = sets MS|) = sigma (space M) (sets M)) \<and>
1.969 +             measure_space MS"
1.970 +  proof -
1.971 +    have inc: "increasing M f"
1.973 +    let ?infm = "(\<lambda>x. Inf (measure_set M f x))"
1.974 +    def ls \<equiv> "lambda_system (|space = space M, sets = Pow (space M)|) ?infm"
1.975 +    have mls: "measure_space (|space = space M, sets = ls, measure = ?infm|)"
1.976 +      using sigma_algebra.caratheodory_lemma
1.977 +              [OF sigma_algebra_Pow  inf_measure_outer [OF posf inc]]
1.978 +      by (simp add: ls_def)
1.979 +    hence sls: "sigma_algebra (|space = space M, sets = ls, measure = ?infm|)"
1.980 +      by (simp add: measure_space_def)
1.981 +    have "sets M \<subseteq> ls"
1.982 +      by (simp add: ls_def)
1.983 +         (metis ca posf inc countably_additive_additive algebra_subset_lambda_system)
1.984 +    hence sgs_sb: "sigma_sets (space M) (sets M) \<subseteq> ls"
1.985 +      using sigma_algebra.sigma_sets_subset [OF sls, of "sets M"]
1.986 +      by simp
1.987 +    have "measure_space (|space = space M,
1.988 +                          sets = sigma_sets (space M) (sets M),
1.989 +                          measure = ?infm|)"
1.990 +      by (rule measure_down [OF mls], rule sigma_algebra_sigma_sets)
1.991 +         (simp_all add: sgs_sb space_closed)
1.992 +    thus ?thesis
1.993 +      by (force simp add: sigma_def inf_measure_agrees [OF posf ca])
1.994 +qed
1.995 +
1.996 +end
```