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.95 +lemma subadditiveD:
    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.100 +lemma additiveD:
   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.105 +lemma countably_additiveD:
   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.108 +  by (simp add: countably_additive_def) 
   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.289 +lemma (in algebra) countably_subadditive_subadditive:
   1.290 +  assumes f: "positive M f" and cs: "countably_subadditive M f"
   1.291 +  shows  "subadditive M f"
   1.292 +proof (auto simp add: subadditive_def) 
   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.403 +lemma countably_subadditiveD:
   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.622 +lemma (in algebra) countably_additive_additive:
   1.623 +  assumes posf: "positive M f" and ca: "countably_additive M f" 
   1.624 +  shows "additive M f"
   1.625 +proof (auto simp add: additive_def) 
   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.656 +    by (metis additive_increasing ca countably_additive_additive posf)
   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.961 +                countably_additive_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.972 +      by (metis additive_increasing ca countably_additive_additive posf) 
   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