src/HOL/Probability/Caratheodory.thy
 changeset 38656 d5d342611edb parent 37591 d3daea901123 child 39096 111756225292
```     1.1 --- a/src/HOL/Probability/Caratheodory.thy	Mon Aug 23 17:46:13 2010 +0200
1.2 +++ b/src/HOL/Probability/Caratheodory.thy	Mon Aug 23 19:35:57 2010 +0200
1.3 @@ -1,43 +1,28 @@
1.5
1.6  theory Caratheodory
1.7 -  imports Sigma_Algebra SeriesPlus
1.8 +  imports Sigma_Algebra Positive_Infinite_Real
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_on  where
1.23 -  "disjoint_family_on A S \<longleftrightarrow> (\<forall>m\<in>S. \<forall>n\<in>S. m \<noteq> n \<longrightarrow> A m \<inter> A n = {})"
1.24 -
1.25 -abbreviation
1.26 -  "disjoint_family A \<equiv> disjoint_family_on A UNIV"
1.27 -
1.28 -definition
1.29 -  positive  where
1.30 -  "positive M f \<longleftrightarrow> f {} = (0::real) & (\<forall>x \<in> sets M. 0 \<le> f x)"
1.31 +definition "positive f \<longleftrightarrow> f {} = (0::pinfreal)" -- "Positive is enforced by the type"
1.32
1.33  definition
1.35 -  "additive M f \<longleftrightarrow>
1.36 -    (\<forall>x \<in> sets M. \<forall>y \<in> sets M. x \<inter> y = {}
1.37 +  "additive M f \<longleftrightarrow>
1.38 +    (\<forall>x \<in> sets M. \<forall>y \<in> sets M. x \<inter> y = {}
1.39      \<longrightarrow> f (x \<union> y) = f x + f y)"
1.40
1.41  definition
1.43 -  "countably_additive M f \<longleftrightarrow>
1.44 -    (\<forall>A. range A \<subseteq> sets M \<longrightarrow>
1.45 +  "countably_additive M f \<longleftrightarrow>
1.46 +    (\<forall>A. range A \<subseteq> sets M \<longrightarrow>
1.47           disjoint_family A \<longrightarrow>
1.48 -         (\<Union>i. A i) \<in> sets M \<longrightarrow>
1.49 -         (\<lambda>n. f (A n))  sums  f (\<Union>i. A i))"
1.50 +         (\<Union>i. A i) \<in> sets M \<longrightarrow>
1.51 +         (\<Sum>\<^isub>\<infinity> n. f (A n)) = f (\<Union>i. A i))"
1.52
1.53  definition
1.54    increasing  where
1.55 @@ -45,90 +30,58 @@
1.56
1.57  definition
1.59 -  "subadditive M f \<longleftrightarrow>
1.60 -    (\<forall>x \<in> sets M. \<forall>y \<in> sets M. x \<inter> y = {}
1.61 +  "subadditive M f \<longleftrightarrow>
1.62 +    (\<forall>x \<in> sets M. \<forall>y \<in> sets M. x \<inter> y = {}
1.63      \<longrightarrow> f (x \<union> y) \<le> f x + f y)"
1.64
1.65  definition
1.67 -  "countably_subadditive M f \<longleftrightarrow>
1.68 -    (\<forall>A. range A \<subseteq> sets M \<longrightarrow>
1.69 +  "countably_subadditive M f \<longleftrightarrow>
1.70 +    (\<forall>A. range A \<subseteq> sets M \<longrightarrow>
1.71           disjoint_family A \<longrightarrow>
1.72 -         (\<Union>i. A i) \<in> sets M \<longrightarrow>
1.73 -         summable (f o A) \<longrightarrow>
1.74 -         f (\<Union>i. A i) \<le> suminf (\<lambda>n. f (A n)))"
1.75 +         (\<Union>i. A i) \<in> sets M \<longrightarrow>
1.76 +         f (\<Union>i. A i) \<le> psuminf (\<lambda>n. f (A n)))"
1.77
1.78  definition
1.79    lambda_system where
1.80 -  "lambda_system M f =
1.81 +  "lambda_system M f =
1.82      {l. l \<in> sets M & (\<forall>x \<in> sets M. f (l \<inter> x) + f ((space M - l) \<inter> x) = f x)}"
1.83
1.84  definition
1.85    outer_measure_space where
1.86 -  "outer_measure_space M f  \<longleftrightarrow>
1.87 -     positive M f & increasing M f & countably_subadditive M f"
1.88 +  "outer_measure_space M f  \<longleftrightarrow>
1.89 +     positive f \<and> increasing M f \<and> countably_subadditive M f"
1.90
1.91  definition
1.92    measure_set where
1.93    "measure_set M f X =
1.94 -     {r . \<exists>A. range A \<subseteq> sets M & disjoint_family A & X \<subseteq> (\<Union>i. A i) & (f \<circ> A) sums r}"
1.95 -
1.96 +     {r . \<exists>A. range A \<subseteq> sets M \<and> disjoint_family A \<and> X \<subseteq> (\<Union>i. A i) \<and> (\<Sum>\<^isub>\<infinity> i. f (A i)) = r}"
1.97
1.98  locale measure_space = sigma_algebra +
1.99 -  assumes positive: "!!a. a \<in> sets M \<Longrightarrow> 0 \<le> measure M a"
1.100 -      and empty_measure [simp]: "measure M {} = (0::real)"
1.101 -      and ca: "countably_additive M (measure M)"
1.102 -
1.103 -subsection {* Basic Lemmas *}
1.104 -
1.105 -lemma positive_imp_0: "positive M f \<Longrightarrow> f {} = 0"
1.106 -  by (simp add: positive_def)
1.107 -
1.108 -lemma positive_imp_pos: "positive M f \<Longrightarrow> x \<in> sets M \<Longrightarrow> 0 \<le> f x"
1.109 -  by (simp add: positive_def)
1.110 +  fixes \<mu> :: "'a set \<Rightarrow> pinfreal"
1.111 +  assumes empty_measure [simp]: "\<mu> {} = 0"
1.112 +      and ca: "countably_additive M \<mu>"
1.113
1.114  lemma increasingD:
1.115       "increasing M f \<Longrightarrow> x \<subseteq> y \<Longrightarrow> x\<in>sets M \<Longrightarrow> y\<in>sets M \<Longrightarrow> f x \<le> f y"
1.116    by (auto simp add: increasing_def)
1.117
1.119 -     "subadditive M f \<Longrightarrow> x \<inter> y = {} \<Longrightarrow> x\<in>sets M \<Longrightarrow> y\<in>sets M
1.120 +     "subadditive M f \<Longrightarrow> x \<inter> y = {} \<Longrightarrow> x\<in>sets M \<Longrightarrow> y\<in>sets M
1.121        \<Longrightarrow> f (x \<union> y) \<le> f x + f y"
1.123
1.125 -     "additive M f \<Longrightarrow> x \<inter> y = {} \<Longrightarrow> x\<in>sets M \<Longrightarrow> y\<in>sets M
1.126 +     "additive M f \<Longrightarrow> x \<inter> y = {} \<Longrightarrow> x\<in>sets M \<Longrightarrow> y\<in>sets M
1.127        \<Longrightarrow> f (x \<union> y) = f x + f y"
1.129
1.131    "countably_additive M f \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A
1.132 -   \<Longrightarrow> (\<Union>i. A i) \<in> sets M \<Longrightarrow> (\<lambda>n. f (A n))  sums  f (\<Union>i. A i)"
1.133 +   \<Longrightarrow> (\<Union>i. A i) \<in> sets M \<Longrightarrow> (\<Sum>\<^isub>\<infinity> n. f (A n)) = f (\<Union>i. A i)"
1.135
1.136 -lemma Int_Diff_disjoint: "A \<inter> B \<inter> (A - B) = {}"
1.137 -  by blast
1.138 -
1.139 -lemma Int_Diff_Un: "A \<inter> B \<union> (A - B) = A"
1.140 -  by blast
1.141 -
1.142 -lemma disjoint_family_subset:
1.143 -     "disjoint_family A \<Longrightarrow> (!!x. B x \<subseteq> A x) \<Longrightarrow> disjoint_family B"
1.144 -  by (force simp add: disjoint_family_on_def)
1.145 -
1.146 -subsection {* A Two-Element Series *}
1.147 -
1.148 -definition binaryset :: "'a set \<Rightarrow> 'a set \<Rightarrow> nat \<Rightarrow> 'a set "
1.149 -  where "binaryset A B = (\<lambda>\<^isup>x. {})(0 := A, Suc 0 := B)"
1.150 -
1.151 -lemma range_binaryset_eq: "range(binaryset A B) = {A,B,{}}"
1.152 -  apply (simp add: binaryset_def)
1.153 -  apply (rule set_ext)
1.154 -  apply (auto simp add: image_iff)
1.155 -  done
1.156 -
1.157 -lemma UN_binaryset_eq: "(\<Union>i. binaryset A B i) = A \<union> B"
1.158 -  by (simp add: UNION_eq_Union_image range_binaryset_eq)
1.159 +section "Extend binary sets"
1.160
1.161  lemma LIMSEQ_binaryset:
1.162    assumes f: "f {} = 0"
1.163 @@ -153,17 +106,31 @@
1.164  lemma binaryset_sums:
1.165    assumes f: "f {} = 0"
1.166    shows  "(\<lambda>n. f (binaryset A B n)) sums (f A + f B)"
1.167 -    by (simp add: sums_def LIMSEQ_binaryset [where f=f, OF f])
1.168 +    by (simp add: sums_def LIMSEQ_binaryset [where f=f, OF f])
1.169
1.170  lemma suminf_binaryset_eq:
1.171       "f {} = 0 \<Longrightarrow> suminf (\<lambda>n. f (binaryset A B n)) = f A + f B"
1.172    by (metis binaryset_sums sums_unique)
1.173
1.174 +lemma binaryset_psuminf:
1.175 +  assumes "f {} = 0"
1.176 +  shows "(\<Sum>\<^isub>\<infinity> n. f (binaryset A B n)) = f A + f B" (is "?suminf = ?sum")
1.177 +proof -
1.178 +  have *: "{..<2} = {0, 1::nat}" by auto
1.179 +  have "\<forall>n\<ge>2. f (binaryset A B n) = 0"
1.180 +    unfolding binaryset_def
1.181 +    using assms by auto
1.182 +  hence "?suminf = (\<Sum>N<2. f (binaryset A B N))"
1.183 +    by (rule psuminf_finite)
1.184 +  also have "... = ?sum" unfolding * binaryset_def
1.185 +    by simp
1.186 +  finally show ?thesis .
1.187 +qed
1.188
1.189  subsection {* Lambda Systems *}
1.190
1.191  lemma (in algebra) lambda_system_eq:
1.192 -    "lambda_system M f =
1.193 +    "lambda_system M f =
1.194          {l. l \<in> sets M & (\<forall>x \<in> sets M. f (x \<inter> l) + f (x - l) = f x)}"
1.195  proof -
1.196    have [simp]: "!!l x. l \<in> sets M \<Longrightarrow> x \<in> sets M \<Longrightarrow> (space M - l) \<inter> x = x - l"
1.197 @@ -173,28 +140,28 @@
1.198  qed
1.199
1.200  lemma (in algebra) lambda_system_empty:
1.201 -    "positive M f \<Longrightarrow> {} \<in> lambda_system M f"
1.202 -  by (auto simp add: positive_def lambda_system_eq)
1.203 +  "positive f \<Longrightarrow> {} \<in> lambda_system M f"
1.204 +  by (auto simp add: positive_def lambda_system_eq)
1.205
1.206  lemma lambda_system_sets:
1.207      "x \<in> lambda_system M f \<Longrightarrow> x \<in> sets M"
1.209
1.210  lemma (in algebra) lambda_system_Compl:
1.211 -  fixes f:: "'a set \<Rightarrow> real"
1.212 +  fixes f:: "'a set \<Rightarrow> pinfreal"
1.213    assumes x: "x \<in> lambda_system M f"
1.214    shows "space M - x \<in> lambda_system M f"
1.215    proof -
1.216      have "x \<subseteq> space M"
1.217        by (metis sets_into_space lambda_system_sets x)
1.218      hence "space M - (space M - x) = x"
1.219 -      by (metis double_diff equalityE)
1.220 +      by (metis double_diff equalityE)
1.221      with x show ?thesis
1.222 -      by (force simp add: lambda_system_def)
1.223 +      by (force simp add: lambda_system_def ac_simps)
1.224    qed
1.225
1.226  lemma (in algebra) lambda_system_Int:
1.227 -  fixes f:: "'a set \<Rightarrow> real"
1.228 +  fixes f:: "'a set \<Rightarrow> pinfreal"
1.229    assumes xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f"
1.230    shows "x \<inter> y \<in> lambda_system M f"
1.231    proof -
1.232 @@ -213,42 +180,42 @@
1.233          ultimately
1.234          have ey: "f (u - x \<inter> y) = f (u \<inter> y - x) + f (u - y)" using fy
1.235            by force
1.236 -        have "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y)
1.237 +        have "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y)
1.238                = (f (u \<inter> (x \<inter> y)) + f (u \<inter> y - x)) + f (u - y)"
1.239 -          by (simp add: ey)
1.240 +          by (simp add: ey ac_simps)
1.241          also have "... =  (f ((u \<inter> y) \<inter> x) + f (u \<inter> y - x)) + f (u - y)"
1.242 -          by (simp add: Int_ac)
1.243 +          by (simp add: Int_ac)
1.244          also have "... = f (u \<inter> y) + f (u - y)"
1.245            using fx [THEN bspec, of "u \<inter> y"] Int y u
1.246            by force
1.247          also have "... = f u"
1.248 -          by (metis fy u)
1.249 +          by (metis fy u)
1.250          finally show "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y) = f u" .
1.251        qed
1.252    qed
1.253
1.254
1.255  lemma (in algebra) lambda_system_Un:
1.256 -  fixes f:: "'a set \<Rightarrow> real"
1.257 +  fixes f:: "'a set \<Rightarrow> pinfreal"
1.258    assumes xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f"
1.259    shows "x \<union> y \<in> lambda_system M f"
1.260  proof -
1.261    have "(space M - x) \<inter> (space M - y) \<in> sets M"
1.262 -    by (metis Diff_Un Un compl_sets lambda_system_sets xl yl)
1.263 +    by (metis Diff_Un Un compl_sets lambda_system_sets xl yl)
1.264    moreover
1.265    have "x \<union> y = space M - ((space M - x) \<inter> (space M - y))"
1.266      by auto  (metis subsetD lambda_system_sets sets_into_space xl yl)+
1.267    ultimately show ?thesis
1.268 -    by (metis lambda_system_Compl lambda_system_Int xl yl)
1.269 +    by (metis lambda_system_Compl lambda_system_Int xl yl)
1.270  qed
1.271
1.272  lemma (in algebra) lambda_system_algebra:
1.273 -    "positive M f \<Longrightarrow> algebra (M (|sets := lambda_system M f|))"
1.274 -  apply (auto simp add: algebra_def)
1.275 +  "positive f \<Longrightarrow> algebra (M (|sets := lambda_system M f|))"
1.276 +  apply (auto simp add: algebra_def)
1.277    apply (metis lambda_system_sets set_mp sets_into_space)
1.278    apply (metis lambda_system_empty)
1.279    apply (metis lambda_system_Compl)
1.280 -  apply (metis lambda_system_Un)
1.281 +  apply (metis lambda_system_Un)
1.282    done
1.283
1.285 @@ -259,19 +226,13 @@
1.286      have "z \<inter> x = (z \<inter> (x \<union> y)) \<inter> x" using disj by blast
1.287      moreover
1.288      have "z \<inter> y = (z \<inter> (x \<union> y)) - x" using disj by blast
1.289 -    moreover
1.290 +    moreover
1.291      have "(z \<inter> (x \<union> y)) \<in> sets M"
1.292 -      by (metis Int Un lambda_system_sets xl yl z)
1.293 +      by (metis Int Un lambda_system_sets xl yl z)
1.294      ultimately show ?thesis using xl yl
1.296    qed
1.297
1.298 -lemma (in algebra) Int_space_eq1 [simp]: "x \<in> sets M \<Longrightarrow> space M \<inter> x = x"
1.299 -  by (metis Int_absorb1 sets_into_space)
1.300 -
1.301 -lemma (in algebra) Int_space_eq2 [simp]: "x \<in> sets M \<Longrightarrow> x \<inter> space M = x"
1.302 -  by (metis Int_absorb2 sets_into_space)
1.303 -
1.305       "additive (M (|sets := lambda_system M f|)) f"
1.307 @@ -279,14 +240,14 @@
1.308      assume disj: "x \<inter> y = {}"
1.309         and xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f"
1.310      hence  "x \<in> sets M" "y \<in> sets M" by (blast intro: lambda_system_sets)+
1.311 -    thus "f (x \<union> y) = f x + f y"
1.312 +    thus "f (x \<union> y) = f x + f y"
1.313        using lambda_system_strong_additive [OF top disj xl yl]
1.315    qed
1.316
1.317
1.319 -  assumes f: "positive M f" and cs: "countably_subadditive M f"
1.320 +  assumes f: "positive f" and cs: "countably_subadditive M f"
1.323    fix x y
1.324 @@ -295,159 +256,80 @@
1.325      by (auto simp add: disjoint_family_on_def binaryset_def)
1.326    hence "range (binaryset x y) \<subseteq> sets M \<longrightarrow>
1.327           (\<Union>i. binaryset x y i) \<in> sets M \<longrightarrow>
1.328 -         summable (f o (binaryset x y)) \<longrightarrow>
1.329 -         f (\<Union>i. binaryset x y i) \<le> suminf (\<lambda>n. f (binaryset x y n))"
1.330 +         f (\<Union>i. binaryset x y i) \<le> (\<Sum>\<^isub>\<infinity> n. f (binaryset x y n))"
1.332    hence "{x,y,{}} \<subseteq> sets M \<longrightarrow> x \<union> y \<in> sets M \<longrightarrow>
1.333 -         summable (f o (binaryset x y)) \<longrightarrow>
1.334 -         f (x \<union> y) \<le> suminf (\<lambda>n. f (binaryset x y n))"
1.335 +         f (x \<union> y) \<le> (\<Sum>\<^isub>\<infinity> n. f (binaryset x y n))"
1.336      by (simp add: range_binaryset_eq UN_binaryset_eq)
1.337 -  thus "f (x \<union> y) \<le>  f x + f y" using f x y binaryset_sums
1.338 -    by (auto simp add: Un sums_iff positive_def o_def)
1.339 -qed
1.340 -
1.341 -
1.342 -definition disjointed :: "(nat \<Rightarrow> 'a set) \<Rightarrow> nat \<Rightarrow> 'a set "
1.343 -  where "disjointed A n = A n - (\<Union>i\<in>{0..<n}. A i)"
1.344 -
1.345 -lemma finite_UN_disjointed_eq: "(\<Union>i\<in>{0..<n}. disjointed A i) = (\<Union>i\<in>{0..<n}. A i)"
1.346 -proof (induct n)
1.347 -  case 0 show ?case by simp
1.348 -next
1.349 -  case (Suc n)
1.350 -  thus ?case by (simp add: atLeastLessThanSuc disjointed_def)
1.351 +  thus "f (x \<union> y) \<le>  f x + f y" using f x y
1.352 +    by (auto simp add: Un o_def binaryset_psuminf positive_def)
1.353  qed
1.354
1.355 -lemma UN_disjointed_eq: "(\<Union>i. disjointed A i) = (\<Union>i. A i)"
1.356 -  apply (rule UN_finite2_eq [where k=0])
1.357 -  apply (simp add: finite_UN_disjointed_eq)
1.358 -  done
1.359 -
1.360 -lemma less_disjoint_disjointed: "m<n \<Longrightarrow> disjointed A m \<inter> disjointed A n = {}"
1.361 -  by (auto simp add: disjointed_def)
1.362 -
1.363 -lemma disjoint_family_disjointed: "disjoint_family (disjointed A)"
1.364 -  by (simp add: disjoint_family_on_def)
1.365 -     (metis neq_iff Int_commute less_disjoint_disjointed)
1.366 -
1.367 -lemma disjointed_subset: "disjointed A n \<subseteq> A n"
1.368 -  by (auto simp add: disjointed_def)
1.369 -
1.370 -
1.371 -lemma (in algebra) UNION_in_sets:
1.372 -  fixes A:: "nat \<Rightarrow> 'a set"
1.373 -  assumes A: "range A \<subseteq> sets M "
1.374 -  shows  "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
1.375 -proof (induct n)
1.376 -  case 0 show ?case by simp
1.377 -next
1.378 -  case (Suc n)
1.379 -  thus ?case
1.380 -    by (simp add: atLeastLessThanSuc) (metis A Un UNIV_I image_subset_iff)
1.381 -qed
1.382 -
1.383 -lemma (in algebra) range_disjointed_sets:
1.384 -  assumes A: "range A \<subseteq> sets M "
1.385 -  shows  "range (disjointed A) \<subseteq> sets M"
1.386 -proof (auto simp add: disjointed_def)
1.387 -  fix n
1.388 -  show "A n - (\<Union>i\<in>{0..<n}. A i) \<in> sets M" using UNION_in_sets
1.389 -    by (metis A Diff UNIV_I image_subset_iff)
1.390 -qed
1.391 -
1.392 -lemma sigma_algebra_disjoint_iff:
1.393 -     "sigma_algebra M \<longleftrightarrow>
1.394 -      algebra M &
1.395 -      (\<forall>A. range A \<subseteq> sets M \<longrightarrow> disjoint_family A \<longrightarrow>
1.396 -           (\<Union>i::nat. A i) \<in> sets M)"
1.397 -proof (auto simp add: sigma_algebra_iff)
1.398 -  fix A :: "nat \<Rightarrow> 'a set"
1.399 -  assume M: "algebra M"
1.400 -     and A: "range A \<subseteq> sets M"
1.401 -     and UnA: "\<forall>A. range A \<subseteq> sets M \<longrightarrow>
1.402 -               disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
1.403 -  hence "range (disjointed A) \<subseteq> sets M \<longrightarrow>
1.404 -         disjoint_family (disjointed A) \<longrightarrow>
1.405 -         (\<Union>i. disjointed A i) \<in> sets M" by blast
1.406 -  hence "(\<Union>i. disjointed A i) \<in> sets M"
1.407 -    by (simp add: algebra.range_disjointed_sets M A disjoint_family_disjointed)
1.408 -  thus "(\<Union>i::nat. A i) \<in> sets M" by (simp add: UN_disjointed_eq)
1.409 -qed
1.410 -
1.411 -
1.413    fixes A:: "nat \<Rightarrow> 'a set"
1.414 -  assumes f: "positive M f" and ad: "additive M f"
1.416        and A: "range A \<subseteq> sets M"
1.417        and disj: "disjoint_family A"
1.418 -  shows  "setsum (f o A) {0..<n} = f (\<Union>i\<in>{0..<n}. A i)"
1.419 +  shows  "setsum (f \<circ> A) {0..<n} = f (\<Union>i\<in>{0..<n}. A i)"
1.420  proof (induct n)
1.421 -  case 0 show ?case using f by (simp add: positive_def)
1.422 +  case 0 show ?case using f by (simp add: positive_def)
1.423  next
1.424 -  case (Suc n)
1.425 -  have "A n \<inter> (\<Union>i\<in>{0..<n}. A i) = {}" using disj
1.426 +  case (Suc n)
1.427 +  have "A n \<inter> (\<Union>i\<in>{0..<n}. A i) = {}" using disj
1.428      by (auto simp add: disjoint_family_on_def neq_iff) blast
1.429 -  moreover
1.430 -  have "A n \<in> sets M" using A by blast
1.431 +  moreover
1.432 +  have "A n \<in> sets M" using A by blast
1.433    moreover have "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
1.434      by (metis A UNION_in_sets atLeast0LessThan)
1.435 -  moreover
1.436 +  moreover
1.437    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.440    with Suc.hyps show ?case using ad
1.443  qed
1.444
1.445
1.447    "countably_subadditive M f \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A \<Longrightarrow>
1.448 -   (\<Union>i. A i) \<in> sets M \<Longrightarrow> summable (f o A) \<Longrightarrow> f (\<Union>i. A i) \<le> suminf (f o A)"
1.449 +   (\<Union>i. A i) \<in> sets M \<Longrightarrow> f (\<Union>i. A i) \<le> psuminf (f o A)"
1.451
1.453 -  fixes A:: "nat \<Rightarrow> 'a set"
1.454 -  assumes f: "positive M f" and ad: "additive M f"
1.456 +  fixes A:: "nat \<Rightarrow> 'a set" and  f :: "'a set \<Rightarrow> pinfreal"
1.458        and inc: "increasing M f"
1.459        and A: "range A \<subseteq> sets M"
1.460        and disj: "disjoint_family A"
1.461 -  shows  "summable (f o A)"
1.462 -proof (rule pos_summable)
1.463 -  fix n
1.464 -  show "0 \<le> (f \<circ> A) n" using f A
1.465 -    by (force simp add: positive_def)
1.466 -  next
1.467 -  fix n
1.468 -  have "setsum (f \<circ> A) {0..<n} = f (\<Union>i\<in>{0..<n}. A i)"
1.470 +  shows  "psuminf (f \<circ> A) \<le> f (space M)"
1.471 +proof (safe intro!: psuminf_bound)
1.472 +  fix N
1.473 +  have "setsum (f \<circ> A) {0..<N} = f (\<Union>i\<in>{0..<N}. A i)"
1.475    also have "... \<le> f (space M)" using space_closed A
1.476 -    by (blast intro: increasingD [OF inc] UNION_in_sets top)
1.477 -  finally show "setsum (f \<circ> A) {0..<n} \<le> f (space M)" .
1.478 +    by (blast intro: increasingD [OF inc] UNION_in_sets top)
1.479 +  finally show "setsum (f \<circ> A) {..<N} \<le> f (space M)" by (simp add: atLeast0LessThan)
1.480  qed
1.481
1.482 -lemma lambda_system_positive:
1.483 -     "positive M f \<Longrightarrow> positive (M (|sets := lambda_system M f|)) f"
1.484 -  by (simp add: positive_def lambda_system_def)
1.485 -
1.486  lemma lambda_system_increasing:
1.487     "increasing M f \<Longrightarrow> increasing (M (|sets := lambda_system M f|)) f"
1.488 -  by (simp add: increasing_def lambda_system_def)
1.489 +  by (simp add: increasing_def lambda_system_def)
1.490
1.491  lemma (in algebra) lambda_system_strong_sum:
1.492 -  fixes A:: "nat \<Rightarrow> 'a set"
1.493 -  assumes f: "positive M f" and a: "a \<in> sets M"
1.494 +  fixes A:: "nat \<Rightarrow> 'a set" and f :: "'a set \<Rightarrow> pinfreal"
1.495 +  assumes f: "positive f" and a: "a \<in> sets M"
1.496        and A: "range A \<subseteq> lambda_system M f"
1.497        and disj: "disjoint_family A"
1.498    shows  "(\<Sum>i = 0..<n. f (a \<inter>A i)) = f (a \<inter> (\<Union>i\<in>{0..<n}. A i))"
1.499  proof (induct n)
1.500 -  case 0 show ?case using f by (simp add: positive_def)
1.501 +  case 0 show ?case using f by (simp add: positive_def)
1.502  next
1.503 -  case (Suc n)
1.504 +  case (Suc n)
1.505    have 2: "A n \<inter> UNION {0..<n} A = {}" using disj
1.506 -    by (force simp add: disjoint_family_on_def neq_iff)
1.507 +    by (force simp add: disjoint_family_on_def neq_iff)
1.508    have 3: "A n \<in> lambda_system M f" using A
1.509      by blast
1.510    have 4: "UNION {0..<n} A \<in> lambda_system M f"
1.511 -    using A algebra.UNION_in_sets [OF local.lambda_system_algebra [OF f]]
1.512 +    using A algebra.UNION_in_sets [OF local.lambda_system_algebra, of f, OF f]
1.513      by simp
1.514    from Suc.hyps show ?case
1.516 @@ -458,89 +340,77 @@
1.517    assumes oms: "outer_measure_space M f"
1.518        and A: "range A \<subseteq> lambda_system M f"
1.519        and disj: "disjoint_family A"
1.520 -  shows  "(\<Union>i. A i) \<in> lambda_system M f & (f \<circ> A)  sums  f (\<Union>i. A i)"
1.521 +  shows  "(\<Union>i. A i) \<in> lambda_system M f \<and> psuminf (f \<circ> A) = f (\<Union>i. A i)"
1.522  proof -
1.523 -  have pos: "positive M f" and inc: "increasing M f"
1.524 -   and csa: "countably_subadditive M f"
1.525 +  have pos: "positive f" and inc: "increasing M f"
1.526 +   and csa: "countably_subadditive M f"
1.527      by (metis oms outer_measure_space_def)+
1.528    have sa: "subadditive M f"
1.530 -  have A': "range A \<subseteq> sets (M(|sets := lambda_system M f|))" using A
1.532 +  have A': "range A \<subseteq> sets (M(|sets := lambda_system M f|))" using A
1.533      by simp
1.534    have alg_ls: "algebra (M(|sets := lambda_system M f|))"
1.535 -    by (rule lambda_system_algebra [OF pos])
1.536 +    by (rule lambda_system_algebra) (rule pos)
1.537    have A'': "range A \<subseteq> sets M"
1.538       by (metis A image_subset_iff lambda_system_sets)
1.539 -  have sumfA: "summable (f \<circ> A)"
1.540 -    by (metis algebra.increasing_additive_summable [OF alg_ls]
1.542 -          A' oms outer_measure_space_def disj)
1.543 +
1.544    have U_in: "(\<Union>i. A i) \<in> sets M"
1.545      by (metis A'' countable_UN)
1.546 -  have U_eq: "f (\<Union>i. A i) = suminf (f o A)"
1.547 +  have U_eq: "f (\<Union>i. A i) = psuminf (f o A)"
1.548      proof (rule antisym)
1.549 -      show "f (\<Union>i. A i) \<le> suminf (f \<circ> A)"
1.550 -        by (rule countably_subadditiveD [OF csa A'' disj U_in sumfA])
1.551 -      show "suminf (f \<circ> A) \<le> f (\<Union>i. A i)"
1.552 -        by (rule suminf_le [OF sumfA])
1.553 +      show "f (\<Union>i. A i) \<le> psuminf (f \<circ> A)"
1.554 +        by (rule countably_subadditiveD [OF csa A'' disj U_in])
1.555 +      show "psuminf (f \<circ> A) \<le> f (\<Union>i. A i)"
1.556 +        by (rule psuminf_bound, unfold atLeast0LessThan[symmetric])
1.557             (metis algebra.additive_sum [OF alg_ls] pos disj UN_Un Un_UNIV_right
1.559 -                  subset_Un_eq increasingD [OF inc] A' A'' UNION_in_sets U_in)
1.560 +                  lambda_system_additive subset_Un_eq increasingD [OF inc]
1.561 +                  A' A'' UNION_in_sets U_in)
1.562      qed
1.563    {
1.564 -    fix a
1.565 -    assume a [iff]: "a \<in> sets M"
1.566 +    fix a
1.567 +    assume a [iff]: "a \<in> sets M"
1.568      have "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) = f a"
1.569      proof -
1.570 -      have summ: "summable (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)" using pos A''
1.571 -        apply -
1.572 -        apply (rule summable_comparison_test [OF _ sumfA])
1.573 -        apply (rule_tac x="0" in exI)
1.574 -        apply (simp add: positive_def)
1.575 -        apply (auto simp add: )
1.576 -        apply (subst abs_of_nonneg)
1.577 -        apply (metis A'' Int UNIV_I a image_subset_iff)
1.578 -        apply (blast intro:  increasingD [OF inc])
1.579 -        done
1.580        show ?thesis
1.581        proof (rule antisym)
1.582          have "range (\<lambda>i. a \<inter> A i) \<subseteq> sets M" using A''
1.583            by blast
1.584 -        moreover
1.585 +        moreover
1.586          have "disjoint_family (\<lambda>i. a \<inter> A i)" using disj
1.587 -          by (auto simp add: disjoint_family_on_def)
1.588 -        moreover
1.589 +          by (auto simp add: disjoint_family_on_def)
1.590 +        moreover
1.591          have "a \<inter> (\<Union>i. A i) \<in> sets M"
1.592            by (metis Int U_in a)
1.593 -        ultimately
1.594 -        have "f (a \<inter> (\<Union>i. A i)) \<le> suminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)"
1.595 -          using countably_subadditiveD [OF csa, of "(\<lambda>i. a \<inter> A i)"] summ
1.596 -          by (simp add: o_def)
1.597 -        moreover
1.598 -        have "suminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)  \<le> f a - f (a - (\<Union>i. A i))"
1.599 -          proof (rule suminf_le [OF summ])
1.600 +        ultimately
1.601 +        have "f (a \<inter> (\<Union>i. A i)) \<le> psuminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)"
1.602 +          using countably_subadditiveD [OF csa, of "(\<lambda>i. a \<inter> A i)"]
1.603 +          by (simp add: o_def)
1.604 +        hence "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le>
1.605 +            psuminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) + f (a - (\<Union>i. A i))"
1.607 +        moreover
1.608 +        have "psuminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) + f (a - (\<Union>i. A i)) \<le> f a"
1.609 +          proof (safe intro!: psuminf_bound_add)
1.610              fix n
1.611              have UNION_in: "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
1.612 -              by (metis A'' UNION_in_sets)
1.613 +              by (metis A'' UNION_in_sets)
1.614              have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A''
1.615                by (blast intro: increasingD [OF inc] A'' UNION_in_sets)
1.616              have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system M f"
1.617 -              using algebra.UNION_in_sets [OF lambda_system_algebra [OF pos]]
1.618 -              by (simp add: A)
1.619 -            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.620 +              using algebra.UNION_in_sets [OF lambda_system_algebra [of f, OF pos]]
1.621 +              by (simp add: A)
1.622 +            hence eq_fa: "f a = f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i))"
1.623                by (simp add: lambda_system_eq UNION_in)
1.624              have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))"
1.625 -              by (blast intro: increasingD [OF inc] UNION_eq_Union_image
1.626 +              by (blast intro: increasingD [OF inc] UNION_eq_Union_image
1.627                                 UNION_in U_in)
1.628 -            thus "setsum (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) {0..<n} \<le> f a - f (a - (\<Union>i. A i))"
1.629 -              using eq_fa
1.630 -              by (simp add: suminf_le [OF summ] lambda_system_strong_sum pos
1.631 -                            a A disj)
1.632 +            thus "setsum (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) {..<n} + f (a - (\<Union>i. A i)) \<le> f a"
1.633 +              by (simp add: lambda_system_strong_sum pos A disj eq_fa add_left_mono atLeast0LessThan[symmetric])
1.634            qed
1.635 -        ultimately show "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le> f a"
1.636 -          by arith
1.637 +        ultimately show "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le> f a"
1.638 +          by (rule order_trans)
1.639        next
1.640 -        have "f a \<le> f (a \<inter> (\<Union>i. A i) \<union> (a - (\<Union>i. A i)))"
1.641 +        have "f a \<le> f (a \<inter> (\<Union>i. A i) \<union> (a - (\<Union>i. A i)))"
1.642            by (blast intro:  increasingD [OF inc] U_in)
1.643          also have "... \<le>  f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))"
1.644            by (blast intro: subadditiveD [OF sa] U_in)
1.645 @@ -549,68 +419,54 @@
1.646       qed
1.647    }
1.648    thus  ?thesis
1.649 -    by (simp add: lambda_system_eq sums_iff U_eq U_in sumfA)
1.650 +    by (simp add: lambda_system_eq sums_iff U_eq U_in)
1.651  qed
1.652
1.653  lemma (in sigma_algebra) caratheodory_lemma:
1.654    assumes oms: "outer_measure_space M f"
1.655 -  shows "measure_space (|space = space M, sets = lambda_system M f, measure = f|)"
1.656 +  shows "measure_space (|space = space M, sets = lambda_system M f|) f"
1.657  proof -
1.658 -  have pos: "positive M f"
1.659 +  have pos: "positive f"
1.660      by (metis oms outer_measure_space_def)
1.661 -  have alg: "algebra (|space = space M, sets = lambda_system M f, measure = f|)"
1.662 -    using lambda_system_algebra [OF pos]
1.663 -    by (simp add: algebra_def)
1.664 -  then moreover
1.665 -  have "sigma_algebra (|space = space M, sets = lambda_system M f, measure = f|)"
1.666 +  have alg: "algebra (|space = space M, sets = lambda_system M f|)"
1.667 +    using lambda_system_algebra [of f, OF pos]
1.668 +    by (simp add: algebra_def)
1.669 +  then moreover
1.670 +  have "sigma_algebra (|space = space M, sets = lambda_system M f|)"
1.671      using lambda_system_caratheodory [OF oms]
1.672 -    by (simp add: sigma_algebra_disjoint_iff)
1.673 -  moreover
1.674 -  have "measure_space_axioms (|space = space M, sets = lambda_system M f, measure = f|)"
1.675 +    by (simp add: sigma_algebra_disjoint_iff)
1.676 +  moreover
1.677 +  have "measure_space_axioms (|space = space M, sets = lambda_system M f|) f"
1.678      using pos lambda_system_caratheodory [OF oms]
1.679 -    by (simp add: measure_space_axioms_def positive_def lambda_system_sets
1.681 -  ultimately
1.682 +    by (simp add: measure_space_axioms_def positive_def lambda_system_sets
1.684 +  ultimately
1.685    show ?thesis
1.686 -    by intro_locales (auto simp add: sigma_algebra_def)
1.687 +    by intro_locales (auto simp add: sigma_algebra_def)
1.688  qed
1.689
1.690
1.691  lemma (in algebra) inf_measure_nonempty:
1.692 -  assumes f: "positive M f" and b: "b \<in> sets M" and a: "a \<subseteq> b"
1.693 +  assumes f: "positive f" and b: "b \<in> sets M" and a: "a \<subseteq> b"
1.694    shows "f b \<in> measure_set M f a"
1.695  proof -
1.696 -  have "(f \<circ> (\<lambda>i. {})(0 := b)) sums setsum (f \<circ> (\<lambda>i. {})(0 := b)) {0..<1::nat}"
1.697 -    by (rule series_zero)  (simp add: positive_imp_0 [OF f])
1.698 -  also have "... = f b"
1.699 +  have "psuminf (f \<circ> (\<lambda>i. {})(0 := b)) = setsum (f \<circ> (\<lambda>i. {})(0 := b)) {..<1::nat}"
1.700 +    by (rule psuminf_finite) (simp add: f[unfolded positive_def])
1.701 +  also have "... = f b"
1.702      by simp
1.703 -  finally have "(f \<circ> (\<lambda>i. {})(0 := b)) sums f b" .
1.704 -  thus ?thesis using a
1.705 -    by (auto intro!: exI [of _ "(\<lambda>i. {})(0 := b)"]
1.706 -             simp add: measure_set_def disjoint_family_on_def b split_if_mem2)
1.707 -qed
1.708 -
1.709 -lemma (in algebra) inf_measure_pos0:
1.710 -     "positive M f \<Longrightarrow> x \<in> measure_set M f a \<Longrightarrow> 0 \<le> x"
1.711 -apply (auto simp add: positive_def measure_set_def sums_iff intro!: suminf_ge_zero)
1.712 -apply blast
1.713 -done
1.714 -
1.715 -lemma (in algebra) inf_measure_pos:
1.716 -  shows "positive M f \<Longrightarrow> x \<subseteq> space M \<Longrightarrow> 0 \<le> Inf (measure_set M f x)"
1.717 -apply (rule Inf_greatest)
1.718 -apply (metis emptyE inf_measure_nonempty top)
1.719 -apply (metis inf_measure_pos0)
1.720 -done
1.721 +  finally have "psuminf (f \<circ> (\<lambda>i. {})(0 := b)) = f b" .
1.722 +  thus ?thesis using a b
1.723 +    by (auto intro!: exI [of _ "(\<lambda>i. {})(0 := b)"]
1.724 +             simp: measure_set_def disjoint_family_on_def split_if_mem2 comp_def)
1.725 +qed
1.726
1.728 -  assumes posf: "positive M f" and addf: "additive M f"
1.730    shows "increasing M f"
1.731 -proof (auto simp add: increasing_def)
1.732 +proof (auto simp add: increasing_def)
1.733    fix x y
1.734    assume xy: "x \<in> sets M" "y \<in> sets M" "x \<subseteq> y"
1.735 -  have "f x \<le> f x + f (y-x)" using posf
1.736 -    by (simp add: positive_def) (metis Diff xy(1,2))
1.737 +  have "f x \<le> f x + f (y-x)" ..
1.738    also have "... = f (x \<union> (y-x))" using addf
1.740    also have "... = f y"
1.741 @@ -619,42 +475,42 @@
1.742  qed
1.743
1.745 -  assumes posf: "positive M f" and ca: "countably_additive M f"
1.746 +  assumes posf: "positive f" and ca: "countably_additive M f"
1.750    fix x y
1.751    assume x: "x \<in> sets M" and y: "y \<in> sets M" and "x \<inter> y = {}"
1.752    hence "disjoint_family (binaryset x y)"
1.753 -    by (auto simp add: disjoint_family_on_def binaryset_def)
1.754 -  hence "range (binaryset x y) \<subseteq> sets M \<longrightarrow>
1.755 -         (\<Union>i. binaryset x y i) \<in> sets M \<longrightarrow>
1.756 -         f (\<Union>i. binaryset x y i) = suminf (\<lambda>n. f (binaryset x y n))"
1.757 +    by (auto simp add: disjoint_family_on_def binaryset_def)
1.758 +  hence "range (binaryset x y) \<subseteq> sets M \<longrightarrow>
1.759 +         (\<Union>i. binaryset x y i) \<in> sets M \<longrightarrow>
1.760 +         f (\<Union>i. binaryset x y i) = (\<Sum>\<^isub>\<infinity> n. f (binaryset x y n))"
1.761      using ca
1.763 -  hence "{x,y,{}} \<subseteq> sets M \<longrightarrow> x \<union> y \<in> sets M \<longrightarrow>
1.764 -         f (x \<union> y) = suminf (\<lambda>n. f (binaryset x y n))"
1.766 +  hence "{x,y,{}} \<subseteq> sets M \<longrightarrow> x \<union> y \<in> sets M \<longrightarrow>
1.767 +         f (x \<union> y) = (\<Sum>\<^isub>\<infinity> n. f (binaryset x y n))"
1.768      by (simp add: range_binaryset_eq UN_binaryset_eq)
1.769    thus "f (x \<union> y) = f x + f y" using posf x y
1.770 -    by (simp add: Un suminf_binaryset_eq positive_def)
1.771 -qed
1.772 -
1.773 +    by (auto simp add: Un binaryset_psuminf positive_def)
1.774 +qed
1.775 +
1.776  lemma (in algebra) inf_measure_agrees:
1.777 -  assumes posf: "positive M f" and ca: "countably_additive M f"
1.778 -      and s: "s \<in> sets M"
1.779 +  assumes posf: "positive f" and ca: "countably_additive M f"
1.780 +      and s: "s \<in> sets M"
1.781    shows "Inf (measure_set M f s) = f s"
1.782 -proof (rule Inf_eq)
1.783 +  unfolding Inf_pinfreal_def
1.784 +proof (safe intro!: Greatest_equality)
1.785    fix z
1.786    assume z: "z \<in> measure_set M f s"
1.787 -  from this obtain A where
1.788 +  from this obtain A where
1.789      A: "range A \<subseteq> sets M" and disj: "disjoint_family A"
1.790 -    and "s \<subseteq> (\<Union>x. A x)" and sm: "summable (f \<circ> A)"
1.791 -    and si: "suminf (f \<circ> A) = z"
1.792 -    by (auto simp add: measure_set_def sums_iff)
1.793 +    and "s \<subseteq> (\<Union>x. A x)" and si: "psuminf (f \<circ> A) = z"
1.794 +    by (auto simp add: measure_set_def comp_def)
1.795    hence seq: "s = (\<Union>i. A i \<inter> s)" by blast
1.796    have inc: "increasing M f"
1.798 -  have sums: "(\<lambda>i. f (A i \<inter> s)) sums f (\<Union>i. A i \<inter> s)"
1.799 -    proof (rule countably_additiveD [OF ca])
1.800 +  have sums: "psuminf (\<lambda>i. f (A i \<inter> s)) = f (\<Union>i. A i \<inter> s)"
1.801 +    proof (rule countably_additiveD [OF ca])
1.802        show "range (\<lambda>n. A n \<inter> s) \<subseteq> sets M" using A s
1.803          by blast
1.804        show "disjoint_family (\<lambda>n. A n \<inter> s)" using disj
1.805 @@ -662,228 +518,184 @@
1.806        show "(\<Union>i. A i \<inter> s) \<in> sets M" using A s
1.807          by (metis UN_extend_simps(4) s seq)
1.808      qed
1.809 -  hence "f s = suminf (\<lambda>i. f (A i \<inter> s))"
1.810 +  hence "f s = psuminf (\<lambda>i. f (A i \<inter> s))"
1.811      using seq [symmetric] by (simp add: sums_iff)
1.812 -  also have "... \<le> suminf (f \<circ> A)"
1.813 -    proof (rule summable_le [OF _ _ sm])
1.814 -      show "\<forall>n. f (A n \<inter> s) \<le> (f \<circ> A) n" using A s
1.815 -        by (force intro: increasingD [OF inc])
1.816 -      show "summable (\<lambda>i. f (A i \<inter> s))" using sums
1.817 -        by (simp add: sums_iff)
1.818 +  also have "... \<le> psuminf (f \<circ> A)"
1.819 +    proof (rule psuminf_le)
1.820 +      fix n show "f (A n \<inter> s) \<le> (f \<circ> A) n" using A s
1.821 +        by (force intro: increasingD [OF inc])
1.822      qed
1.823 -  also have "... = z" by (rule si)
1.824 +  also have "... = z" by (rule si)
1.825    finally show "f s \<le> z" .
1.826  next
1.827    fix y
1.828 -  assume y: "!!u. u \<in> measure_set M f s \<Longrightarrow> y \<le> u"
1.829 +  assume y: "\<forall>u \<in> measure_set M f s. y \<le> u"
1.830    thus "y \<le> f s"
1.831 -    by (blast intro: inf_measure_nonempty [OF posf s subset_refl])
1.832 +    by (blast intro: inf_measure_nonempty [of f, OF posf s subset_refl])
1.833  qed
1.834
1.835  lemma (in algebra) inf_measure_empty:
1.836 -  assumes posf: "positive M f"
1.837 +  assumes posf: "positive f"
1.838    shows "Inf (measure_set M f {}) = 0"
1.839  proof (rule antisym)
1.840 -  show "0 \<le> Inf (measure_set M f {})"
1.841 -    by (metis empty_subsetI inf_measure_pos posf)
1.842    show "Inf (measure_set M f {}) \<le> 0"
1.843 -    by (metis Inf_lower empty_sets inf_measure_pos0 inf_measure_nonempty posf
1.844 -              positive_imp_0 subset_refl)
1.845 -qed
1.846 +    by (metis complete_lattice_class.Inf_lower empty_sets inf_measure_nonempty[OF posf] subset_refl posf[unfolded positive_def])
1.847 +qed simp
1.848
1.849  lemma (in algebra) inf_measure_positive:
1.850 -  "positive M f \<Longrightarrow>
1.851 -   positive (| space = space M, sets = Pow (space M) |)
1.852 -                  (\<lambda>x. Inf (measure_set M f x))"
1.853 -  by (simp add: positive_def inf_measure_empty inf_measure_pos)
1.854 +  "positive f \<Longrightarrow>
1.855 +   positive (\<lambda>x. Inf (measure_set M f x))"
1.856 +  by (simp add: positive_def inf_measure_empty)
1.857
1.858  lemma (in algebra) inf_measure_increasing:
1.859 -  assumes posf: "positive M f"
1.860 +  assumes posf: "positive f"
1.861    shows "increasing (| space = space M, sets = Pow (space M) |)
1.862                      (\<lambda>x. Inf (measure_set M f x))"
1.863 -apply (auto simp add: increasing_def)
1.864 -apply (rule Inf_greatest, metis emptyE inf_measure_nonempty top posf)
1.865 -apply (rule Inf_lower)
1.866 +apply (auto simp add: increasing_def)
1.867 +apply (rule complete_lattice_class.Inf_greatest)
1.868 +apply (rule complete_lattice_class.Inf_lower)
1.869  apply (clarsimp simp add: measure_set_def, rule_tac x=A in exI, blast)
1.870 -apply (blast intro: inf_measure_pos0 posf)
1.871  done
1.872
1.873
1.874  lemma (in algebra) inf_measure_le:
1.875 -  assumes posf: "positive M f" and inc: "increasing M f"
1.876 -      and x: "x \<in> {r . \<exists>A. range A \<subseteq> sets M & s \<subseteq> (\<Union>i. A i) & (f \<circ> A) sums r}"
1.877 +  assumes posf: "positive f" and inc: "increasing M f"
1.878 +      and x: "x \<in> {r . \<exists>A. range A \<subseteq> sets M \<and> s \<subseteq> (\<Union>i. A i) \<and> psuminf (f \<circ> A) = r}"
1.879    shows "Inf (measure_set M f s) \<le> x"
1.880  proof -
1.881    from x
1.882 -  obtain A where A: "range A \<subseteq> sets M" and ss: "s \<subseteq> (\<Union>i. A i)"
1.883 -             and sm: "summable (f \<circ> A)" and xeq: "suminf (f \<circ> A) = x"
1.884 -    by (auto simp add: sums_iff)
1.885 +  obtain A where A: "range A \<subseteq> sets M" and ss: "s \<subseteq> (\<Union>i. A i)"
1.886 +             and xeq: "psuminf (f \<circ> A) = x"
1.887 +    by auto
1.888    have dA: "range (disjointed A) \<subseteq> sets M"
1.889      by (metis A range_disjointed_sets)
1.890 -  have "\<forall>n. \<bar>(f o disjointed A) n\<bar> \<le> (f \<circ> A) n"
1.891 -    proof (auto)
1.892 -      fix n
1.893 -      have "\<bar>f (disjointed A n)\<bar> = f (disjointed A n)" using posf dA
1.894 -        by (auto simp add: positive_def image_subset_iff)
1.895 -      also have "... \<le> f (A n)"
1.896 -        by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A)
1.897 -      finally show "\<bar>f (disjointed A n)\<bar> \<le> f (A n)" .
1.898 -    qed
1.899 -  from Series.summable_le2 [OF this sm]
1.900 -  have sda:  "summable (f o disjointed A)"
1.901 -             "suminf (f o disjointed A) \<le> suminf (f \<circ> A)"
1.902 -    by blast+
1.903 -  hence ley: "suminf (f o disjointed A) \<le> x"
1.904 -    by (metis xeq)
1.905 -  from sda have "(f \<circ> disjointed A) sums suminf (f \<circ> disjointed A)"
1.906 -    by (simp add: sums_iff)
1.907 -  hence y: "suminf (f o disjointed A) \<in> measure_set M f s"
1.908 +  have "\<forall>n.(f o disjointed A) n \<le> (f \<circ> A) n" unfolding comp_def
1.909 +    by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A comp_def)
1.910 +  hence sda: "psuminf (f o disjointed A) \<le> psuminf (f \<circ> A)"
1.911 +    by (blast intro: psuminf_le)
1.912 +  hence ley: "psuminf (f o disjointed A) \<le> x"
1.913 +    by (metis xeq)
1.914 +  hence y: "psuminf (f o disjointed A) \<in> measure_set M f s"
1.915      apply (auto simp add: measure_set_def)
1.916 -    apply (rule_tac x="disjointed A" in exI)
1.917 -    apply (simp add: disjoint_family_disjointed UN_disjointed_eq ss dA)
1.918 +    apply (rule_tac x="disjointed A" in exI)
1.919 +    apply (simp add: disjoint_family_disjointed UN_disjointed_eq ss dA comp_def)
1.920      done
1.921    show ?thesis
1.922 -    by (blast intro: y order_trans [OF _ ley] inf_measure_pos0 posf)
1.923 +    by (blast intro: y order_trans [OF _ ley] posf complete_lattice_class.Inf_lower)
1.924  qed
1.925
1.926  lemma (in algebra) inf_measure_close:
1.927 -  assumes posf: "positive M f" and e: "0 < e" and ss: "s \<subseteq> (space M)"
1.928 -  shows "\<exists>A l. range A \<subseteq> sets M & disjoint_family A & s \<subseteq> (\<Union>i. A i) &
1.929 -               (f \<circ> A) sums l & l \<le> Inf (measure_set M f s) + e"
1.930 -proof -
1.931 -  have " measure_set M f s \<noteq> {}"
1.932 -    by (metis emptyE ss inf_measure_nonempty [OF posf top])
1.933 -  hence "\<exists>l \<in> measure_set M f s. l < Inf (measure_set M f s) + e"
1.934 -    by (rule Inf_close [OF _ e])
1.935 -  thus ?thesis
1.936 -    by (auto simp add: measure_set_def, rule_tac x=" A" in exI, auto)
1.937 +  assumes posf: "positive f" and e: "0 < e" and ss: "s \<subseteq> (space M)"
1.938 +  shows "\<exists>A. range A \<subseteq> sets M \<and> disjoint_family A \<and> s \<subseteq> (\<Union>i. A i) \<and>
1.939 +               psuminf (f \<circ> A) \<le> Inf (measure_set M f s) + e"
1.940 +proof (cases "Inf (measure_set M f s) = \<omega>")
1.941 +  case False
1.942 +  obtain l where "l \<in> measure_set M f s" "l \<le> Inf (measure_set M f s) + e"
1.943 +    using Inf_close[OF False e] by auto
1.944 +  thus ?thesis
1.945 +    by (auto intro!: exI[of _ l] simp: measure_set_def comp_def)
1.946 +next
1.947 +  case True
1.948 +  have "measure_set M f s \<noteq> {}"
1.949 +    by (metis emptyE ss inf_measure_nonempty [of f, OF posf top])
1.950 +  then obtain l where "l \<in> measure_set M f s" by auto
1.951 +  moreover from True have "l \<le> Inf (measure_set M f s) + e" by simp
1.952 +  ultimately show ?thesis
1.953 +    by (auto intro!: exI[of _ l] simp: measure_set_def comp_def)
1.954  qed
1.955
1.957 -  assumes posf: "positive M f" and inc: "increasing M f"
1.958 +  assumes posf: "positive f" and inc: "increasing M f"
1.959    shows "countably_subadditive (| space = space M, sets = Pow (space M) |)
1.960                    (\<lambda>x. Inf (measure_set M f x))"
1.962 -  fix A :: "nat \<Rightarrow> 'a set" and e :: real
1.963 -    assume A: "range A \<subseteq> Pow (space M)"
1.964 -       and disj: "disjoint_family A"
1.965 -       and sb: "(\<Union>i. A i) \<subseteq> space M"
1.966 -       and sum1: "summable (\<lambda>n. Inf (measure_set M f (A n)))"
1.967 -       and e: "0 < e"
1.968 -    have "!!n. \<exists>B l. range B \<subseteq> sets M \<and> disjoint_family B \<and> A n \<subseteq> (\<Union>i. B i) \<and>
1.969 -                    (f o B) sums l \<and>
1.970 -                    l \<le> Inf (measure_set M f (A n)) + e * (1/2)^(Suc n)"
1.971 -      apply (rule inf_measure_close [OF posf])
1.972 -      apply (metis e half mult_pos_pos zero_less_power)
1.973 -      apply (metis UNIV_I UN_subset_iff sb)
1.974 -      done
1.975 -    hence "\<exists>BB ll. \<forall>n. range (BB n) \<subseteq> sets M \<and> disjoint_family (BB n) \<and>
1.976 -                       A n \<subseteq> (\<Union>i. BB n i) \<and> (f o BB n) sums ll n \<and>
1.977 -                       ll n \<le> Inf (measure_set M f (A n)) + e * (1/2)^(Suc n)"
1.978 -      by (rule choice2)
1.979 -    then obtain BB ll
1.980 -      where BB: "!!n. (range (BB n) \<subseteq> sets M)"
1.981 -        and disjBB: "!!n. disjoint_family (BB n)"
1.982 -        and sbBB: "!!n. A n \<subseteq> (\<Union>i. BB n i)"
1.983 -        and BBsums: "!!n. (f o BB n) sums ll n"
1.984 -        and ll: "!!n. ll n \<le> Inf (measure_set M f (A n)) + e * (1/2)^(Suc n)"
1.985 -      by auto blast
1.986 -    have llpos: "!!n. 0 \<le> ll n"
1.987 -        by (metis BBsums sums_iff o_apply posf positive_imp_pos suminf_ge_zero
1.988 -              range_subsetD BB)
1.989 -    have sll: "summable ll &
1.990 -               suminf ll \<le> suminf (\<lambda>n. Inf (measure_set M f (A n))) + e"
1.991 -      proof -
1.992 -        have "(\<lambda>n. e * (1/2)^(Suc n)) sums (e*1)"
1.993 -          by (rule sums_mult [OF power_half_series])
1.994 -        hence sum0: "summable (\<lambda>n. e * (1 / 2) ^ Suc n)"
1.995 -          and eqe:  "(\<Sum>n. e * (1 / 2) ^ n / 2) = e"
1.996 -          by (auto simp add: sums_iff)
1.997 -        have 0: "suminf (\<lambda>n. Inf (measure_set M f (A n))) +
1.998 -                 suminf (\<lambda>n. e * (1/2)^(Suc n)) =
1.999 -                 suminf (\<lambda>n. Inf (measure_set M f (A n)) + e * (1/2)^(Suc n))"
1.1000 -          by (rule suminf_add [OF sum1 sum0])
1.1001 -        have 1: "\<forall>n. \<bar>ll n\<bar> \<le> Inf (measure_set M f (A n)) + e * (1/2) ^ Suc n"
1.1002 -          by (metis ll llpos abs_of_nonneg)
1.1003 -        have 2: "summable (\<lambda>n. Inf (measure_set M f (A n)) + e*(1/2)^(Suc n))"
1.1004 -          by (rule summable_add [OF sum1 sum0])
1.1005 -        have "suminf ll \<le> (\<Sum>n. Inf (measure_set M f (A n)) + e*(1/2) ^ Suc n)"
1.1006 -          using Series.summable_le2 [OF 1 2] by auto
1.1007 -        also have "... = (\<Sum>n. Inf (measure_set M f (A n))) +
1.1008 -                         (\<Sum>n. e * (1 / 2) ^ Suc n)"
1.1009 -          by (metis 0)
1.1010 -        also have "... = (\<Sum>n. Inf (measure_set M f (A n))) + e"
1.1011 -          by (simp add: eqe)
1.1012 -        finally show ?thesis using  Series.summable_le2 [OF 1 2] by auto
1.1013 -      qed
1.1014 -    def C \<equiv> "(split BB) o prod_decode"
1.1015 -    have C: "!!n. C n \<in> sets M"
1.1016 -      apply (rule_tac p="prod_decode n" in PairE)
1.1017 -      apply (simp add: C_def)
1.1018 -      apply (metis BB subsetD rangeI)
1.1019 -      done
1.1020 -    have sbC: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)"
1.1021 -      proof (auto simp add: C_def)
1.1022 -        fix x i
1.1023 -        assume x: "x \<in> A i"
1.1024 -        with sbBB [of i] obtain j where "x \<in> BB i j"
1.1025 -          by blast
1.1026 -        thus "\<exists>i. x \<in> split BB (prod_decode i)"
1.1027 -          by (metis prod_encode_inverse prod.cases)
1.1028 -      qed
1.1029 -    have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> prod_decode"
1.1030 -      by (rule ext)  (auto simp add: C_def)
1.1031 -    also have "... sums suminf ll"
1.1032 -      proof (rule suminf_2dimen)
1.1033 -        show "\<And>m n. 0 \<le> (f \<circ> (\<lambda>(x, y). BB x y)) (m, n)" using posf BB
1.1034 -          by (force simp add: positive_def)
1.1035 -        show "\<And>m. (\<lambda>n. (f \<circ> (\<lambda>(x, y). BB x y)) (m, n)) sums ll m"using BBsums BB
1.1036 -          by (force simp add: o_def)
1.1037 -        show "summable ll" using sll
1.1038 -          by auto
1.1039 -      qed
1.1040 -    finally have Csums: "(f \<circ> C) sums suminf ll" .
1.1041 -    have "Inf (measure_set M f (\<Union>i. A i)) \<le> suminf ll"
1.1042 -      apply (rule inf_measure_le [OF posf inc], auto)
1.1043 -      apply (rule_tac x="C" in exI)
1.1044 -      apply (auto simp add: C sbC Csums)
1.1045 -      done
1.1046 -    also have "... \<le> (\<Sum>n. Inf (measure_set M f (A n))) + e" using sll
1.1047 -      by blast
1.1048 -    finally show "Inf (measure_set M f (\<Union>i. A i)) \<le>
1.1049 -          (\<Sum>n. Inf (measure_set M f (A n))) + e" .
1.1051 +proof (safe, simp, rule pinfreal_le_epsilon)
1.1052 +  fix A :: "nat \<Rightarrow> 'a set" and e :: pinfreal
1.1053 +
1.1054 +  let "?outer n" = "Inf (measure_set M f (A n))"
1.1055 +  assume A: "range A \<subseteq> Pow (space M)"
1.1056 +     and disj: "disjoint_family A"
1.1057 +     and sb: "(\<Union>i. A i) \<subseteq> space M"
1.1058 +     and e: "0 < e"
1.1059 +  hence "\<exists>BB. \<forall>n. range (BB n) \<subseteq> sets M \<and> disjoint_family (BB n) \<and>
1.1060 +                   A n \<subseteq> (\<Union>i. BB n i) \<and>
1.1061 +                   psuminf (f o BB n) \<le> ?outer n + e * (1/2)^(Suc n)"
1.1062 +    apply (safe intro!: choice inf_measure_close [of f, OF posf _])
1.1063 +    using e sb by (cases e, auto simp add: not_le mult_pos_pos)
1.1064 +  then obtain BB
1.1065 +    where BB: "\<And>n. (range (BB n) \<subseteq> sets M)"
1.1066 +      and disjBB: "\<And>n. disjoint_family (BB n)"
1.1067 +      and sbBB: "\<And>n. A n \<subseteq> (\<Union>i. BB n i)"
1.1068 +      and BBle: "\<And>n. psuminf (f o BB n) \<le> ?outer n + e * (1/2)^(Suc n)"
1.1069 +    by auto blast
1.1070 +  have sll: "(\<Sum>\<^isub>\<infinity> n. psuminf (f o BB n)) \<le> psuminf ?outer + e"
1.1071 +    proof -
1.1072 +      have "(\<Sum>\<^isub>\<infinity> n. psuminf (f o BB n)) \<le> (\<Sum>\<^isub>\<infinity> n. ?outer n + e*(1/2) ^ Suc n)"
1.1073 +        by (rule psuminf_le[OF BBle])
1.1074 +      also have "... = psuminf ?outer + e"
1.1075 +        using psuminf_half_series by simp
1.1076 +      finally show ?thesis .
1.1077 +    qed
1.1078 +  def C \<equiv> "(split BB) o prod_decode"
1.1079 +  have C: "!!n. C n \<in> sets M"
1.1080 +    apply (rule_tac p="prod_decode n" in PairE)
1.1081 +    apply (simp add: C_def)
1.1082 +    apply (metis BB subsetD rangeI)
1.1083 +    done
1.1084 +  have sbC: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)"
1.1085 +    proof (auto simp add: C_def)
1.1086 +      fix x i
1.1087 +      assume x: "x \<in> A i"
1.1088 +      with sbBB [of i] obtain j where "x \<in> BB i j"
1.1089 +        by blast
1.1090 +      thus "\<exists>i. x \<in> split BB (prod_decode i)"
1.1091 +        by (metis prod_encode_inverse prod.cases)
1.1092 +    qed
1.1093 +  have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> prod_decode"
1.1094 +    by (rule ext)  (auto simp add: C_def)
1.1095 +  moreover have "psuminf ... = (\<Sum>\<^isub>\<infinity> n. psuminf (f o BB n))" using BBle
1.1096 +    by (force intro!: psuminf_2dimen simp: o_def)
1.1097 +  ultimately have Csums: "psuminf (f \<circ> C) = (\<Sum>\<^isub>\<infinity> n. psuminf (f o BB n))" by simp
1.1098 +  have "Inf (measure_set M f (\<Union>i. A i)) \<le> (\<Sum>\<^isub>\<infinity> n. psuminf (f o BB n))"
1.1099 +    apply (rule inf_measure_le [OF posf(1) inc], auto)
1.1100 +    apply (rule_tac x="C" in exI)
1.1101 +    apply (auto simp add: C sbC Csums)
1.1102 +    done
1.1103 +  also have "... \<le> (\<Sum>\<^isub>\<infinity>n. Inf (measure_set M f (A n))) + e" using sll
1.1104 +    by blast
1.1105 +  finally show "Inf (measure_set M f (\<Union>i. A i)) \<le> psuminf ?outer + e" .
1.1106  qed
1.1107
1.1108  lemma (in algebra) inf_measure_outer:
1.1109 -  "positive M f \<Longrightarrow> increasing M f
1.1110 +  "\<lbrakk> positive f ; increasing M f \<rbrakk>
1.1111     \<Longrightarrow> outer_measure_space (| space = space M, sets = Pow (space M) |)
1.1112                            (\<lambda>x. Inf (measure_set M f x))"
1.1113 -  by (simp add: outer_measure_space_def inf_measure_positive
1.1115 +  by (simp add: outer_measure_space_def inf_measure_empty
1.1117
1.1118  (*MOVE UP*)
1.1119
1.1120  lemma (in algebra) algebra_subset_lambda_system:
1.1121 -  assumes posf: "positive M f" and inc: "increasing M f"
1.1122 +  assumes posf: "positive f" and inc: "increasing M f"
1.1124    shows "sets M \<subseteq> lambda_system (| space = space M, sets = Pow (space M) |)
1.1125                                  (\<lambda>x. Inf (measure_set M f x))"
1.1126 -proof (auto dest: sets_into_space
1.1127 -            simp add: algebra.lambda_system_eq [OF algebra_Pow])
1.1128 +proof (auto dest: sets_into_space
1.1129 +            simp add: algebra.lambda_system_eq [OF algebra_Pow])
1.1130    fix x s
1.1131    assume x: "x \<in> sets M"
1.1132       and s: "s \<subseteq> space M"
1.1133 -  have [simp]: "!!x. x \<in> sets M \<Longrightarrow> s \<inter> (space M - x) = s-x" using s
1.1134 +  have [simp]: "!!x. x \<in> sets M \<Longrightarrow> s \<inter> (space M - x) = s-x" using s
1.1135      by blast
1.1136    have "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
1.1137          \<le> Inf (measure_set M f s)"
1.1138 -    proof (rule field_le_epsilon)
1.1139 -      fix e :: real
1.1140 +    proof (rule pinfreal_le_epsilon)
1.1141 +      fix e :: pinfreal
1.1142        assume e: "0 < e"
1.1143 -      from inf_measure_close [OF posf e s]
1.1144 -      obtain A l where A: "range A \<subseteq> sets M" and disj: "disjoint_family A"
1.1145 -                   and sUN: "s \<subseteq> (\<Union>i. A i)" and fsums: "(f \<circ> A) sums l"
1.1146 -                   and l: "l \<le> Inf (measure_set M f s) + e"
1.1147 +      from inf_measure_close [of f, OF posf e s]
1.1148 +      obtain A where A: "range A \<subseteq> sets M" and disj: "disjoint_family A"
1.1149 +                 and sUN: "s \<subseteq> (\<Union>i. A i)"
1.1150 +                 and l: "psuminf (f \<circ> A) \<le> Inf (measure_set M f s) + e"
1.1151          by auto
1.1152        have [simp]: "!!x. x \<in> sets M \<Longrightarrow>
1.1153                        (f o (\<lambda>z. z \<inter> (space M - x)) o A) = (f o (\<lambda>z. z - x) o A)"
1.1154 @@ -891,104 +703,87 @@
1.1155        have  [simp]: "!!n. f (A n \<inter> x) + f (A n - x) = f (A n)"
1.1157             (auto simp add: x range_subsetD [OF A] Int_Diff_Un Int_Diff_disjoint)
1.1158 -      have fsumb: "summable (f \<circ> A)"
1.1159 -        by (metis fsums sums_iff)
1.1160        { fix u
1.1161          assume u: "u \<in> sets M"
1.1162 -        have [simp]: "\<And>n. \<bar>f (A n \<inter> u)\<bar> \<le> f (A n)"
1.1163 -          by (simp add: positive_imp_pos [OF posf]  increasingD [OF inc]
1.1164 -                        u Int  range_subsetD [OF A])
1.1165 -        have 1: "summable (f o (\<lambda>z. z\<inter>u) o A)"
1.1166 -          by (rule summable_comparison_test [OF _ fsumb]) simp
1.1167 -        have 2: "Inf (measure_set M f (s\<inter>u)) \<le> suminf (f o (\<lambda>z. z\<inter>u) o A)"
1.1168 -          proof (rule Inf_lower)
1.1169 -            show "suminf (f \<circ> (\<lambda>z. z \<inter> u) \<circ> A) \<in> measure_set M f (s \<inter> u)"
1.1170 -              apply (simp add: measure_set_def)
1.1171 -              apply (rule_tac x="(\<lambda>z. z \<inter> u) o A" in exI)
1.1172 -              apply (auto simp add: disjoint_family_subset [OF disj])
1.1173 -              apply (blast intro: u range_subsetD [OF A])
1.1174 +        have [simp]: "\<And>n. f (A n \<inter> u) \<le> f (A n)"
1.1175 +          by (simp add: increasingD [OF inc] u Int range_subsetD [OF A])
1.1176 +        have 2: "Inf (measure_set M f (s \<inter> u)) \<le> psuminf (f \<circ> (\<lambda>z. z \<inter> u) \<circ> A)"
1.1177 +          proof (rule complete_lattice_class.Inf_lower)
1.1178 +            show "psuminf (f \<circ> (\<lambda>z. z \<inter> u) \<circ> A) \<in> measure_set M f (s \<inter> u)"
1.1179 +              apply (simp add: measure_set_def)
1.1180 +              apply (rule_tac x="(\<lambda>z. z \<inter> u) o A" in exI)
1.1181 +              apply (auto simp add: disjoint_family_subset [OF disj] o_def)
1.1182 +              apply (blast intro: u range_subsetD [OF A])
1.1183                apply (blast dest: subsetD [OF sUN])
1.1184 -              apply (metis 1 o_assoc sums_iff)
1.1185                done
1.1186 -          next
1.1187 -            show "\<And>x. x \<in> measure_set M f (s \<inter> u) \<Longrightarrow> 0 \<le> x"
1.1188 -              by (blast intro: inf_measure_pos0 [OF posf])
1.1189 -            qed
1.1190 -          note 1 2
1.1191 +          qed
1.1192        } note lesum = this
1.1193 -      have sum1: "summable (f o (\<lambda>z. z\<inter>x) o A)"
1.1194 -        and inf1: "Inf (measure_set M f (s\<inter>x)) \<le> suminf (f o (\<lambda>z. z\<inter>x) o A)"
1.1195 -        and sum2: "summable (f o (\<lambda>z. z \<inter> (space M - x)) o A)"
1.1196 -        and inf2: "Inf (measure_set M f (s \<inter> (space M - x)))
1.1197 -                   \<le> suminf (f o (\<lambda>z. z \<inter> (space M - x)) o A)"
1.1198 +      have inf1: "Inf (measure_set M f (s\<inter>x)) \<le> psuminf (f o (\<lambda>z. z\<inter>x) o A)"
1.1199 +        and inf2: "Inf (measure_set M f (s \<inter> (space M - x)))
1.1200 +                   \<le> psuminf (f o (\<lambda>z. z \<inter> (space M - x)) o A)"
1.1201          by (metis Diff lesum top x)+
1.1202        hence "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
1.1203 -           \<le> suminf (f o (\<lambda>s. s\<inter>x) o A) + suminf (f o (\<lambda>s. s-x) o A)"
1.1204 -        by (simp add: x)
1.1205 -      also have "... \<le> suminf (f o A)" using suminf_add [OF sum1 sum2]
1.1207 +           \<le> psuminf (f o (\<lambda>s. s\<inter>x) o A) + psuminf (f o (\<lambda>s. s-x) o A)"
1.1209 +      also have "... \<le> psuminf (f o A)"
1.1211        also have "... \<le> Inf (measure_set M f s) + e"
1.1212 -        by (metis fsums l sums_unique)
1.1213 +        by (rule l)
1.1214        finally show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
1.1215          \<le> Inf (measure_set M f s) + e" .
1.1216      qed
1.1217 -  moreover
1.1218 +  moreover
1.1219    have "Inf (measure_set M f s)
1.1220         \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))"
1.1221      proof -
1.1222      have "Inf (measure_set M f s) = Inf (measure_set M f ((s\<inter>x) \<union> (s-x)))"
1.1223        by (metis Un_Diff_Int Un_commute)
1.1224 -    also have "... \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))"
1.1227 +    also have "... \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))"
1.1231 -      apply (auto simp add: subsetD [OF s])
1.1232 +      apply (auto simp add: subsetD [OF s])
1.1233        done
1.1234      finally show ?thesis .
1.1235      qed
1.1236 -  ultimately
1.1237 +  ultimately
1.1238    show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
1.1239          = Inf (measure_set M f s)"
1.1240      by (rule order_antisym)
1.1241  qed
1.1242
1.1243  lemma measure_down:
1.1244 -     "measure_space N \<Longrightarrow> sigma_algebra M \<Longrightarrow> sets M \<subseteq> sets N \<Longrightarrow>
1.1245 -      (measure M = measure N) \<Longrightarrow> measure_space M"
1.1246 -  by (simp add: measure_space_def measure_space_axioms_def positive_def
1.1248 +     "measure_space N \<mu> \<Longrightarrow> sigma_algebra M \<Longrightarrow> sets M \<subseteq> sets N \<Longrightarrow>
1.1249 +      (\<nu> = \<mu>) \<Longrightarrow> measure_space M \<nu>"
1.1250 +  by (simp add: measure_space_def measure_space_axioms_def positive_def
1.1252       blast
1.1253
1.1254  theorem (in algebra) caratheodory:
1.1255 -  assumes posf: "positive M f" and ca: "countably_additive M f"
1.1256 -  shows "\<exists>MS :: 'a measure_space.
1.1257 -             (\<forall>s \<in> sets M. measure MS s = f s) \<and>
1.1258 -             ((|space = space MS, sets = sets MS|) = sigma (space M) (sets M)) \<and>
1.1259 -             measure_space MS"
1.1260 +  assumes posf: "positive f" and ca: "countably_additive M f"
1.1261 +  shows "\<exists>\<mu> :: 'a set \<Rightarrow> pinfreal. (\<forall>s \<in> sets M. \<mu> s = f s) \<and> measure_space (sigma (space M) (sets M)) \<mu>"
1.1262    proof -
1.1263      have inc: "increasing M f"
1.1266      let ?infm = "(\<lambda>x. Inf (measure_set M f x))"
1.1267      def ls \<equiv> "lambda_system (|space = space M, sets = Pow (space M)|) ?infm"
1.1268 -    have mls: "measure_space (|space = space M, sets = ls, measure = ?infm|)"
1.1269 +    have mls: "measure_space \<lparr>space = space M, sets = ls\<rparr> ?infm"
1.1270        using sigma_algebra.caratheodory_lemma
1.1271                [OF sigma_algebra_Pow  inf_measure_outer [OF posf inc]]
1.1273 -    hence sls: "sigma_algebra (|space = space M, sets = ls, measure = ?infm|)"
1.1274 -      by (simp add: measure_space_def)
1.1275 -    have "sets M \<subseteq> ls"
1.1276 +    hence sls: "sigma_algebra (|space = space M, sets = ls|)"
1.1277 +      by (simp add: measure_space_def)
1.1278 +    have "sets M \<subseteq> ls"
1.1281 -    hence sgs_sb: "sigma_sets (space M) (sets M) \<subseteq> ls"
1.1282 +    hence sgs_sb: "sigma_sets (space M) (sets M) \<subseteq> ls"
1.1283        using sigma_algebra.sigma_sets_subset [OF sls, of "sets M"]
1.1284        by simp
1.1285 -    have "measure_space (|space = space M,
1.1286 -                          sets = sigma_sets (space M) (sets M),
1.1287 -                          measure = ?infm|)"
1.1288 -      by (rule measure_down [OF mls], rule sigma_algebra_sigma_sets)
1.1289 +    have "measure_space (sigma (space M) (sets M)) ?infm"
1.1290 +      unfolding sigma_def
1.1291 +      by (rule measure_down [OF mls], rule sigma_algebra_sigma_sets)