src/HOL/Probability/Caratheodory.thy
 author hoelzl Mon Aug 23 19:35:57 2010 +0200 (2010-08-23) changeset 38656 d5d342611edb parent 37591 d3daea901123 child 39096 111756225292 permissions -rw-r--r--
Rewrite the Probability theory.

Introduced pinfreal as real numbers with infinity.
Use pinfreal as value for measures.
Introduces Lebesgue Measure based on the integral in Multivariate Analysis.
Proved Radon Nikodym for arbitrary sigma finite measure spaces.
```     1 header {*Caratheodory Extension Theorem*}
```
```     2
```
```     3 theory Caratheodory
```
```     4   imports Sigma_Algebra Positive_Infinite_Real
```
```     5 begin
```
```     6
```
```     7 text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
```
```     8
```
```     9 subsection {* Measure Spaces *}
```
```    10
```
```    11 definition "positive f \<longleftrightarrow> f {} = (0::pinfreal)" -- "Positive is enforced by the type"
```
```    12
```
```    13 definition
```
```    14   additive  where
```
```    15   "additive M f \<longleftrightarrow>
```
```    16     (\<forall>x \<in> sets M. \<forall>y \<in> sets M. x \<inter> y = {}
```
```    17     \<longrightarrow> f (x \<union> y) = f x + f y)"
```
```    18
```
```    19 definition
```
```    20   countably_additive  where
```
```    21   "countably_additive M f \<longleftrightarrow>
```
```    22     (\<forall>A. range A \<subseteq> sets M \<longrightarrow>
```
```    23          disjoint_family A \<longrightarrow>
```
```    24          (\<Union>i. A i) \<in> sets M \<longrightarrow>
```
```    25          (\<Sum>\<^isub>\<infinity> n. f (A n)) = f (\<Union>i. A i))"
```
```    26
```
```    27 definition
```
```    28   increasing  where
```
```    29   "increasing M f \<longleftrightarrow> (\<forall>x \<in> sets M. \<forall>y \<in> sets M. x \<subseteq> y \<longrightarrow> f x \<le> f y)"
```
```    30
```
```    31 definition
```
```    32   subadditive  where
```
```    33   "subadditive M f \<longleftrightarrow>
```
```    34     (\<forall>x \<in> sets M. \<forall>y \<in> sets M. x \<inter> y = {}
```
```    35     \<longrightarrow> f (x \<union> y) \<le> f x + f y)"
```
```    36
```
```    37 definition
```
```    38   countably_subadditive  where
```
```    39   "countably_subadditive M f \<longleftrightarrow>
```
```    40     (\<forall>A. range A \<subseteq> sets M \<longrightarrow>
```
```    41          disjoint_family A \<longrightarrow>
```
```    42          (\<Union>i. A i) \<in> sets M \<longrightarrow>
```
```    43          f (\<Union>i. A i) \<le> psuminf (\<lambda>n. f (A n)))"
```
```    44
```
```    45 definition
```
```    46   lambda_system where
```
```    47   "lambda_system M f =
```
```    48     {l. l \<in> sets M & (\<forall>x \<in> sets M. f (l \<inter> x) + f ((space M - l) \<inter> x) = f x)}"
```
```    49
```
```    50 definition
```
```    51   outer_measure_space where
```
```    52   "outer_measure_space M f  \<longleftrightarrow>
```
```    53      positive f \<and> increasing M f \<and> countably_subadditive M f"
```
```    54
```
```    55 definition
```
```    56   measure_set where
```
```    57   "measure_set M f X =
```
```    58      {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}"
```
```    59
```
```    60 locale measure_space = sigma_algebra +
```
```    61   fixes \<mu> :: "'a set \<Rightarrow> pinfreal"
```
```    62   assumes empty_measure [simp]: "\<mu> {} = 0"
```
```    63       and ca: "countably_additive M \<mu>"
```
```    64
```
```    65 lemma increasingD:
```
```    66      "increasing M f \<Longrightarrow> x \<subseteq> y \<Longrightarrow> x\<in>sets M \<Longrightarrow> y\<in>sets M \<Longrightarrow> f x \<le> f y"
```
```    67   by (auto simp add: increasing_def)
```
```    68
```
```    69 lemma subadditiveD:
```
```    70      "subadditive M f \<Longrightarrow> x \<inter> y = {} \<Longrightarrow> x\<in>sets M \<Longrightarrow> y\<in>sets M
```
```    71       \<Longrightarrow> f (x \<union> y) \<le> f x + f y"
```
```    72   by (auto simp add: subadditive_def)
```
```    73
```
```    74 lemma additiveD:
```
```    75      "additive M f \<Longrightarrow> x \<inter> y = {} \<Longrightarrow> x\<in>sets M \<Longrightarrow> y\<in>sets M
```
```    76       \<Longrightarrow> f (x \<union> y) = f x + f y"
```
```    77   by (auto simp add: additive_def)
```
```    78
```
```    79 lemma countably_additiveD:
```
```    80   "countably_additive M f \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A
```
```    81    \<Longrightarrow> (\<Union>i. A i) \<in> sets M \<Longrightarrow> (\<Sum>\<^isub>\<infinity> n. f (A n)) = f (\<Union>i. A i)"
```
```    82   by (simp add: countably_additive_def)
```
```    83
```
```    84 section "Extend binary sets"
```
```    85
```
```    86 lemma LIMSEQ_binaryset:
```
```    87   assumes f: "f {} = 0"
```
```    88   shows  "(\<lambda>n. \<Sum>i = 0..<n. f (binaryset A B i)) ----> f A + f B"
```
```    89 proof -
```
```    90   have "(\<lambda>n. \<Sum>i = 0..< Suc (Suc n). f (binaryset A B i)) = (\<lambda>n. f A + f B)"
```
```    91     proof
```
```    92       fix n
```
```    93       show "(\<Sum>i\<Colon>nat = 0\<Colon>nat..<Suc (Suc n). f (binaryset A B i)) = f A + f B"
```
```    94         by (induct n)  (auto simp add: binaryset_def f)
```
```    95     qed
```
```    96   moreover
```
```    97   have "... ----> f A + f B" by (rule LIMSEQ_const)
```
```    98   ultimately
```
```    99   have "(\<lambda>n. \<Sum>i = 0..< Suc (Suc n). f (binaryset A B i)) ----> f A + f B"
```
```   100     by metis
```
```   101   hence "(\<lambda>n. \<Sum>i = 0..< n+2. f (binaryset A B i)) ----> f A + f B"
```
```   102     by simp
```
```   103   thus ?thesis by (rule LIMSEQ_offset [where k=2])
```
```   104 qed
```
```   105
```
```   106 lemma binaryset_sums:
```
```   107   assumes f: "f {} = 0"
```
```   108   shows  "(\<lambda>n. f (binaryset A B n)) sums (f A + f B)"
```
```   109     by (simp add: sums_def LIMSEQ_binaryset [where f=f, OF f])
```
```   110
```
```   111 lemma suminf_binaryset_eq:
```
```   112      "f {} = 0 \<Longrightarrow> suminf (\<lambda>n. f (binaryset A B n)) = f A + f B"
```
```   113   by (metis binaryset_sums sums_unique)
```
```   114
```
```   115 lemma binaryset_psuminf:
```
```   116   assumes "f {} = 0"
```
```   117   shows "(\<Sum>\<^isub>\<infinity> n. f (binaryset A B n)) = f A + f B" (is "?suminf = ?sum")
```
```   118 proof -
```
```   119   have *: "{..<2} = {0, 1::nat}" by auto
```
```   120   have "\<forall>n\<ge>2. f (binaryset A B n) = 0"
```
```   121     unfolding binaryset_def
```
```   122     using assms by auto
```
```   123   hence "?suminf = (\<Sum>N<2. f (binaryset A B N))"
```
```   124     by (rule psuminf_finite)
```
```   125   also have "... = ?sum" unfolding * binaryset_def
```
```   126     by simp
```
```   127   finally show ?thesis .
```
```   128 qed
```
```   129
```
```   130 subsection {* Lambda Systems *}
```
```   131
```
```   132 lemma (in algebra) lambda_system_eq:
```
```   133     "lambda_system M f =
```
```   134         {l. l \<in> sets M & (\<forall>x \<in> sets M. f (x \<inter> l) + f (x - l) = f x)}"
```
```   135 proof -
```
```   136   have [simp]: "!!l x. l \<in> sets M \<Longrightarrow> x \<in> sets M \<Longrightarrow> (space M - l) \<inter> x = x - l"
```
```   137     by (metis Int_Diff Int_absorb1 Int_commute sets_into_space)
```
```   138   show ?thesis
```
```   139     by (auto simp add: lambda_system_def) (metis Int_commute)+
```
```   140 qed
```
```   141
```
```   142 lemma (in algebra) lambda_system_empty:
```
```   143   "positive f \<Longrightarrow> {} \<in> lambda_system M f"
```
```   144   by (auto simp add: positive_def lambda_system_eq)
```
```   145
```
```   146 lemma lambda_system_sets:
```
```   147     "x \<in> lambda_system M f \<Longrightarrow> x \<in> sets M"
```
```   148   by (simp add:  lambda_system_def)
```
```   149
```
```   150 lemma (in algebra) lambda_system_Compl:
```
```   151   fixes f:: "'a set \<Rightarrow> pinfreal"
```
```   152   assumes x: "x \<in> lambda_system M f"
```
```   153   shows "space M - x \<in> lambda_system M f"
```
```   154   proof -
```
```   155     have "x \<subseteq> space M"
```
```   156       by (metis sets_into_space lambda_system_sets x)
```
```   157     hence "space M - (space M - x) = x"
```
```   158       by (metis double_diff equalityE)
```
```   159     with x show ?thesis
```
```   160       by (force simp add: lambda_system_def ac_simps)
```
```   161   qed
```
```   162
```
```   163 lemma (in algebra) lambda_system_Int:
```
```   164   fixes f:: "'a set \<Rightarrow> pinfreal"
```
```   165   assumes xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f"
```
```   166   shows "x \<inter> y \<in> lambda_system M f"
```
```   167   proof -
```
```   168     from xl yl show ?thesis
```
```   169       proof (auto simp add: positive_def lambda_system_eq Int)
```
```   170         fix u
```
```   171         assume x: "x \<in> sets M" and y: "y \<in> sets M" and u: "u \<in> sets M"
```
```   172            and fx: "\<forall>z\<in>sets M. f (z \<inter> x) + f (z - x) = f z"
```
```   173            and fy: "\<forall>z\<in>sets M. f (z \<inter> y) + f (z - y) = f z"
```
```   174         have "u - x \<inter> y \<in> sets M"
```
```   175           by (metis Diff Diff_Int Un u x y)
```
```   176         moreover
```
```   177         have "(u - (x \<inter> y)) \<inter> y = u \<inter> y - x" by blast
```
```   178         moreover
```
```   179         have "u - x \<inter> y - y = u - y" by blast
```
```   180         ultimately
```
```   181         have ey: "f (u - x \<inter> y) = f (u \<inter> y - x) + f (u - y)" using fy
```
```   182           by force
```
```   183         have "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y)
```
```   184               = (f (u \<inter> (x \<inter> y)) + f (u \<inter> y - x)) + f (u - y)"
```
```   185           by (simp add: ey ac_simps)
```
```   186         also have "... =  (f ((u \<inter> y) \<inter> x) + f (u \<inter> y - x)) + f (u - y)"
```
```   187           by (simp add: Int_ac)
```
```   188         also have "... = f (u \<inter> y) + f (u - y)"
```
```   189           using fx [THEN bspec, of "u \<inter> y"] Int y u
```
```   190           by force
```
```   191         also have "... = f u"
```
```   192           by (metis fy u)
```
```   193         finally show "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y) = f u" .
```
```   194       qed
```
```   195   qed
```
```   196
```
```   197
```
```   198 lemma (in algebra) lambda_system_Un:
```
```   199   fixes f:: "'a set \<Rightarrow> pinfreal"
```
```   200   assumes xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f"
```
```   201   shows "x \<union> y \<in> lambda_system M f"
```
```   202 proof -
```
```   203   have "(space M - x) \<inter> (space M - y) \<in> sets M"
```
```   204     by (metis Diff_Un Un compl_sets lambda_system_sets xl yl)
```
```   205   moreover
```
```   206   have "x \<union> y = space M - ((space M - x) \<inter> (space M - y))"
```
```   207     by auto  (metis subsetD lambda_system_sets sets_into_space xl yl)+
```
```   208   ultimately show ?thesis
```
```   209     by (metis lambda_system_Compl lambda_system_Int xl yl)
```
```   210 qed
```
```   211
```
```   212 lemma (in algebra) lambda_system_algebra:
```
```   213   "positive f \<Longrightarrow> algebra (M (|sets := lambda_system M f|))"
```
```   214   apply (auto simp add: algebra_def)
```
```   215   apply (metis lambda_system_sets set_mp sets_into_space)
```
```   216   apply (metis lambda_system_empty)
```
```   217   apply (metis lambda_system_Compl)
```
```   218   apply (metis lambda_system_Un)
```
```   219   done
```
```   220
```
```   221 lemma (in algebra) lambda_system_strong_additive:
```
```   222   assumes z: "z \<in> sets M" and disj: "x \<inter> y = {}"
```
```   223       and xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f"
```
```   224   shows "f (z \<inter> (x \<union> y)) = f (z \<inter> x) + f (z \<inter> y)"
```
```   225   proof -
```
```   226     have "z \<inter> x = (z \<inter> (x \<union> y)) \<inter> x" using disj by blast
```
```   227     moreover
```
```   228     have "z \<inter> y = (z \<inter> (x \<union> y)) - x" using disj by blast
```
```   229     moreover
```
```   230     have "(z \<inter> (x \<union> y)) \<in> sets M"
```
```   231       by (metis Int Un lambda_system_sets xl yl z)
```
```   232     ultimately show ?thesis using xl yl
```
```   233       by (simp add: lambda_system_eq)
```
```   234   qed
```
```   235
```
```   236 lemma (in algebra) lambda_system_additive:
```
```   237      "additive (M (|sets := lambda_system M f|)) f"
```
```   238   proof (auto simp add: additive_def)
```
```   239     fix x and y
```
```   240     assume disj: "x \<inter> y = {}"
```
```   241        and xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f"
```
```   242     hence  "x \<in> sets M" "y \<in> sets M" by (blast intro: lambda_system_sets)+
```
```   243     thus "f (x \<union> y) = f x + f y"
```
```   244       using lambda_system_strong_additive [OF top disj xl yl]
```
```   245       by (simp add: Un)
```
```   246   qed
```
```   247
```
```   248
```
```   249 lemma (in algebra) countably_subadditive_subadditive:
```
```   250   assumes f: "positive f" and cs: "countably_subadditive M f"
```
```   251   shows  "subadditive M f"
```
```   252 proof (auto simp add: subadditive_def)
```
```   253   fix x y
```
```   254   assume x: "x \<in> sets M" and y: "y \<in> sets M" and "x \<inter> y = {}"
```
```   255   hence "disjoint_family (binaryset x y)"
```
```   256     by (auto simp add: disjoint_family_on_def binaryset_def)
```
```   257   hence "range (binaryset x y) \<subseteq> sets M \<longrightarrow>
```
```   258          (\<Union>i. binaryset x y i) \<in> sets M \<longrightarrow>
```
```   259          f (\<Union>i. binaryset x y i) \<le> (\<Sum>\<^isub>\<infinity> n. f (binaryset x y n))"
```
```   260     using cs by (simp add: countably_subadditive_def)
```
```   261   hence "{x,y,{}} \<subseteq> sets M \<longrightarrow> x \<union> y \<in> sets M \<longrightarrow>
```
```   262          f (x \<union> y) \<le> (\<Sum>\<^isub>\<infinity> n. f (binaryset x y n))"
```
```   263     by (simp add: range_binaryset_eq UN_binaryset_eq)
```
```   264   thus "f (x \<union> y) \<le>  f x + f y" using f x y
```
```   265     by (auto simp add: Un o_def binaryset_psuminf positive_def)
```
```   266 qed
```
```   267
```
```   268 lemma (in algebra) additive_sum:
```
```   269   fixes A:: "nat \<Rightarrow> 'a set"
```
```   270   assumes f: "positive f" and ad: "additive M f"
```
```   271       and A: "range A \<subseteq> sets M"
```
```   272       and disj: "disjoint_family A"
```
```   273   shows  "setsum (f \<circ> A) {0..<n} = f (\<Union>i\<in>{0..<n}. A i)"
```
```   274 proof (induct n)
```
```   275   case 0 show ?case using f by (simp add: positive_def)
```
```   276 next
```
```   277   case (Suc n)
```
```   278   have "A n \<inter> (\<Union>i\<in>{0..<n}. A i) = {}" using disj
```
```   279     by (auto simp add: disjoint_family_on_def neq_iff) blast
```
```   280   moreover
```
```   281   have "A n \<in> sets M" using A by blast
```
```   282   moreover have "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
```
```   283     by (metis A UNION_in_sets atLeast0LessThan)
```
```   284   moreover
```
```   285   ultimately have "f (A n \<union> (\<Union>i\<in>{0..<n}. A i)) = f (A n) + f(\<Union>i\<in>{0..<n}. A i)"
```
```   286     using ad UNION_in_sets A by (auto simp add: additive_def)
```
```   287   with Suc.hyps show ?case using ad
```
```   288     by (auto simp add: atLeastLessThanSuc additive_def)
```
```   289 qed
```
```   290
```
```   291
```
```   292 lemma countably_subadditiveD:
```
```   293   "countably_subadditive M f \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A \<Longrightarrow>
```
```   294    (\<Union>i. A i) \<in> sets M \<Longrightarrow> f (\<Union>i. A i) \<le> psuminf (f o A)"
```
```   295   by (auto simp add: countably_subadditive_def o_def)
```
```   296
```
```   297 lemma (in algebra) increasing_additive_bound:
```
```   298   fixes A:: "nat \<Rightarrow> 'a set" and  f :: "'a set \<Rightarrow> pinfreal"
```
```   299   assumes f: "positive f" and ad: "additive M f"
```
```   300       and inc: "increasing M f"
```
```   301       and A: "range A \<subseteq> sets M"
```
```   302       and disj: "disjoint_family A"
```
```   303   shows  "psuminf (f \<circ> A) \<le> f (space M)"
```
```   304 proof (safe intro!: psuminf_bound)
```
```   305   fix N
```
```   306   have "setsum (f \<circ> A) {0..<N} = f (\<Union>i\<in>{0..<N}. A i)"
```
```   307     by (rule additive_sum [OF f ad A disj])
```
```   308   also have "... \<le> f (space M)" using space_closed A
```
```   309     by (blast intro: increasingD [OF inc] UNION_in_sets top)
```
```   310   finally show "setsum (f \<circ> A) {..<N} \<le> f (space M)" by (simp add: atLeast0LessThan)
```
```   311 qed
```
```   312
```
```   313 lemma lambda_system_increasing:
```
```   314    "increasing M f \<Longrightarrow> increasing (M (|sets := lambda_system M f|)) f"
```
```   315   by (simp add: increasing_def lambda_system_def)
```
```   316
```
```   317 lemma (in algebra) lambda_system_strong_sum:
```
```   318   fixes A:: "nat \<Rightarrow> 'a set" and f :: "'a set \<Rightarrow> pinfreal"
```
```   319   assumes f: "positive f" and a: "a \<in> sets M"
```
```   320       and A: "range A \<subseteq> lambda_system M f"
```
```   321       and disj: "disjoint_family A"
```
```   322   shows  "(\<Sum>i = 0..<n. f (a \<inter>A i)) = f (a \<inter> (\<Union>i\<in>{0..<n}. A i))"
```
```   323 proof (induct n)
```
```   324   case 0 show ?case using f by (simp add: positive_def)
```
```   325 next
```
```   326   case (Suc n)
```
```   327   have 2: "A n \<inter> UNION {0..<n} A = {}" using disj
```
```   328     by (force simp add: disjoint_family_on_def neq_iff)
```
```   329   have 3: "A n \<in> lambda_system M f" using A
```
```   330     by blast
```
```   331   have 4: "UNION {0..<n} A \<in> lambda_system M f"
```
```   332     using A algebra.UNION_in_sets [OF local.lambda_system_algebra, of f, OF f]
```
```   333     by simp
```
```   334   from Suc.hyps show ?case
```
```   335     by (simp add: atLeastLessThanSuc lambda_system_strong_additive [OF a 2 3 4])
```
```   336 qed
```
```   337
```
```   338
```
```   339 lemma (in sigma_algebra) lambda_system_caratheodory:
```
```   340   assumes oms: "outer_measure_space M f"
```
```   341       and A: "range A \<subseteq> lambda_system M f"
```
```   342       and disj: "disjoint_family A"
```
```   343   shows  "(\<Union>i. A i) \<in> lambda_system M f \<and> psuminf (f \<circ> A) = f (\<Union>i. A i)"
```
```   344 proof -
```
```   345   have pos: "positive f" and inc: "increasing M f"
```
```   346    and csa: "countably_subadditive M f"
```
```   347     by (metis oms outer_measure_space_def)+
```
```   348   have sa: "subadditive M f"
```
```   349     by (metis countably_subadditive_subadditive csa pos)
```
```   350   have A': "range A \<subseteq> sets (M(|sets := lambda_system M f|))" using A
```
```   351     by simp
```
```   352   have alg_ls: "algebra (M(|sets := lambda_system M f|))"
```
```   353     by (rule lambda_system_algebra) (rule pos)
```
```   354   have A'': "range A \<subseteq> sets M"
```
```   355      by (metis A image_subset_iff lambda_system_sets)
```
```   356
```
```   357   have U_in: "(\<Union>i. A i) \<in> sets M"
```
```   358     by (metis A'' countable_UN)
```
```   359   have U_eq: "f (\<Union>i. A i) = psuminf (f o A)"
```
```   360     proof (rule antisym)
```
```   361       show "f (\<Union>i. A i) \<le> psuminf (f \<circ> A)"
```
```   362         by (rule countably_subadditiveD [OF csa A'' disj U_in])
```
```   363       show "psuminf (f \<circ> A) \<le> f (\<Union>i. A i)"
```
```   364         by (rule psuminf_bound, unfold atLeast0LessThan[symmetric])
```
```   365            (metis algebra.additive_sum [OF alg_ls] pos disj UN_Un Un_UNIV_right
```
```   366                   lambda_system_additive subset_Un_eq increasingD [OF inc]
```
```   367                   A' A'' UNION_in_sets U_in)
```
```   368     qed
```
```   369   {
```
```   370     fix a
```
```   371     assume a [iff]: "a \<in> sets M"
```
```   372     have "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) = f a"
```
```   373     proof -
```
```   374       show ?thesis
```
```   375       proof (rule antisym)
```
```   376         have "range (\<lambda>i. a \<inter> A i) \<subseteq> sets M" using A''
```
```   377           by blast
```
```   378         moreover
```
```   379         have "disjoint_family (\<lambda>i. a \<inter> A i)" using disj
```
```   380           by (auto simp add: disjoint_family_on_def)
```
```   381         moreover
```
```   382         have "a \<inter> (\<Union>i. A i) \<in> sets M"
```
```   383           by (metis Int U_in a)
```
```   384         ultimately
```
```   385         have "f (a \<inter> (\<Union>i. A i)) \<le> psuminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)"
```
```   386           using countably_subadditiveD [OF csa, of "(\<lambda>i. a \<inter> A i)"]
```
```   387           by (simp add: o_def)
```
```   388         hence "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le>
```
```   389             psuminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) + f (a - (\<Union>i. A i))"
```
```   390           by (rule add_right_mono)
```
```   391         moreover
```
```   392         have "psuminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) + f (a - (\<Union>i. A i)) \<le> f a"
```
```   393           proof (safe intro!: psuminf_bound_add)
```
```   394             fix n
```
```   395             have UNION_in: "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
```
```   396               by (metis A'' UNION_in_sets)
```
```   397             have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A''
```
```   398               by (blast intro: increasingD [OF inc] A'' UNION_in_sets)
```
```   399             have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system M f"
```
```   400               using algebra.UNION_in_sets [OF lambda_system_algebra [of f, OF pos]]
```
```   401               by (simp add: A)
```
```   402             hence eq_fa: "f a = f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i))"
```
```   403               by (simp add: lambda_system_eq UNION_in)
```
```   404             have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))"
```
```   405               by (blast intro: increasingD [OF inc] UNION_eq_Union_image
```
```   406                                UNION_in U_in)
```
```   407             thus "setsum (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) {..<n} + f (a - (\<Union>i. A i)) \<le> f a"
```
```   408               by (simp add: lambda_system_strong_sum pos A disj eq_fa add_left_mono atLeast0LessThan[symmetric])
```
```   409           qed
```
```   410         ultimately show "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le> f a"
```
```   411           by (rule order_trans)
```
```   412       next
```
```   413         have "f a \<le> f (a \<inter> (\<Union>i. A i) \<union> (a - (\<Union>i. A i)))"
```
```   414           by (blast intro:  increasingD [OF inc] U_in)
```
```   415         also have "... \<le>  f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))"
```
```   416           by (blast intro: subadditiveD [OF sa] U_in)
```
```   417         finally show "f a \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))" .
```
```   418         qed
```
```   419      qed
```
```   420   }
```
```   421   thus  ?thesis
```
```   422     by (simp add: lambda_system_eq sums_iff U_eq U_in)
```
```   423 qed
```
```   424
```
```   425 lemma (in sigma_algebra) caratheodory_lemma:
```
```   426   assumes oms: "outer_measure_space M f"
```
```   427   shows "measure_space (|space = space M, sets = lambda_system M f|) f"
```
```   428 proof -
```
```   429   have pos: "positive f"
```
```   430     by (metis oms outer_measure_space_def)
```
```   431   have alg: "algebra (|space = space M, sets = lambda_system M f|)"
```
```   432     using lambda_system_algebra [of f, OF pos]
```
```   433     by (simp add: algebra_def)
```
```   434   then moreover
```
```   435   have "sigma_algebra (|space = space M, sets = lambda_system M f|)"
```
```   436     using lambda_system_caratheodory [OF oms]
```
```   437     by (simp add: sigma_algebra_disjoint_iff)
```
```   438   moreover
```
```   439   have "measure_space_axioms (|space = space M, sets = lambda_system M f|) f"
```
```   440     using pos lambda_system_caratheodory [OF oms]
```
```   441     by (simp add: measure_space_axioms_def positive_def lambda_system_sets
```
```   442                   countably_additive_def o_def)
```
```   443   ultimately
```
```   444   show ?thesis
```
```   445     by intro_locales (auto simp add: sigma_algebra_def)
```
```   446 qed
```
```   447
```
```   448
```
```   449 lemma (in algebra) inf_measure_nonempty:
```
```   450   assumes f: "positive f" and b: "b \<in> sets M" and a: "a \<subseteq> b"
```
```   451   shows "f b \<in> measure_set M f a"
```
```   452 proof -
```
```   453   have "psuminf (f \<circ> (\<lambda>i. {})(0 := b)) = setsum (f \<circ> (\<lambda>i. {})(0 := b)) {..<1::nat}"
```
```   454     by (rule psuminf_finite) (simp add: f[unfolded positive_def])
```
```   455   also have "... = f b"
```
```   456     by simp
```
```   457   finally have "psuminf (f \<circ> (\<lambda>i. {})(0 := b)) = f b" .
```
```   458   thus ?thesis using a b
```
```   459     by (auto intro!: exI [of _ "(\<lambda>i. {})(0 := b)"]
```
```   460              simp: measure_set_def disjoint_family_on_def split_if_mem2 comp_def)
```
```   461 qed
```
```   462
```
```   463 lemma (in algebra) additive_increasing:
```
```   464   assumes posf: "positive f" and addf: "additive M f"
```
```   465   shows "increasing M f"
```
```   466 proof (auto simp add: increasing_def)
```
```   467   fix x y
```
```   468   assume xy: "x \<in> sets M" "y \<in> sets M" "x \<subseteq> y"
```
```   469   have "f x \<le> f x + f (y-x)" ..
```
```   470   also have "... = f (x \<union> (y-x))" using addf
```
```   471     by (auto simp add: additive_def) (metis Diff_disjoint Un_Diff_cancel Diff xy(1,2))
```
```   472   also have "... = f y"
```
```   473     by (metis Un_Diff_cancel Un_absorb1 xy(3))
```
```   474   finally show "f x \<le> f y" .
```
```   475 qed
```
```   476
```
```   477 lemma (in algebra) countably_additive_additive:
```
```   478   assumes posf: "positive f" and ca: "countably_additive M f"
```
```   479   shows "additive M f"
```
```   480 proof (auto simp add: additive_def)
```
```   481   fix x y
```
```   482   assume x: "x \<in> sets M" and y: "y \<in> sets M" and "x \<inter> y = {}"
```
```   483   hence "disjoint_family (binaryset x y)"
```
```   484     by (auto simp add: disjoint_family_on_def binaryset_def)
```
```   485   hence "range (binaryset x y) \<subseteq> sets M \<longrightarrow>
```
```   486          (\<Union>i. binaryset x y i) \<in> sets M \<longrightarrow>
```
```   487          f (\<Union>i. binaryset x y i) = (\<Sum>\<^isub>\<infinity> n. f (binaryset x y n))"
```
```   488     using ca
```
```   489     by (simp add: countably_additive_def)
```
```   490   hence "{x,y,{}} \<subseteq> sets M \<longrightarrow> x \<union> y \<in> sets M \<longrightarrow>
```
```   491          f (x \<union> y) = (\<Sum>\<^isub>\<infinity> n. f (binaryset x y n))"
```
```   492     by (simp add: range_binaryset_eq UN_binaryset_eq)
```
```   493   thus "f (x \<union> y) = f x + f y" using posf x y
```
```   494     by (auto simp add: Un binaryset_psuminf positive_def)
```
```   495 qed
```
```   496
```
```   497 lemma (in algebra) inf_measure_agrees:
```
```   498   assumes posf: "positive f" and ca: "countably_additive M f"
```
```   499       and s: "s \<in> sets M"
```
```   500   shows "Inf (measure_set M f s) = f s"
```
```   501   unfolding Inf_pinfreal_def
```
```   502 proof (safe intro!: Greatest_equality)
```
```   503   fix z
```
```   504   assume z: "z \<in> measure_set M f s"
```
```   505   from this obtain A where
```
```   506     A: "range A \<subseteq> sets M" and disj: "disjoint_family A"
```
```   507     and "s \<subseteq> (\<Union>x. A x)" and si: "psuminf (f \<circ> A) = z"
```
```   508     by (auto simp add: measure_set_def comp_def)
```
```   509   hence seq: "s = (\<Union>i. A i \<inter> s)" by blast
```
```   510   have inc: "increasing M f"
```
```   511     by (metis additive_increasing ca countably_additive_additive posf)
```
```   512   have sums: "psuminf (\<lambda>i. f (A i \<inter> s)) = f (\<Union>i. A i \<inter> s)"
```
```   513     proof (rule countably_additiveD [OF ca])
```
```   514       show "range (\<lambda>n. A n \<inter> s) \<subseteq> sets M" using A s
```
```   515         by blast
```
```   516       show "disjoint_family (\<lambda>n. A n \<inter> s)" using disj
```
```   517         by (auto simp add: disjoint_family_on_def)
```
```   518       show "(\<Union>i. A i \<inter> s) \<in> sets M" using A s
```
```   519         by (metis UN_extend_simps(4) s seq)
```
```   520     qed
```
```   521   hence "f s = psuminf (\<lambda>i. f (A i \<inter> s))"
```
```   522     using seq [symmetric] by (simp add: sums_iff)
```
```   523   also have "... \<le> psuminf (f \<circ> A)"
```
```   524     proof (rule psuminf_le)
```
```   525       fix n show "f (A n \<inter> s) \<le> (f \<circ> A) n" using A s
```
```   526         by (force intro: increasingD [OF inc])
```
```   527     qed
```
```   528   also have "... = z" by (rule si)
```
```   529   finally show "f s \<le> z" .
```
```   530 next
```
```   531   fix y
```
```   532   assume y: "\<forall>u \<in> measure_set M f s. y \<le> u"
```
```   533   thus "y \<le> f s"
```
```   534     by (blast intro: inf_measure_nonempty [of f, OF posf s subset_refl])
```
```   535 qed
```
```   536
```
```   537 lemma (in algebra) inf_measure_empty:
```
```   538   assumes posf: "positive f"
```
```   539   shows "Inf (measure_set M f {}) = 0"
```
```   540 proof (rule antisym)
```
```   541   show "Inf (measure_set M f {}) \<le> 0"
```
```   542     by (metis complete_lattice_class.Inf_lower empty_sets inf_measure_nonempty[OF posf] subset_refl posf[unfolded positive_def])
```
```   543 qed simp
```
```   544
```
```   545 lemma (in algebra) inf_measure_positive:
```
```   546   "positive f \<Longrightarrow>
```
```   547    positive (\<lambda>x. Inf (measure_set M f x))"
```
```   548   by (simp add: positive_def inf_measure_empty)
```
```   549
```
```   550 lemma (in algebra) inf_measure_increasing:
```
```   551   assumes posf: "positive f"
```
```   552   shows "increasing (| space = space M, sets = Pow (space M) |)
```
```   553                     (\<lambda>x. Inf (measure_set M f x))"
```
```   554 apply (auto simp add: increasing_def)
```
```   555 apply (rule complete_lattice_class.Inf_greatest)
```
```   556 apply (rule complete_lattice_class.Inf_lower)
```
```   557 apply (clarsimp simp add: measure_set_def, rule_tac x=A in exI, blast)
```
```   558 done
```
```   559
```
```   560
```
```   561 lemma (in algebra) inf_measure_le:
```
```   562   assumes posf: "positive f" and inc: "increasing M f"
```
```   563       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}"
```
```   564   shows "Inf (measure_set M f s) \<le> x"
```
```   565 proof -
```
```   566   from x
```
```   567   obtain A where A: "range A \<subseteq> sets M" and ss: "s \<subseteq> (\<Union>i. A i)"
```
```   568              and xeq: "psuminf (f \<circ> A) = x"
```
```   569     by auto
```
```   570   have dA: "range (disjointed A) \<subseteq> sets M"
```
```   571     by (metis A range_disjointed_sets)
```
```   572   have "\<forall>n.(f o disjointed A) n \<le> (f \<circ> A) n" unfolding comp_def
```
```   573     by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A comp_def)
```
```   574   hence sda: "psuminf (f o disjointed A) \<le> psuminf (f \<circ> A)"
```
```   575     by (blast intro: psuminf_le)
```
```   576   hence ley: "psuminf (f o disjointed A) \<le> x"
```
```   577     by (metis xeq)
```
```   578   hence y: "psuminf (f o disjointed A) \<in> measure_set M f s"
```
```   579     apply (auto simp add: measure_set_def)
```
```   580     apply (rule_tac x="disjointed A" in exI)
```
```   581     apply (simp add: disjoint_family_disjointed UN_disjointed_eq ss dA comp_def)
```
```   582     done
```
```   583   show ?thesis
```
```   584     by (blast intro: y order_trans [OF _ ley] posf complete_lattice_class.Inf_lower)
```
```   585 qed
```
```   586
```
```   587 lemma (in algebra) inf_measure_close:
```
```   588   assumes posf: "positive f" and e: "0 < e" and ss: "s \<subseteq> (space M)"
```
```   589   shows "\<exists>A. range A \<subseteq> sets M \<and> disjoint_family A \<and> s \<subseteq> (\<Union>i. A i) \<and>
```
```   590                psuminf (f \<circ> A) \<le> Inf (measure_set M f s) + e"
```
```   591 proof (cases "Inf (measure_set M f s) = \<omega>")
```
```   592   case False
```
```   593   obtain l where "l \<in> measure_set M f s" "l \<le> Inf (measure_set M f s) + e"
```
```   594     using Inf_close[OF False e] by auto
```
```   595   thus ?thesis
```
```   596     by (auto intro!: exI[of _ l] simp: measure_set_def comp_def)
```
```   597 next
```
```   598   case True
```
```   599   have "measure_set M f s \<noteq> {}"
```
```   600     by (metis emptyE ss inf_measure_nonempty [of f, OF posf top])
```
```   601   then obtain l where "l \<in> measure_set M f s" by auto
```
```   602   moreover from True have "l \<le> Inf (measure_set M f s) + e" by simp
```
```   603   ultimately show ?thesis
```
```   604     by (auto intro!: exI[of _ l] simp: measure_set_def comp_def)
```
```   605 qed
```
```   606
```
```   607 lemma (in algebra) inf_measure_countably_subadditive:
```
```   608   assumes posf: "positive f" and inc: "increasing M f"
```
```   609   shows "countably_subadditive (| space = space M, sets = Pow (space M) |)
```
```   610                   (\<lambda>x. Inf (measure_set M f x))"
```
```   611   unfolding countably_subadditive_def o_def
```
```   612 proof (safe, simp, rule pinfreal_le_epsilon)
```
```   613   fix A :: "nat \<Rightarrow> 'a set" and e :: pinfreal
```
```   614
```
```   615   let "?outer n" = "Inf (measure_set M f (A n))"
```
```   616   assume A: "range A \<subseteq> Pow (space M)"
```
```   617      and disj: "disjoint_family A"
```
```   618      and sb: "(\<Union>i. A i) \<subseteq> space M"
```
```   619      and e: "0 < e"
```
```   620   hence "\<exists>BB. \<forall>n. range (BB n) \<subseteq> sets M \<and> disjoint_family (BB n) \<and>
```
```   621                    A n \<subseteq> (\<Union>i. BB n i) \<and>
```
```   622                    psuminf (f o BB n) \<le> ?outer n + e * (1/2)^(Suc n)"
```
```   623     apply (safe intro!: choice inf_measure_close [of f, OF posf _])
```
```   624     using e sb by (cases e, auto simp add: not_le mult_pos_pos)
```
```   625   then obtain BB
```
```   626     where BB: "\<And>n. (range (BB n) \<subseteq> sets M)"
```
```   627       and disjBB: "\<And>n. disjoint_family (BB n)"
```
```   628       and sbBB: "\<And>n. A n \<subseteq> (\<Union>i. BB n i)"
```
```   629       and BBle: "\<And>n. psuminf (f o BB n) \<le> ?outer n + e * (1/2)^(Suc n)"
```
```   630     by auto blast
```
```   631   have sll: "(\<Sum>\<^isub>\<infinity> n. psuminf (f o BB n)) \<le> psuminf ?outer + e"
```
```   632     proof -
```
```   633       have "(\<Sum>\<^isub>\<infinity> n. psuminf (f o BB n)) \<le> (\<Sum>\<^isub>\<infinity> n. ?outer n + e*(1/2) ^ Suc n)"
```
```   634         by (rule psuminf_le[OF BBle])
```
```   635       also have "... = psuminf ?outer + e"
```
```   636         using psuminf_half_series by simp
```
```   637       finally show ?thesis .
```
```   638     qed
```
```   639   def C \<equiv> "(split BB) o prod_decode"
```
```   640   have C: "!!n. C n \<in> sets M"
```
```   641     apply (rule_tac p="prod_decode n" in PairE)
```
```   642     apply (simp add: C_def)
```
```   643     apply (metis BB subsetD rangeI)
```
```   644     done
```
```   645   have sbC: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)"
```
```   646     proof (auto simp add: C_def)
```
```   647       fix x i
```
```   648       assume x: "x \<in> A i"
```
```   649       with sbBB [of i] obtain j where "x \<in> BB i j"
```
```   650         by blast
```
```   651       thus "\<exists>i. x \<in> split BB (prod_decode i)"
```
```   652         by (metis prod_encode_inverse prod.cases)
```
```   653     qed
```
```   654   have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> prod_decode"
```
```   655     by (rule ext)  (auto simp add: C_def)
```
```   656   moreover have "psuminf ... = (\<Sum>\<^isub>\<infinity> n. psuminf (f o BB n))" using BBle
```
```   657     by (force intro!: psuminf_2dimen simp: o_def)
```
```   658   ultimately have Csums: "psuminf (f \<circ> C) = (\<Sum>\<^isub>\<infinity> n. psuminf (f o BB n))" by simp
```
```   659   have "Inf (measure_set M f (\<Union>i. A i)) \<le> (\<Sum>\<^isub>\<infinity> n. psuminf (f o BB n))"
```
```   660     apply (rule inf_measure_le [OF posf(1) inc], auto)
```
```   661     apply (rule_tac x="C" in exI)
```
```   662     apply (auto simp add: C sbC Csums)
```
```   663     done
```
```   664   also have "... \<le> (\<Sum>\<^isub>\<infinity>n. Inf (measure_set M f (A n))) + e" using sll
```
```   665     by blast
```
```   666   finally show "Inf (measure_set M f (\<Union>i. A i)) \<le> psuminf ?outer + e" .
```
```   667 qed
```
```   668
```
```   669 lemma (in algebra) inf_measure_outer:
```
```   670   "\<lbrakk> positive f ; increasing M f \<rbrakk>
```
```   671    \<Longrightarrow> outer_measure_space (| space = space M, sets = Pow (space M) |)
```
```   672                           (\<lambda>x. Inf (measure_set M f x))"
```
```   673   by (simp add: outer_measure_space_def inf_measure_empty
```
```   674                 inf_measure_increasing inf_measure_countably_subadditive positive_def)
```
```   675
```
```   676 (*MOVE UP*)
```
```   677
```
```   678 lemma (in algebra) algebra_subset_lambda_system:
```
```   679   assumes posf: "positive f" and inc: "increasing M f"
```
```   680       and add: "additive M f"
```
```   681   shows "sets M \<subseteq> lambda_system (| space = space M, sets = Pow (space M) |)
```
```   682                                 (\<lambda>x. Inf (measure_set M f x))"
```
```   683 proof (auto dest: sets_into_space
```
```   684             simp add: algebra.lambda_system_eq [OF algebra_Pow])
```
```   685   fix x s
```
```   686   assume x: "x \<in> sets M"
```
```   687      and s: "s \<subseteq> space M"
```
```   688   have [simp]: "!!x. x \<in> sets M \<Longrightarrow> s \<inter> (space M - x) = s-x" using s
```
```   689     by blast
```
```   690   have "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
```
```   691         \<le> Inf (measure_set M f s)"
```
```   692     proof (rule pinfreal_le_epsilon)
```
```   693       fix e :: pinfreal
```
```   694       assume e: "0 < e"
```
```   695       from inf_measure_close [of f, OF posf e s]
```
```   696       obtain A where A: "range A \<subseteq> sets M" and disj: "disjoint_family A"
```
```   697                  and sUN: "s \<subseteq> (\<Union>i. A i)"
```
```   698                  and l: "psuminf (f \<circ> A) \<le> Inf (measure_set M f s) + e"
```
```   699         by auto
```
```   700       have [simp]: "!!x. x \<in> sets M \<Longrightarrow>
```
```   701                       (f o (\<lambda>z. z \<inter> (space M - x)) o A) = (f o (\<lambda>z. z - x) o A)"
```
```   702         by (rule ext, simp, metis A Int_Diff Int_space_eq2 range_subsetD)
```
```   703       have  [simp]: "!!n. f (A n \<inter> x) + f (A n - x) = f (A n)"
```
```   704         by (subst additiveD [OF add, symmetric])
```
```   705            (auto simp add: x range_subsetD [OF A] Int_Diff_Un Int_Diff_disjoint)
```
```   706       { fix u
```
```   707         assume u: "u \<in> sets M"
```
```   708         have [simp]: "\<And>n. f (A n \<inter> u) \<le> f (A n)"
```
```   709           by (simp add: increasingD [OF inc] u Int range_subsetD [OF A])
```
```   710         have 2: "Inf (measure_set M f (s \<inter> u)) \<le> psuminf (f \<circ> (\<lambda>z. z \<inter> u) \<circ> A)"
```
```   711           proof (rule complete_lattice_class.Inf_lower)
```
```   712             show "psuminf (f \<circ> (\<lambda>z. z \<inter> u) \<circ> A) \<in> measure_set M f (s \<inter> u)"
```
```   713               apply (simp add: measure_set_def)
```
```   714               apply (rule_tac x="(\<lambda>z. z \<inter> u) o A" in exI)
```
```   715               apply (auto simp add: disjoint_family_subset [OF disj] o_def)
```
```   716               apply (blast intro: u range_subsetD [OF A])
```
```   717               apply (blast dest: subsetD [OF sUN])
```
```   718               done
```
```   719           qed
```
```   720       } note lesum = this
```
```   721       have inf1: "Inf (measure_set M f (s\<inter>x)) \<le> psuminf (f o (\<lambda>z. z\<inter>x) o A)"
```
```   722         and inf2: "Inf (measure_set M f (s \<inter> (space M - x)))
```
```   723                    \<le> psuminf (f o (\<lambda>z. z \<inter> (space M - x)) o A)"
```
```   724         by (metis Diff lesum top x)+
```
```   725       hence "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
```
```   726            \<le> psuminf (f o (\<lambda>s. s\<inter>x) o A) + psuminf (f o (\<lambda>s. s-x) o A)"
```
```   727         by (simp add: x add_mono)
```
```   728       also have "... \<le> psuminf (f o A)"
```
```   729         by (simp add: x psuminf_add[symmetric] o_def)
```
```   730       also have "... \<le> Inf (measure_set M f s) + e"
```
```   731         by (rule l)
```
```   732       finally show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
```
```   733         \<le> Inf (measure_set M f s) + e" .
```
```   734     qed
```
```   735   moreover
```
```   736   have "Inf (measure_set M f s)
```
```   737        \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))"
```
```   738     proof -
```
```   739     have "Inf (measure_set M f s) = Inf (measure_set M f ((s\<inter>x) \<union> (s-x)))"
```
```   740       by (metis Un_Diff_Int Un_commute)
```
```   741     also have "... \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))"
```
```   742       apply (rule subadditiveD)
```
```   743       apply (iprover intro: algebra.countably_subadditive_subadditive algebra_Pow
```
```   744                inf_measure_positive inf_measure_countably_subadditive posf inc)
```
```   745       apply (auto simp add: subsetD [OF s])
```
```   746       done
```
```   747     finally show ?thesis .
```
```   748     qed
```
```   749   ultimately
```
```   750   show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
```
```   751         = Inf (measure_set M f s)"
```
```   752     by (rule order_antisym)
```
```   753 qed
```
```   754
```
```   755 lemma measure_down:
```
```   756      "measure_space N \<mu> \<Longrightarrow> sigma_algebra M \<Longrightarrow> sets M \<subseteq> sets N \<Longrightarrow>
```
```   757       (\<nu> = \<mu>) \<Longrightarrow> measure_space M \<nu>"
```
```   758   by (simp add: measure_space_def measure_space_axioms_def positive_def
```
```   759                 countably_additive_def)
```
```   760      blast
```
```   761
```
```   762 theorem (in algebra) caratheodory:
```
```   763   assumes posf: "positive f" and ca: "countably_additive M f"
```
```   764   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>"
```
```   765   proof -
```
```   766     have inc: "increasing M f"
```
```   767       by (metis additive_increasing ca countably_additive_additive posf)
```
```   768     let ?infm = "(\<lambda>x. Inf (measure_set M f x))"
```
```   769     def ls \<equiv> "lambda_system (|space = space M, sets = Pow (space M)|) ?infm"
```
```   770     have mls: "measure_space \<lparr>space = space M, sets = ls\<rparr> ?infm"
```
```   771       using sigma_algebra.caratheodory_lemma
```
```   772               [OF sigma_algebra_Pow  inf_measure_outer [OF posf inc]]
```
```   773       by (simp add: ls_def)
```
```   774     hence sls: "sigma_algebra (|space = space M, sets = ls|)"
```
```   775       by (simp add: measure_space_def)
```
```   776     have "sets M \<subseteq> ls"
```
```   777       by (simp add: ls_def)
```
```   778          (metis ca posf inc countably_additive_additive algebra_subset_lambda_system)
```
```   779     hence sgs_sb: "sigma_sets (space M) (sets M) \<subseteq> ls"
```
```   780       using sigma_algebra.sigma_sets_subset [OF sls, of "sets M"]
```
```   781       by simp
```
```   782     have "measure_space (sigma (space M) (sets M)) ?infm"
```
```   783       unfolding sigma_def
```
```   784       by (rule measure_down [OF mls], rule sigma_algebra_sigma_sets)
```
```   785          (simp_all add: sgs_sb space_closed)
```
```   786     thus ?thesis using inf_measure_agrees [OF posf ca] by (auto intro!: exI[of _ ?infm])
```
```   787   qed
```
```   788
```
```   789 end
```