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.4  header {*Caratheodory Extension Theorem*}
     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.34    additive  where
    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.42    countably_additive  where
    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.58    subadditive  where
    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.66    countably_subadditive  where
    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.118  lemma subadditiveD:
   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.122    by (auto simp add: subadditive_def)
   1.123  
   1.124  lemma additiveD:
   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.128    by (auto simp add: additive_def)
   1.129  
   1.130  lemma countably_additiveD:
   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.134    by (simp add: countably_additive_def)
   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.208    by (simp add:  lambda_system_def)
   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.284  lemma (in algebra) lambda_system_strong_additive:
   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.295        by (simp add: lambda_system_eq)
   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.304  lemma (in algebra) lambda_system_additive:
   1.305       "additive (M (|sets := lambda_system M f|)) f"
   1.306    proof (auto simp add: additive_def)
   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.314        by (simp add: Un)
   1.315    qed
   1.316  
   1.317  
   1.318  lemma (in algebra) countably_subadditive_subadditive:
   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.321    shows  "subadditive M f"
   1.322  proof (auto simp add: subadditive_def)
   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.331      using cs by (simp add: countably_subadditive_def)
   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.412  lemma (in algebra) additive_sum:
   1.413    fixes A:: "nat \<Rightarrow> 'a set"
   1.414 -  assumes f: "positive M f" and ad: "additive M f"
   1.415 +  assumes f: "positive 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.438 -    using ad UNION_in_sets A by (auto simp add: additive_def) 
   1.439 +    using ad UNION_in_sets A by (auto simp add: additive_def)
   1.440    with Suc.hyps show ?case using ad
   1.441 -    by (auto simp add: atLeastLessThanSuc additive_def) 
   1.442 +    by (auto simp add: atLeastLessThanSuc additive_def)
   1.443  qed
   1.444  
   1.445  
   1.446  lemma countably_subadditiveD:
   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.450    by (auto simp add: countably_subadditive_def o_def)
   1.451  
   1.452 -lemma (in algebra) increasing_additive_summable:
   1.453 -  fixes A:: "nat \<Rightarrow> 'a set"
   1.454 -  assumes f: "positive M f" and ad: "additive M f"
   1.455 +lemma (in algebra) increasing_additive_bound:
   1.456 +  fixes A:: "nat \<Rightarrow> 'a set" and  f :: "'a set \<Rightarrow> pinfreal"
   1.457 +  assumes f: "positive f" and ad: "additive M f"
   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.469 -    by (rule additive_sum [OF f ad A disj]) 
   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.474 +    by (rule additive_sum [OF f ad A disj])
   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.515      by (simp add: atLeastLessThanSuc lambda_system_strong_additive [OF a 2 3 4])
   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.529 -    by (metis countably_subadditive_subadditive csa pos) 
   1.530 -  have A': "range A \<subseteq> sets (M(|sets := lambda_system M f|))" using A 
   1.531 +    by (metis countably_subadditive_subadditive csa pos)
   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.541 -          lambda_system_positive lambda_system_additive lambda_system_increasing
   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.558 -                  lambda_system_positive lambda_system_additive 
   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.606 +          by (rule add_right_mono)
   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.680 -                  countably_additive_def o_def) 
   1.681 -  ultimately 
   1.682 +    by (simp add: measure_space_axioms_def positive_def lambda_system_sets
   1.683 +                  countably_additive_def o_def)
   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.727  lemma (in algebra) additive_increasing:
   1.728 -  assumes posf: "positive M f" and addf: "additive M f" 
   1.729 +  assumes posf: "positive 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.739      by (auto simp add: additive_def) (metis Diff_disjoint Un_Diff_cancel Diff xy(1,2))
   1.740    also have "... = f y"
   1.741 @@ -619,42 +475,42 @@
   1.742  qed
   1.743  
   1.744  lemma (in algebra) countably_additive_additive:
   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.747    shows "additive M f"
   1.748 -proof (auto simp add: additive_def) 
   1.749 +proof (auto simp add: additive_def)
   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.762 -    by (simp add: countably_additive_def) (metis UN_binaryset_eq sums_unique) 
   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.765 +    by (simp add: countably_additive_def)
   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.797      by (metis additive_increasing ca countably_additive_additive posf)
   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.956  lemma (in algebra) inf_measure_countably_subadditive:
   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.961 -proof (auto simp add: countably_subadditive_def o_def, rule field_le_epsilon)
   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.1050 +  unfolding countably_subadditive_def o_def
  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.1114 -                inf_measure_increasing inf_measure_countably_subadditive) 
  1.1115 +  by (simp add: outer_measure_space_def inf_measure_empty
  1.1116 +                inf_measure_increasing inf_measure_countably_subadditive positive_def)
  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.1123        and add: "additive 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.1156          by (subst additiveD [OF add, symmetric])
  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.1206 -        by (simp add: x) (simp add: o_def) 
  1.1207 +           \<le> psuminf (f o (\<lambda>s. s\<inter>x) o A) + psuminf (f o (\<lambda>s. s-x) o A)"
  1.1208 +        by (simp add: x add_mono)
  1.1209 +      also have "... \<le> psuminf (f o A)"
  1.1210 +        by (simp add: x psuminf_add[symmetric] o_def)
  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.1225 -      apply (rule subadditiveD) 
  1.1226 -      apply (iprover intro: algebra.countably_subadditive_subadditive algebra_Pow 
  1.1227 +    also have "... \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))"
  1.1228 +      apply (rule subadditiveD)
  1.1229 +      apply (iprover intro: algebra.countably_subadditive_subadditive algebra_Pow
  1.1230                 inf_measure_positive inf_measure_countably_subadditive posf inc)
  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.1247 -                countably_additive_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.1251 +                countably_additive_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.1264 -      by (metis additive_increasing ca countably_additive_additive posf) 
  1.1265 +      by (metis additive_increasing ca countably_additive_additive posf)
  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.1272        by (simp add: ls_def)
  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.1279        by (simp add: ls_def)
  1.1280           (metis ca posf inc countably_additive_additive algebra_subset_lambda_system)
  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)
  1.1292           (simp_all add: sgs_sb space_closed)
  1.1293 -    thus ?thesis
  1.1294 -      by (force simp add: sigma_def inf_measure_agrees [OF posf ca]) 
  1.1295 -qed
  1.1296 +    thus ?thesis using inf_measure_agrees [OF posf ca] by (auto intro!: exI[of _ ?infm])
  1.1297 +  qed
  1.1298  
  1.1299  end