author haftmann
Tue Oct 13 09:21:15 2015 +0200 (2015-10-13)
changeset 61424 c3658c18b7bc
parent 61273 542a4d9bac96
child 61427 3c69ea85f8dd
permissions -rw-r--r--
prod_case as canonical name for product type eliminator
     1 (*  Title:      HOL/Probability/Caratheodory.thy
     2     Author:     Lawrence C Paulson
     3     Author:     Johannes Hölzl, TU München
     4 *)
     6 section {*Caratheodory Extension Theorem*}
     8 theory Caratheodory
     9   imports Measure_Space
    10 begin
    12 text {*
    13   Originally from the Hurd/Coble measure theory development, translated by Lawrence Paulson.
    14 *}
    16 lemma suminf_ereal_2dimen:
    17   fixes f:: "nat \<times> nat \<Rightarrow> ereal"
    18   assumes pos: "\<And>p. 0 \<le> f p"
    19   assumes "\<And>m. g m = (\<Sum>n. f (m,n))"
    20   shows "(\<Sum>i. f (prod_decode i)) = suminf g"
    21 proof -
    22   have g_def: "g = (\<lambda>m. (\<Sum>n. f (m,n)))"
    23     using assms by (simp add: fun_eq_iff)
    24   have reindex: "\<And>B. (\<Sum>x\<in>B. f (prod_decode x)) = setsum f (prod_decode ` B)"
    25     by (simp add: setsum.reindex[OF inj_prod_decode] comp_def)
    26   { fix n
    27     let ?M = "\<lambda>f. Suc (Max (f ` prod_decode ` {..<n}))"
    28     { fix a b x assume "x < n" and [symmetric]: "(a, b) = prod_decode x"
    29       then have "a < ?M fst" "b < ?M snd"
    30         by (auto intro!: Max_ge le_imp_less_Suc image_eqI) }
    31     then have "setsum f (prod_decode ` {..<n}) \<le> setsum f ({..<?M fst} \<times> {..<?M snd})"
    32       by (auto intro!: setsum_mono3 simp: pos)
    33     then have "\<exists>a b. setsum f (prod_decode ` {..<n}) \<le> setsum f ({..<a} \<times> {..<b})" by auto }
    34   moreover
    35   { fix a b
    36     let ?M = "prod_decode ` {..<Suc (Max (prod_encode ` ({..<a} \<times> {..<b})))}"
    37     { fix a' b' assume "a' < a" "b' < b" then have "(a', b') \<in> ?M"
    38         by (auto intro!: Max_ge le_imp_less_Suc image_eqI[where x="prod_encode (a', b')"]) }
    39     then have "setsum f ({..<a} \<times> {..<b}) \<le> setsum f ?M"
    40       by (auto intro!: setsum_mono3 simp: pos) }
    41   ultimately
    42   show ?thesis unfolding g_def using pos
    43     by (auto intro!: SUP_eq  simp: setsum.cartesian_product reindex SUP_upper2
    44                      suminf_ereal_eq_SUP SUP_pair
    45                      SUP_ereal_setsum[symmetric] incseq_setsumI setsum_nonneg)
    46 qed
    48 subsection {* Characterizations of Measures *}
    50 definition subadditive where
    51   "subadditive M f \<longleftrightarrow> (\<forall>x\<in>M. \<forall>y\<in>M. x \<inter> y = {} \<longrightarrow> f (x \<union> y) \<le> f x + f y)"
    53 definition countably_subadditive where
    54   "countably_subadditive M f \<longleftrightarrow>
    55     (\<forall>A. range A \<subseteq> M \<longrightarrow> disjoint_family A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow> (f (\<Union>i. A i) \<le> (\<Sum>i. f (A i))))"
    57 definition outer_measure_space where
    58   "outer_measure_space M f \<longleftrightarrow> positive M f \<and> increasing M f \<and> countably_subadditive M f"
    60 lemma subadditiveD: "subadditive M f \<Longrightarrow> x \<inter> y = {} \<Longrightarrow> x \<in> M \<Longrightarrow> y \<in> M \<Longrightarrow> f (x \<union> y) \<le> f x + f y"
    61   by (auto simp add: subadditive_def)
    63 subsubsection {* Lambda Systems *}
    65 definition lambda_system where
    66   "lambda_system \<Omega> M f = {l \<in> M. \<forall>x \<in> M. f (l \<inter> x) + f ((\<Omega> - l) \<inter> x) = f x}"
    68 lemma (in algebra) lambda_system_eq:
    69   "lambda_system \<Omega> M f = {l \<in> M. \<forall>x \<in> M. f (x \<inter> l) + f (x - l) = f x}"
    70 proof -
    71   have [simp]: "\<And>l x. l \<in> M \<Longrightarrow> x \<in> M \<Longrightarrow> (\<Omega> - l) \<inter> x = x - l"
    72     by (metis Int_Diff Int_absorb1 Int_commute sets_into_space)
    73   show ?thesis
    74     by (auto simp add: lambda_system_def) (metis Int_commute)+
    75 qed
    77 lemma (in algebra) lambda_system_empty: "positive M f \<Longrightarrow> {} \<in> lambda_system \<Omega> M f"
    78   by (auto simp add: positive_def lambda_system_eq)
    80 lemma lambda_system_sets: "x \<in> lambda_system \<Omega> M f \<Longrightarrow> x \<in> M"
    81   by (simp add: lambda_system_def)
    83 lemma (in algebra) lambda_system_Compl:
    84   fixes f:: "'a set \<Rightarrow> ereal"
    85   assumes x: "x \<in> lambda_system \<Omega> M f"
    86   shows "\<Omega> - x \<in> lambda_system \<Omega> M f"
    87 proof -
    88   have "x \<subseteq> \<Omega>"
    89     by (metis sets_into_space lambda_system_sets x)
    90   hence "\<Omega> - (\<Omega> - x) = x"
    91     by (metis double_diff equalityE)
    92   with x show ?thesis
    93     by (force simp add: lambda_system_def ac_simps)
    94 qed
    96 lemma (in algebra) lambda_system_Int:
    97   fixes f:: "'a set \<Rightarrow> ereal"
    98   assumes xl: "x \<in> lambda_system \<Omega> M f" and yl: "y \<in> lambda_system \<Omega> M f"
    99   shows "x \<inter> y \<in> lambda_system \<Omega> M f"
   100 proof -
   101   from xl yl show ?thesis
   102   proof (auto simp add: positive_def lambda_system_eq Int)
   103     fix u
   104     assume x: "x \<in> M" and y: "y \<in> M" and u: "u \<in> M"
   105        and fx: "\<forall>z\<in>M. f (z \<inter> x) + f (z - x) = f z"
   106        and fy: "\<forall>z\<in>M. f (z \<inter> y) + f (z - y) = f z"
   107     have "u - x \<inter> y \<in> M"
   108       by (metis Diff Diff_Int Un u x y)
   109     moreover
   110     have "(u - (x \<inter> y)) \<inter> y = u \<inter> y - x" by blast
   111     moreover
   112     have "u - x \<inter> y - y = u - y" by blast
   113     ultimately
   114     have ey: "f (u - x \<inter> y) = f (u \<inter> y - x) + f (u - y)" using fy
   115       by force
   116     have "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y)
   117           = (f (u \<inter> (x \<inter> y)) + f (u \<inter> y - x)) + f (u - y)"
   118       by (simp add: ey ac_simps)
   119     also have "... =  (f ((u \<inter> y) \<inter> x) + f (u \<inter> y - x)) + f (u - y)"
   120       by (simp add: Int_ac)
   121     also have "... = f (u \<inter> y) + f (u - y)"
   122       using fx [THEN bspec, of "u \<inter> y"] Int y u
   123       by force
   124     also have "... = f u"
   125       by (metis fy u)
   126     finally show "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y) = f u" .
   127   qed
   128 qed
   130 lemma (in algebra) lambda_system_Un:
   131   fixes f:: "'a set \<Rightarrow> ereal"
   132   assumes xl: "x \<in> lambda_system \<Omega> M f" and yl: "y \<in> lambda_system \<Omega> M f"
   133   shows "x \<union> y \<in> lambda_system \<Omega> M f"
   134 proof -
   135   have "(\<Omega> - x) \<inter> (\<Omega> - y) \<in> M"
   136     by (metis Diff_Un Un compl_sets lambda_system_sets xl yl)
   137   moreover
   138   have "x \<union> y = \<Omega> - ((\<Omega> - x) \<inter> (\<Omega> - y))"
   139     by auto (metis subsetD lambda_system_sets sets_into_space xl yl)+
   140   ultimately show ?thesis
   141     by (metis lambda_system_Compl lambda_system_Int xl yl)
   142 qed
   144 lemma (in algebra) lambda_system_algebra:
   145   "positive M f \<Longrightarrow> algebra \<Omega> (lambda_system \<Omega> M f)"
   146   apply (auto simp add: algebra_iff_Un)
   147   apply (metis lambda_system_sets set_mp sets_into_space)
   148   apply (metis lambda_system_empty)
   149   apply (metis lambda_system_Compl)
   150   apply (metis lambda_system_Un)
   151   done
   153 lemma (in algebra) lambda_system_strong_additive:
   154   assumes z: "z \<in> M" and disj: "x \<inter> y = {}"
   155       and xl: "x \<in> lambda_system \<Omega> M f" and yl: "y \<in> lambda_system \<Omega> M f"
   156   shows "f (z \<inter> (x \<union> y)) = f (z \<inter> x) + f (z \<inter> y)"
   157 proof -
   158   have "z \<inter> x = (z \<inter> (x \<union> y)) \<inter> x" using disj by blast
   159   moreover
   160   have "z \<inter> y = (z \<inter> (x \<union> y)) - x" using disj by blast
   161   moreover
   162   have "(z \<inter> (x \<union> y)) \<in> M"
   163     by (metis Int Un lambda_system_sets xl yl z)
   164   ultimately show ?thesis using xl yl
   165     by (simp add: lambda_system_eq)
   166 qed
   168 lemma (in algebra) lambda_system_additive: "additive (lambda_system \<Omega> M f) f"
   169 proof (auto simp add: additive_def)
   170   fix x and y
   171   assume disj: "x \<inter> y = {}"
   172      and xl: "x \<in> lambda_system \<Omega> M f" and yl: "y \<in> lambda_system \<Omega> M f"
   173   hence  "x \<in> M" "y \<in> M" by (blast intro: lambda_system_sets)+
   174   thus "f (x \<union> y) = f x + f y"
   175     using lambda_system_strong_additive [OF top disj xl yl]
   176     by (simp add: Un)
   177 qed
   179 lemma (in ring_of_sets) countably_subadditive_subadditive:
   180   assumes f: "positive M f" and cs: "countably_subadditive M f"
   181   shows  "subadditive M f"
   182 proof (auto simp add: subadditive_def)
   183   fix x y
   184   assume x: "x \<in> M" and y: "y \<in> M" and "x \<inter> y = {}"
   185   hence "disjoint_family (binaryset x y)"
   186     by (auto simp add: disjoint_family_on_def binaryset_def)
   187   hence "range (binaryset x y) \<subseteq> M \<longrightarrow>
   188          (\<Union>i. binaryset x y i) \<in> M \<longrightarrow>
   189          f (\<Union>i. binaryset x y i) \<le> (\<Sum> n. f (binaryset x y n))"
   190     using cs by (auto simp add: countably_subadditive_def)
   191   hence "{x,y,{}} \<subseteq> M \<longrightarrow> x \<union> y \<in> M \<longrightarrow>
   192          f (x \<union> y) \<le> (\<Sum> n. f (binaryset x y n))"
   193     by (simp add: range_binaryset_eq UN_binaryset_eq)
   194   thus "f (x \<union> y) \<le>  f x + f y" using f x y
   195     by (auto simp add: Un o_def suminf_binaryset_eq positive_def)
   196 qed
   198 lemma lambda_system_increasing: "increasing M f \<Longrightarrow> increasing (lambda_system \<Omega> M f) f"
   199   by (simp add: increasing_def lambda_system_def)
   201 lemma lambda_system_positive: "positive M f \<Longrightarrow> positive (lambda_system \<Omega> M f) f"
   202   by (simp add: positive_def lambda_system_def)
   204 lemma (in algebra) lambda_system_strong_sum:
   205   fixes A:: "nat \<Rightarrow> 'a set" and f :: "'a set \<Rightarrow> ereal"
   206   assumes f: "positive M f" and a: "a \<in> M"
   207       and A: "range A \<subseteq> lambda_system \<Omega> M f"
   208       and disj: "disjoint_family A"
   209   shows  "(\<Sum>i = 0..<n. f (a \<inter>A i)) = f (a \<inter> (\<Union>i\<in>{0..<n}. A i))"
   210 proof (induct n)
   211   case 0 show ?case using f by (simp add: positive_def)
   212 next
   213   case (Suc n)
   214   have 2: "A n \<inter> UNION {0..<n} A = {}" using disj
   215     by (force simp add: disjoint_family_on_def neq_iff)
   216   have 3: "A n \<in> lambda_system \<Omega> M f" using A
   217     by blast
   218   interpret l: algebra \<Omega> "lambda_system \<Omega> M f"
   219     using f by (rule lambda_system_algebra)
   220   have 4: "UNION {0..<n} A \<in> lambda_system \<Omega> M f"
   221     using A l.UNION_in_sets by simp
   222   from Suc.hyps show ?case
   223     by (simp add: atLeastLessThanSuc lambda_system_strong_additive [OF a 2 3 4])
   224 qed
   226 lemma (in sigma_algebra) lambda_system_caratheodory:
   227   assumes oms: "outer_measure_space M f"
   228       and A: "range A \<subseteq> lambda_system \<Omega> M f"
   229       and disj: "disjoint_family A"
   230   shows  "(\<Union>i. A i) \<in> lambda_system \<Omega> M f \<and> (\<Sum>i. f (A i)) = f (\<Union>i. A i)"
   231 proof -
   232   have pos: "positive M f" and inc: "increasing M f"
   233    and csa: "countably_subadditive M f"
   234     by (metis oms outer_measure_space_def)+
   235   have sa: "subadditive M f"
   236     by (metis countably_subadditive_subadditive csa pos)
   237   have A': "\<And>S. A`S \<subseteq> (lambda_system \<Omega> M f)" using A
   238     by auto
   239   interpret ls: algebra \<Omega> "lambda_system \<Omega> M f"
   240     using pos by (rule lambda_system_algebra)
   241   have A'': "range A \<subseteq> M"
   242      by (metis A image_subset_iff lambda_system_sets)
   244   have U_in: "(\<Union>i. A i) \<in> M"
   245     by (metis A'' countable_UN)
   246   have U_eq: "f (\<Union>i. A i) = (\<Sum>i. f (A i))"
   247   proof (rule antisym)
   248     show "f (\<Union>i. A i) \<le> (\<Sum>i. f (A i))"
   249       using csa[unfolded countably_subadditive_def] A'' disj U_in by auto
   250     have *: "\<And>i. 0 \<le> f (A i)" using pos A'' unfolding positive_def by auto
   251     have dis: "\<And>N. disjoint_family_on A {..<N}" by (intro disjoint_family_on_mono[OF _ disj]) auto
   252     show "(\<Sum>i. f (A i)) \<le> f (\<Union>i. A i)"
   253       using ls.additive_sum [OF lambda_system_positive[OF pos] lambda_system_additive _ A' dis] A''
   254       by (intro suminf_bound[OF _ *]) (auto intro!: increasingD[OF inc] countable_UN)
   255   qed
   256   have "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) = f a"
   257     if a [iff]: "a \<in> M" for a
   258   proof (rule antisym)
   259     have "range (\<lambda>i. a \<inter> A i) \<subseteq> M" using A''
   260       by blast
   261     moreover
   262     have "disjoint_family (\<lambda>i. a \<inter> A i)" using disj
   263       by (auto simp add: disjoint_family_on_def)
   264     moreover
   265     have "a \<inter> (\<Union>i. A i) \<in> M"
   266       by (metis Int U_in a)
   267     ultimately
   268     have "f (a \<inter> (\<Union>i. A i)) \<le> (\<Sum>i. f (a \<inter> A i))"
   269       using csa[unfolded countably_subadditive_def, rule_format, of "(\<lambda>i. a \<inter> A i)"]
   270       by (simp add: o_def)
   271     hence "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le> (\<Sum>i. f (a \<inter> A i)) + f (a - (\<Union>i. A i))"
   272       by (rule add_right_mono)
   273     also have "\<dots> \<le> f a"
   274     proof (intro suminf_bound_add allI)
   275       fix n
   276       have UNION_in: "(\<Union>i\<in>{0..<n}. A i) \<in> M"
   277         by (metis A'' UNION_in_sets)
   278       have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A''
   279         by (blast intro: increasingD [OF inc] A'' UNION_in_sets)
   280       have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system \<Omega> M f"
   281         using ls.UNION_in_sets by (simp add: A)
   282       hence eq_fa: "f a = f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i))"
   283         by (simp add: lambda_system_eq UNION_in)
   284       have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))"
   285         by (blast intro: increasingD [OF inc] UNION_in U_in)
   286       thus "(\<Sum>i<n. f (a \<inter> A i)) + f (a - (\<Union>i. A i)) \<le> f a"
   287         by (simp add: lambda_system_strong_sum pos A disj eq_fa add_left_mono atLeast0LessThan[symmetric])
   288     next
   289       have "\<And>i. a \<inter> A i \<in> M" using A'' by auto
   290       then show "\<And>i. 0 \<le> f (a \<inter> A i)" using pos[unfolded positive_def] by auto
   291       have "\<And>i. a - (\<Union>i. A i) \<in> M" using A'' by auto
   292       then have "\<And>i. 0 \<le> f (a - (\<Union>i. A i))" using pos[unfolded positive_def] by auto
   293       then show "f (a - (\<Union>i. A i)) \<noteq> -\<infinity>" by auto
   294     qed
   295     finally show "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le> f a" .
   296   next
   297     have "f a \<le> f (a \<inter> (\<Union>i. A i) \<union> (a - (\<Union>i. A i)))"
   298       by (blast intro:  increasingD [OF inc] U_in)
   299     also have "... \<le>  f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))"
   300       by (blast intro: subadditiveD [OF sa] U_in)
   301     finally show "f a \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))" .
   302   qed
   303   thus  ?thesis
   304     by (simp add: lambda_system_eq sums_iff U_eq U_in)
   305 qed
   307 lemma (in sigma_algebra) caratheodory_lemma:
   308   assumes oms: "outer_measure_space M f"
   309   defines "L \<equiv> lambda_system \<Omega> M f"
   310   shows "measure_space \<Omega> L f"
   311 proof -
   312   have pos: "positive M f"
   313     by (metis oms outer_measure_space_def)
   314   have alg: "algebra \<Omega> L"
   315     using lambda_system_algebra [of f, OF pos]
   316     by (simp add: algebra_iff_Un L_def)
   317   then
   318   have "sigma_algebra \<Omega> L"
   319     using lambda_system_caratheodory [OF oms]
   320     by (simp add: sigma_algebra_disjoint_iff L_def)
   321   moreover
   322   have "countably_additive L f" "positive L f"
   323     using pos lambda_system_caratheodory [OF oms]
   324     by (auto simp add: lambda_system_sets L_def countably_additive_def positive_def)
   325   ultimately
   326   show ?thesis
   327     using pos by (simp add: measure_space_def)
   328 qed
   330 definition outer_measure :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> 'a set \<Rightarrow> ereal" where
   331    "outer_measure M f X =
   332      (INF A:{A. range A \<subseteq> M \<and> disjoint_family A \<and> X \<subseteq> (\<Union>i. A i)}. \<Sum>i. f (A i))"
   334 lemma (in ring_of_sets) outer_measure_agrees:
   335   assumes posf: "positive M f" and ca: "countably_additive M f" and s: "s \<in> M"
   336   shows "outer_measure M f s = f s"
   337   unfolding outer_measure_def
   338 proof (safe intro!: antisym INF_greatest)
   339   fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> M" and dA: "disjoint_family A" and sA: "s \<subseteq> (\<Union>x. A x)"
   340   have inc: "increasing M f"
   341     by (metis additive_increasing ca countably_additive_additive posf)
   342   have "f s = f (\<Union>i. A i \<inter> s)"
   343     using sA by (auto simp: Int_absorb1)
   344   also have "\<dots> = (\<Sum>i. f (A i \<inter> s))"
   345     using sA dA A s
   346     by (intro ca[unfolded countably_additive_def, rule_format, symmetric])
   347        (auto simp: Int_absorb1 disjoint_family_on_def)
   348   also have "... \<le> (\<Sum>i. f (A i))"
   349     using A s by (intro suminf_le_pos increasingD[OF inc] positiveD2[OF posf]) auto
   350   finally show "f s \<le> (\<Sum>i. f (A i))" .
   351 next
   352   have "(\<Sum>i. f (if i = 0 then s else {})) \<le> f s"
   353     using positiveD1[OF posf] by (subst suminf_finite[of "{0}"]) auto
   354   with s show "(INF A:{A. range A \<subseteq> M \<and> disjoint_family A \<and> s \<subseteq> UNION UNIV A}. \<Sum>i. f (A i)) \<le> f s"
   355     by (intro INF_lower2[of "\<lambda>i. if i = 0 then s else {}"])
   356        (auto simp: disjoint_family_on_def)
   357 qed
   359 lemma outer_measure_nonneg: "positive M f \<Longrightarrow> 0 \<le> outer_measure M f X"
   360   by (auto intro!: INF_greatest suminf_0_le intro: positiveD2 simp: outer_measure_def)
   362 lemma outer_measure_empty:
   363   assumes posf: "positive M f" and "{} \<in> M"
   364   shows "outer_measure M f {} = 0"
   365 proof (rule antisym)
   366   show "outer_measure M f {} \<le> 0"
   367     using assms by (auto intro!: INF_lower2[of "\<lambda>_. {}"] simp: outer_measure_def disjoint_family_on_def positive_def)
   368 qed (intro outer_measure_nonneg posf)
   370 lemma (in ring_of_sets) positive_outer_measure:
   371   assumes "positive M f" shows "positive (Pow \<Omega>) (outer_measure M f)"
   372   unfolding positive_def by (auto simp: assms outer_measure_empty outer_measure_nonneg)
   374 lemma (in ring_of_sets) increasing_outer_measure: "increasing (Pow \<Omega>) (outer_measure M f)"
   375   by (force simp: increasing_def outer_measure_def intro!: INF_greatest intro: INF_lower)
   377 lemma (in ring_of_sets) outer_measure_le:
   378   assumes pos: "positive M f" and inc: "increasing M f" and A: "range A \<subseteq> M" and X: "X \<subseteq> (\<Union>i. A i)"
   379   shows "outer_measure M f X \<le> (\<Sum>i. f (A i))"
   380   unfolding outer_measure_def
   381 proof (safe intro!: INF_lower2[of "disjointed A"] del: subsetI)
   382   show dA: "range (disjointed A) \<subseteq> M"
   383     by (auto intro!: A range_disjointed_sets)
   384   have "\<forall>n. f (disjointed A n) \<le> f (A n)"
   385     by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A)
   386   moreover have "\<forall>i. 0 \<le> f (disjointed A i)"
   387     using pos dA unfolding positive_def by auto
   388   ultimately show "(\<Sum>i. f (disjointed A i)) \<le> (\<Sum>i. f (A i))"
   389     by (blast intro!: suminf_le_pos)
   390 qed (auto simp: X UN_disjointed_eq disjoint_family_disjointed)
   392 lemma (in ring_of_sets) outer_measure_close:
   393   assumes posf: "positive M f" and "0 < e" and "outer_measure M f X \<noteq> \<infinity>"
   394   shows "\<exists>A. range A \<subseteq> M \<and> disjoint_family A \<and> X \<subseteq> (\<Union>i. A i) \<and> (\<Sum>i. f (A i)) \<le> outer_measure M f X + e"
   395 proof -
   396   from `outer_measure M f X \<noteq> \<infinity>` have fin: "\<bar>outer_measure M f X\<bar> \<noteq> \<infinity>"
   397     using outer_measure_nonneg[OF posf, of X] by auto
   398   show ?thesis
   399     using Inf_ereal_close[OF fin[unfolded outer_measure_def INF_def], OF \<open>0 < e\<close>]
   400     unfolding INF_def[symmetric] outer_measure_def[symmetric] by (auto intro: less_imp_le)
   401 qed
   403 lemma (in ring_of_sets) countably_subadditive_outer_measure:
   404   assumes posf: "positive M f" and inc: "increasing M f"
   405   shows "countably_subadditive (Pow \<Omega>) (outer_measure M f)"
   406 proof (simp add: countably_subadditive_def, safe)
   407   fix A :: "nat \<Rightarrow> _" assume A: "range A \<subseteq> Pow (\<Omega>)" and sb: "(\<Union>i. A i) \<subseteq> \<Omega>"
   408   let ?O = "outer_measure M f"
   410   { fix e :: ereal assume e: "0 < e" and "\<forall>i. ?O (A i) \<noteq> \<infinity>"
   411     hence "\<exists>B. \<forall>n. range (B n) \<subseteq> M \<and> disjoint_family (B n) \<and> A n \<subseteq> (\<Union>i. B n i) \<and>
   412         (\<Sum>i. f (B n i)) \<le> ?O (A n) + e * (1/2)^(Suc n)"
   413       using e sb by (auto intro!: choice outer_measure_close [of f, OF posf] simp: ereal_zero_less_0_iff one_ereal_def)
   414     then obtain B
   415       where B: "\<And>n. range (B n) \<subseteq> M"
   416       and sbB: "\<And>n. A n \<subseteq> (\<Union>i. B n i)"
   417       and Ble: "\<And>n. (\<Sum>i. f (B n i)) \<le> ?O (A n) + e * (1/2)^(Suc n)"
   418       by auto blast
   420     def C \<equiv> "case_prod B o prod_decode"
   421     from B have B_in_M: "\<And>i j. B i j \<in> M"
   422       by (rule range_subsetD)
   423     then have C: "range C \<subseteq> M"
   424       by (auto simp add: C_def split_def)
   425     have A_C: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)"
   426       using sbB by (auto simp add: C_def subset_eq) (metis prod_encode_inverse)
   428     have "?O (\<Union>i. A i) \<le> ?O (\<Union>i. C i)"  
   429       using A_C A C by (intro increasing_outer_measure[THEN increasingD]) (auto dest!: sets_into_space)
   430     also have "\<dots> \<le> (\<Sum>i. f (C i))"
   431       using C by (intro outer_measure_le[OF posf inc]) auto
   432     also have "\<dots> = (\<Sum>n. \<Sum>i. f (B n i))"
   433       using B_in_M unfolding C_def comp_def by (intro suminf_ereal_2dimen positiveD2[OF posf]) auto
   434     also have "\<dots> \<le> (\<Sum>n. ?O (A n) + e*(1/2) ^ Suc n)"
   435       using B_in_M by (intro suminf_le_pos[OF Ble] suminf_0_le posf[THEN positiveD2]) auto
   436     also have "... = (\<Sum>n. ?O (A n)) + (\<Sum>n. e*(1/2) ^ Suc n)"
   437       using e by (subst suminf_add_ereal) (auto simp add: ereal_zero_le_0_iff outer_measure_nonneg posf)
   438     also have "(\<Sum>n. e*(1/2) ^ Suc n) = e"
   439       using suminf_half_series_ereal e by (simp add: ereal_zero_le_0_iff suminf_cmult_ereal)
   440     finally have "?O (\<Union>i. A i) \<le> (\<Sum>n. ?O (A n)) + e" . }
   441   note * = this
   443   show "?O (\<Union>i. A i) \<le> (\<Sum>n. ?O (A n))"
   444   proof cases
   445     assume "\<forall>i. ?O (A i) \<noteq> \<infinity>" with * show ?thesis
   446       by (intro ereal_le_epsilon) auto
   447   qed (metis suminf_PInfty[OF outer_measure_nonneg, OF posf] ereal_less_eq(1))
   448 qed
   450 lemma (in ring_of_sets) outer_measure_space_outer_measure:
   451   "positive M f \<Longrightarrow> increasing M f \<Longrightarrow> outer_measure_space (Pow \<Omega>) (outer_measure M f)"
   452   by (simp add: outer_measure_space_def
   453     positive_outer_measure increasing_outer_measure countably_subadditive_outer_measure)
   455 lemma (in ring_of_sets) algebra_subset_lambda_system:
   456   assumes posf: "positive M f" and inc: "increasing M f"
   457       and add: "additive M f"
   458   shows "M \<subseteq> lambda_system \<Omega> (Pow \<Omega>) (outer_measure M f)"
   459 proof (auto dest: sets_into_space
   460             simp add: algebra.lambda_system_eq [OF algebra_Pow])
   461   fix x s assume x: "x \<in> M" and s: "s \<subseteq> \<Omega>"
   462   have [simp]: "\<And>x. x \<in> M \<Longrightarrow> s \<inter> (\<Omega> - x) = s - x" using s
   463     by blast
   464   have "outer_measure M f (s \<inter> x) + outer_measure M f (s - x) \<le> outer_measure M f s"
   465     unfolding outer_measure_def[of M f s]
   466   proof (safe intro!: INF_greatest)
   467     fix A :: "nat \<Rightarrow> 'a set" assume A: "disjoint_family A" "range A \<subseteq> M" "s \<subseteq> (\<Union>i. A i)"
   468     have "outer_measure M f (s \<inter> x) \<le> (\<Sum>i. f (A i \<inter> x))"
   469       unfolding outer_measure_def
   470     proof (safe intro!: INF_lower2[of "\<lambda>i. A i \<inter> x"])
   471       from A(1) show "disjoint_family (\<lambda>i. A i \<inter> x)"
   472         by (rule disjoint_family_on_bisimulation) auto
   473     qed (insert x A, auto)
   474     moreover
   475     have "outer_measure M f (s - x) \<le> (\<Sum>i. f (A i - x))"
   476       unfolding outer_measure_def
   477     proof (safe intro!: INF_lower2[of "\<lambda>i. A i - x"])
   478       from A(1) show "disjoint_family (\<lambda>i. A i - x)"
   479         by (rule disjoint_family_on_bisimulation) auto
   480     qed (insert x A, auto)
   481     ultimately have "outer_measure M f (s \<inter> x) + outer_measure M f (s - x) \<le>
   482         (\<Sum>i. f (A i \<inter> x)) + (\<Sum>i. f (A i - x))" by (rule add_mono)
   483     also have "\<dots> = (\<Sum>i. f (A i \<inter> x) + f (A i - x))"
   484       using A(2) x posf by (subst suminf_add_ereal) (auto simp: positive_def)
   485     also have "\<dots> = (\<Sum>i. f (A i))"
   486       using A x
   487       by (subst add[THEN additiveD, symmetric])
   488          (auto intro!: arg_cong[where f=suminf] arg_cong[where f=f])
   489     finally show "outer_measure M f (s \<inter> x) + outer_measure M f (s - x) \<le> (\<Sum>i. f (A i))" .
   490   qed
   491   moreover
   492   have "outer_measure M f s \<le> outer_measure M f (s \<inter> x) + outer_measure M f (s - x)"
   493   proof -
   494     have "outer_measure M f s = outer_measure M f ((s \<inter> x) \<union> (s - x))"
   495       by (metis Un_Diff_Int Un_commute)
   496     also have "... \<le> outer_measure M f (s \<inter> x) + outer_measure M f (s - x)"
   497       apply (rule subadditiveD)
   498       apply (rule ring_of_sets.countably_subadditive_subadditive [OF ring_of_sets_Pow])
   499       apply (simp add: positive_def outer_measure_empty[OF posf] outer_measure_nonneg[OF posf])
   500       apply (rule countably_subadditive_outer_measure)
   501       using s by (auto intro!: posf inc)
   502     finally show ?thesis .
   503   qed
   504   ultimately
   505   show "outer_measure M f (s \<inter> x) + outer_measure M f (s - x) = outer_measure M f s"
   506     by (rule order_antisym)
   507 qed
   509 lemma measure_down: "measure_space \<Omega> N \<mu> \<Longrightarrow> sigma_algebra \<Omega> M \<Longrightarrow> M \<subseteq> N \<Longrightarrow> measure_space \<Omega> M \<mu>"
   510   by (auto simp add: measure_space_def positive_def countably_additive_def subset_eq)
   512 subsection {* Caratheodory's theorem *}
   514 theorem (in ring_of_sets) caratheodory':
   515   assumes posf: "positive M f" and ca: "countably_additive M f"
   516   shows "\<exists>\<mu> :: 'a set \<Rightarrow> ereal. (\<forall>s \<in> M. \<mu> s = f s) \<and> measure_space \<Omega> (sigma_sets \<Omega> M) \<mu>"
   517 proof -
   518   have inc: "increasing M f"
   519     by (metis additive_increasing ca countably_additive_additive posf)
   520   let ?O = "outer_measure M f"
   521   def ls \<equiv> "lambda_system \<Omega> (Pow \<Omega>) ?O"
   522   have mls: "measure_space \<Omega> ls ?O"
   523     using sigma_algebra.caratheodory_lemma
   524             [OF sigma_algebra_Pow outer_measure_space_outer_measure [OF posf inc]]
   525     by (simp add: ls_def)
   526   hence sls: "sigma_algebra \<Omega> ls"
   527     by (simp add: measure_space_def)
   528   have "M \<subseteq> ls"
   529     by (simp add: ls_def)
   530        (metis ca posf inc countably_additive_additive algebra_subset_lambda_system)
   531   hence sgs_sb: "sigma_sets (\<Omega>) (M) \<subseteq> ls"
   532     using sigma_algebra.sigma_sets_subset [OF sls, of "M"]
   533     by simp
   534   have "measure_space \<Omega> (sigma_sets \<Omega> M) ?O"
   535     by (rule measure_down [OF mls], rule sigma_algebra_sigma_sets)
   536        (simp_all add: sgs_sb space_closed)
   537   thus ?thesis using outer_measure_agrees [OF posf ca]
   538     by (intro exI[of _ ?O]) auto
   539 qed
   541 lemma (in ring_of_sets) caratheodory_empty_continuous:
   542   assumes f: "positive M f" "additive M f" and fin: "\<And>A. A \<in> M \<Longrightarrow> f A \<noteq> \<infinity>"
   543   assumes cont: "\<And>A. range A \<subseteq> M \<Longrightarrow> decseq A \<Longrightarrow> (\<Inter>i. A i) = {} \<Longrightarrow> (\<lambda>i. f (A i)) ----> 0"
   544   shows "\<exists>\<mu> :: 'a set \<Rightarrow> ereal. (\<forall>s \<in> M. \<mu> s = f s) \<and> measure_space \<Omega> (sigma_sets \<Omega> M) \<mu>"
   545 proof (intro caratheodory' empty_continuous_imp_countably_additive f)
   546   show "\<forall>A\<in>M. f A \<noteq> \<infinity>" using fin by auto
   547 qed (rule cont)
   549 subsection {* Volumes *}
   551 definition volume :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> bool" where
   552   "volume M f \<longleftrightarrow>
   553   (f {} = 0) \<and> (\<forall>a\<in>M. 0 \<le> f a) \<and>
   554   (\<forall>C\<subseteq>M. disjoint C \<longrightarrow> finite C \<longrightarrow> \<Union>C \<in> M \<longrightarrow> f (\<Union>C) = (\<Sum>c\<in>C. f c))"
   556 lemma volumeI:
   557   assumes "f {} = 0"
   558   assumes "\<And>a. a \<in> M \<Longrightarrow> 0 \<le> f a"
   559   assumes "\<And>C. C \<subseteq> M \<Longrightarrow> disjoint C \<Longrightarrow> finite C \<Longrightarrow> \<Union>C \<in> M \<Longrightarrow> f (\<Union>C) = (\<Sum>c\<in>C. f c)"
   560   shows "volume M f"
   561   using assms by (auto simp: volume_def)
   563 lemma volume_positive:
   564   "volume M f \<Longrightarrow> a \<in> M \<Longrightarrow> 0 \<le> f a"
   565   by (auto simp: volume_def)
   567 lemma volume_empty:
   568   "volume M f \<Longrightarrow> f {} = 0"
   569   by (auto simp: volume_def)
   571 lemma volume_finite_additive:
   572   assumes "volume M f" 
   573   assumes A: "\<And>i. i \<in> I \<Longrightarrow> A i \<in> M" "disjoint_family_on A I" "finite I" "UNION I A \<in> M"
   574   shows "f (UNION I A) = (\<Sum>i\<in>I. f (A i))"
   575 proof -
   576   have "A`I \<subseteq> M" "disjoint (A`I)" "finite (A`I)" "\<Union>(A`I) \<in> M"
   577     using A unfolding SUP_def by (auto simp: disjoint_family_on_disjoint_image)
   578   with `volume M f` have "f (\<Union>(A`I)) = (\<Sum>a\<in>A`I. f a)"
   579     unfolding volume_def by blast
   580   also have "\<dots> = (\<Sum>i\<in>I. f (A i))"
   581   proof (subst setsum.reindex_nontrivial)
   582     fix i j assume "i \<in> I" "j \<in> I" "i \<noteq> j" "A i = A j"
   583     with `disjoint_family_on A I` have "A i = {}"
   584       by (auto simp: disjoint_family_on_def)
   585     then show "f (A i) = 0"
   586       using volume_empty[OF `volume M f`] by simp
   587   qed (auto intro: `finite I`)
   588   finally show "f (UNION I A) = (\<Sum>i\<in>I. f (A i))"
   589     by simp
   590 qed
   592 lemma (in ring_of_sets) volume_additiveI:
   593   assumes pos: "\<And>a. a \<in> M \<Longrightarrow> 0 \<le> \<mu> a" 
   594   assumes [simp]: "\<mu> {} = 0"
   595   assumes add: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<inter> b = {} \<Longrightarrow> \<mu> (a \<union> b) = \<mu> a + \<mu> b"
   596   shows "volume M \<mu>"
   597 proof (unfold volume_def, safe)
   598   fix C assume "finite C" "C \<subseteq> M" "disjoint C"
   599   then show "\<mu> (\<Union>C) = setsum \<mu> C"
   600   proof (induct C)
   601     case (insert c C)
   602     from insert(1,2,4,5) have "\<mu> (\<Union>insert c C) = \<mu> c + \<mu> (\<Union>C)"
   603       by (auto intro!: add simp: disjoint_def)
   604     with insert show ?case
   605       by (simp add: disjoint_def)
   606   qed simp
   607 qed fact+
   609 lemma (in semiring_of_sets) extend_volume:
   610   assumes "volume M \<mu>"
   611   shows "\<exists>\<mu>'. volume generated_ring \<mu>' \<and> (\<forall>a\<in>M. \<mu>' a = \<mu> a)"
   612 proof -
   613   let ?R = generated_ring
   614   have "\<forall>a\<in>?R. \<exists>m. \<exists>C\<subseteq>M. a = \<Union>C \<and> finite C \<and> disjoint C \<and> m = (\<Sum>c\<in>C. \<mu> c)"
   615     by (auto simp: generated_ring_def)
   616   from bchoice[OF this] guess \<mu>' .. note \<mu>'_spec = this
   618   { fix C assume C: "C \<subseteq> M" "finite C" "disjoint C"
   619     fix D assume D: "D \<subseteq> M" "finite D" "disjoint D"
   620     assume "\<Union>C = \<Union>D"
   621     have "(\<Sum>d\<in>D. \<mu> d) = (\<Sum>d\<in>D. \<Sum>c\<in>C. \<mu> (c \<inter> d))"
   622     proof (intro setsum.cong refl)
   623       fix d assume "d \<in> D"
   624       have Un_eq_d: "(\<Union>c\<in>C. c \<inter> d) = d"
   625         using `d \<in> D` `\<Union>C = \<Union>D` by auto
   626       moreover have "\<mu> (\<Union>c\<in>C. c \<inter> d) = (\<Sum>c\<in>C. \<mu> (c \<inter> d))"
   627       proof (rule volume_finite_additive)
   628         { fix c assume "c \<in> C" then show "c \<inter> d \<in> M"
   629             using C D `d \<in> D` by auto }
   630         show "(\<Union>a\<in>C. a \<inter> d) \<in> M"
   631           unfolding Un_eq_d using `d \<in> D` D by auto
   632         show "disjoint_family_on (\<lambda>a. a \<inter> d) C"
   633           using `disjoint C` by (auto simp: disjoint_family_on_def disjoint_def)
   634       qed fact+
   635       ultimately show "\<mu> d = (\<Sum>c\<in>C. \<mu> (c \<inter> d))" by simp
   636     qed }
   637   note split_sum = this
   639   { fix C assume C: "C \<subseteq> M" "finite C" "disjoint C"
   640     fix D assume D: "D \<subseteq> M" "finite D" "disjoint D"
   641     assume "\<Union>C = \<Union>D"
   642     with split_sum[OF C D] split_sum[OF D C]
   643     have "(\<Sum>d\<in>D. \<mu> d) = (\<Sum>c\<in>C. \<mu> c)"
   644       by (simp, subst setsum.commute, simp add: ac_simps) }
   645   note sum_eq = this
   647   { fix C assume C: "C \<subseteq> M" "finite C" "disjoint C"
   648     then have "\<Union>C \<in> ?R" by (auto simp: generated_ring_def)
   649     with \<mu>'_spec[THEN bspec, of "\<Union>C"]
   650     obtain D where
   651       D: "D \<subseteq> M" "finite D" "disjoint D" "\<Union>C = \<Union>D" and "\<mu>' (\<Union>C) = (\<Sum>d\<in>D. \<mu> d)"
   652       by blast
   653     with sum_eq[OF C D] have "\<mu>' (\<Union>C) = (\<Sum>c\<in>C. \<mu> c)" by simp }
   654   note \<mu>' = this
   656   show ?thesis
   657   proof (intro exI conjI ring_of_sets.volume_additiveI[OF generating_ring] ballI)
   658     fix a assume "a \<in> M" with \<mu>'[of "{a}"] show "\<mu>' a = \<mu> a"
   659       by (simp add: disjoint_def)
   660   next
   661     fix a assume "a \<in> ?R" then guess Ca .. note Ca = this
   662     with \<mu>'[of Ca] `volume M \<mu>`[THEN volume_positive]
   663     show "0 \<le> \<mu>' a"
   664       by (auto intro!: setsum_nonneg)
   665   next
   666     show "\<mu>' {} = 0" using \<mu>'[of "{}"] by auto
   667   next
   668     fix a assume "a \<in> ?R" then guess Ca .. note Ca = this
   669     fix b assume "b \<in> ?R" then guess Cb .. note Cb = this
   670     assume "a \<inter> b = {}"
   671     with Ca Cb have "Ca \<inter> Cb \<subseteq> {{}}" by auto
   672     then have C_Int_cases: "Ca \<inter> Cb = {{}} \<or> Ca \<inter> Cb = {}" by auto
   674     from `a \<inter> b = {}` have "\<mu>' (\<Union>(Ca \<union> Cb)) = (\<Sum>c\<in>Ca \<union> Cb. \<mu> c)"
   675       using Ca Cb by (intro \<mu>') (auto intro!: disjoint_union)
   676     also have "\<dots> = (\<Sum>c\<in>Ca \<union> Cb. \<mu> c) + (\<Sum>c\<in>Ca \<inter> Cb. \<mu> c)"
   677       using C_Int_cases volume_empty[OF `volume M \<mu>`] by (elim disjE) simp_all
   678     also have "\<dots> = (\<Sum>c\<in>Ca. \<mu> c) + (\<Sum>c\<in>Cb. \<mu> c)"
   679       using Ca Cb by (simp add: setsum.union_inter)
   680     also have "\<dots> = \<mu>' a + \<mu>' b"
   681       using Ca Cb by (simp add: \<mu>')
   682     finally show "\<mu>' (a \<union> b) = \<mu>' a + \<mu>' b"
   683       using Ca Cb by simp
   684   qed
   685 qed
   687 subsubsection {* Caratheodory on semirings *}
   689 theorem (in semiring_of_sets) caratheodory:
   690   assumes pos: "positive M \<mu>" and ca: "countably_additive M \<mu>"
   691   shows "\<exists>\<mu>' :: 'a set \<Rightarrow> ereal. (\<forall>s \<in> M. \<mu>' s = \<mu> s) \<and> measure_space \<Omega> (sigma_sets \<Omega> M) \<mu>'"
   692 proof -
   693   have "volume M \<mu>"
   694   proof (rule volumeI)
   695     { fix a assume "a \<in> M" then show "0 \<le> \<mu> a"
   696         using pos unfolding positive_def by auto }
   697     note p = this
   699     fix C assume sets_C: "C \<subseteq> M" "\<Union>C \<in> M" and "disjoint C" "finite C"
   700     have "\<exists>F'. bij_betw F' {..<card C} C"
   701       by (rule finite_same_card_bij[OF _ `finite C`]) auto
   702     then guess F' .. note F' = this
   703     then have F': "C = F' ` {..< card C}" "inj_on F' {..< card C}"
   704       by (auto simp: bij_betw_def)
   705     { fix i j assume *: "i < card C" "j < card C" "i \<noteq> j"
   706       with F' have "F' i \<in> C" "F' j \<in> C" "F' i \<noteq> F' j"
   707         unfolding inj_on_def by auto
   708       with `disjoint C`[THEN disjointD]
   709       have "F' i \<inter> F' j = {}"
   710         by auto }
   711     note F'_disj = this
   712     def F \<equiv> "\<lambda>i. if i < card C then F' i else {}"
   713     then have "disjoint_family F"
   714       using F'_disj by (auto simp: disjoint_family_on_def)
   715     moreover from F' have "(\<Union>i. F i) = \<Union>C"
   716       by (auto simp: F_def set_eq_iff split: split_if_asm)
   717     moreover have sets_F: "\<And>i. F i \<in> M"
   718       using F' sets_C by (auto simp: F_def)
   719     moreover note sets_C
   720     ultimately have "\<mu> (\<Union>C) = (\<Sum>i. \<mu> (F i))"
   721       using ca[unfolded countably_additive_def, THEN spec, of F] by auto
   722     also have "\<dots> = (\<Sum>i<card C. \<mu> (F' i))"
   723     proof -
   724       have "(\<lambda>i. if i \<in> {..< card C} then \<mu> (F' i) else 0) sums (\<Sum>i<card C. \<mu> (F' i))"
   725         by (rule sums_If_finite_set) auto
   726       also have "(\<lambda>i. if i \<in> {..< card C} then \<mu> (F' i) else 0) = (\<lambda>i. \<mu> (F i))"
   727         using pos by (auto simp: positive_def F_def)
   728       finally show "(\<Sum>i. \<mu> (F i)) = (\<Sum>i<card C. \<mu> (F' i))"
   729         by (simp add: sums_iff)
   730     qed
   731     also have "\<dots> = (\<Sum>c\<in>C. \<mu> c)"
   732       using F'(2) by (subst (2) F') (simp add: setsum.reindex)
   733     finally show "\<mu> (\<Union>C) = (\<Sum>c\<in>C. \<mu> c)" .
   734   next
   735     show "\<mu> {} = 0"
   736       using `positive M \<mu>` by (rule positiveD1)
   737   qed
   738   from extend_volume[OF this] obtain \<mu>_r where
   739     V: "volume generated_ring \<mu>_r" "\<And>a. a \<in> M \<Longrightarrow> \<mu> a = \<mu>_r a"
   740     by auto
   742   interpret G: ring_of_sets \<Omega> generated_ring
   743     by (rule generating_ring)
   745   have pos: "positive generated_ring \<mu>_r"
   746     using V unfolding positive_def by (auto simp: positive_def intro!: volume_positive volume_empty)
   748   have "countably_additive generated_ring \<mu>_r"
   749   proof (rule countably_additiveI)
   750     fix A' :: "nat \<Rightarrow> 'a set" assume A': "range A' \<subseteq> generated_ring" "disjoint_family A'"
   751       and Un_A: "(\<Union>i. A' i) \<in> generated_ring"
   753     from generated_ringE[OF Un_A] guess C' . note C' = this
   755     { fix c assume "c \<in> C'"
   756       moreover def A \<equiv> "\<lambda>i. A' i \<inter> c"
   757       ultimately have A: "range A \<subseteq> generated_ring" "disjoint_family A"
   758         and Un_A: "(\<Union>i. A i) \<in> generated_ring"
   759         using A' C'
   760         by (auto intro!: G.Int G.finite_Union intro: generated_ringI_Basic simp: disjoint_family_on_def)
   761       from A C' `c \<in> C'` have UN_eq: "(\<Union>i. A i) = c"
   762         by (auto simp: A_def)
   764       have "\<forall>i::nat. \<exists>f::nat \<Rightarrow> 'a set. \<mu>_r (A i) = (\<Sum>j. \<mu>_r (f j)) \<and> disjoint_family f \<and> \<Union>range f = A i \<and> (\<forall>j. f j \<in> M)"
   765         (is "\<forall>i. ?P i")
   766       proof
   767         fix i
   768         from A have Ai: "A i \<in> generated_ring" by auto
   769         from generated_ringE[OF this] guess C . note C = this
   771         have "\<exists>F'. bij_betw F' {..<card C} C"
   772           by (rule finite_same_card_bij[OF _ `finite C`]) auto
   773         then guess F .. note F = this
   774         def f \<equiv> "\<lambda>i. if i < card C then F i else {}"
   775         then have f: "bij_betw f {..< card C} C"
   776           by (intro bij_betw_cong[THEN iffD1, OF _ F]) auto
   777         with C have "\<forall>j. f j \<in> M"
   778           by (auto simp: Pi_iff f_def dest!: bij_betw_imp_funcset)
   779         moreover
   780         from f C have d_f: "disjoint_family_on f {..<card C}"
   781           by (intro disjoint_image_disjoint_family_on) (auto simp: bij_betw_def)
   782         then have "disjoint_family f"
   783           by (auto simp: disjoint_family_on_def f_def)
   784         moreover
   785         have Ai_eq: "A i = (\<Union>x<card C. f x)"
   786           using f C Ai unfolding bij_betw_def by (simp add: Union_image_eq[symmetric])
   787         then have "\<Union>range f = A i"
   788           using f C Ai unfolding bij_betw_def by (auto simp: f_def)
   789         moreover 
   790         { have "(\<Sum>j. \<mu>_r (f j)) = (\<Sum>j. if j \<in> {..< card C} then \<mu>_r (f j) else 0)"
   791             using volume_empty[OF V(1)] by (auto intro!: arg_cong[where f=suminf] simp: f_def)
   792           also have "\<dots> = (\<Sum>j<card C. \<mu>_r (f j))"
   793             by (rule sums_If_finite_set[THEN sums_unique, symmetric]) simp
   794           also have "\<dots> = \<mu>_r (A i)"
   795             using C f[THEN bij_betw_imp_funcset] unfolding Ai_eq
   796             by (intro volume_finite_additive[OF V(1) _ d_f, symmetric])
   797                (auto simp: Pi_iff Ai_eq intro: generated_ringI_Basic)
   798           finally have "\<mu>_r (A i) = (\<Sum>j. \<mu>_r (f j))" .. }
   799         ultimately show "?P i"
   800           by blast
   801       qed
   802       from choice[OF this] guess f .. note f = this
   803       then have UN_f_eq: "(\<Union>i. case_prod f (prod_decode i)) = (\<Union>i. A i)"
   804         unfolding UN_extend_simps surj_prod_decode by (auto simp: set_eq_iff)
   806       have d: "disjoint_family (\<lambda>i. case_prod f (prod_decode i))"
   807         unfolding disjoint_family_on_def
   808       proof (intro ballI impI)
   809         fix m n :: nat assume "m \<noteq> n"
   810         then have neq: "prod_decode m \<noteq> prod_decode n"
   811           using inj_prod_decode[of UNIV] by (auto simp: inj_on_def)
   812         show "case_prod f (prod_decode m) \<inter> case_prod f (prod_decode n) = {}"
   813         proof cases
   814           assume "fst (prod_decode m) = fst (prod_decode n)"
   815           then show ?thesis
   816             using neq f by (fastforce simp: disjoint_family_on_def)
   817         next
   818           assume neq: "fst (prod_decode m) \<noteq> fst (prod_decode n)"
   819           have "case_prod f (prod_decode m) \<subseteq> A (fst (prod_decode m))"
   820             "case_prod f (prod_decode n) \<subseteq> A (fst (prod_decode n))"
   821             using f[THEN spec, of "fst (prod_decode m)"]
   822             using f[THEN spec, of "fst (prod_decode n)"]
   823             by (auto simp: set_eq_iff)
   824           with f A neq show ?thesis
   825             by (fastforce simp: disjoint_family_on_def subset_eq set_eq_iff)
   826         qed
   827       qed
   828       from f have "(\<Sum>n. \<mu>_r (A n)) = (\<Sum>n. \<mu>_r (case_prod f (prod_decode n)))"
   829         by (intro suminf_ereal_2dimen[symmetric] positiveD2[OF pos] generated_ringI_Basic)
   830          (auto split: prod.split)
   831       also have "\<dots> = (\<Sum>n. \<mu> (case_prod f (prod_decode n)))"
   832         using f V(2) by (auto intro!: arg_cong[where f=suminf] split: prod.split)
   833       also have "\<dots> = \<mu> (\<Union>i. case_prod f (prod_decode i))"
   834         using f `c \<in> C'` C'
   835         by (intro ca[unfolded countably_additive_def, rule_format])
   836            (auto split: prod.split simp: UN_f_eq d UN_eq)
   837       finally have "(\<Sum>n. \<mu>_r (A' n \<inter> c)) = \<mu> c"
   838         using UN_f_eq UN_eq by (simp add: A_def) }
   839     note eq = this
   841     have "(\<Sum>n. \<mu>_r (A' n)) = (\<Sum>n. \<Sum>c\<in>C'. \<mu>_r (A' n \<inter> c))"
   842       using C' A'
   843       by (subst volume_finite_additive[symmetric, OF V(1)])
   844          (auto simp: disjoint_def disjoint_family_on_def Union_image_eq[symmetric] simp del: Sup_image_eq Union_image_eq
   845                intro!: G.Int G.finite_Union arg_cong[where f="\<lambda>X. suminf (\<lambda>i. \<mu>_r (X i))"] ext
   846                intro: generated_ringI_Basic)
   847     also have "\<dots> = (\<Sum>c\<in>C'. \<Sum>n. \<mu>_r (A' n \<inter> c))"
   848       using C' A'
   849       by (intro suminf_setsum_ereal positiveD2[OF pos] G.Int G.finite_Union)
   850          (auto intro: generated_ringI_Basic)
   851     also have "\<dots> = (\<Sum>c\<in>C'. \<mu>_r c)"
   852       using eq V C' by (auto intro!: setsum.cong)
   853     also have "\<dots> = \<mu>_r (\<Union>C')"
   854       using C' Un_A
   855       by (subst volume_finite_additive[symmetric, OF V(1)])
   856          (auto simp: disjoint_family_on_def disjoint_def Union_image_eq[symmetric] simp del: Sup_image_eq Union_image_eq 
   857                intro: generated_ringI_Basic)
   858     finally show "(\<Sum>n. \<mu>_r (A' n)) = \<mu>_r (\<Union>i. A' i)"
   859       using C' by simp
   860   qed
   861   from G.caratheodory'[OF `positive generated_ring \<mu>_r` `countably_additive generated_ring \<mu>_r`]
   862   guess \<mu>' ..
   863   with V show ?thesis
   864     unfolding sigma_sets_generated_ring_eq
   865     by (intro exI[of _ \<mu>']) (auto intro: generated_ringI_Basic)
   866 qed
   868 lemma extend_measure_caratheodory:
   869   fixes G :: "'i \<Rightarrow> 'a set"
   870   assumes M: "M = extend_measure \<Omega> I G \<mu>"
   871   assumes "i \<in> I"
   872   assumes "semiring_of_sets \<Omega> (G ` I)"
   873   assumes empty: "\<And>i. i \<in> I \<Longrightarrow> G i = {} \<Longrightarrow> \<mu> i = 0"
   874   assumes inj: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> G i = G j \<Longrightarrow> \<mu> i = \<mu> j"
   875   assumes nonneg: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> \<mu> i"
   876   assumes add: "\<And>A::nat \<Rightarrow> 'i. \<And>j. A \<in> UNIV \<rightarrow> I \<Longrightarrow> j \<in> I \<Longrightarrow> disjoint_family (G \<circ> A) \<Longrightarrow>
   877     (\<Union>i. G (A i)) = G j \<Longrightarrow> (\<Sum>n. \<mu> (A n)) = \<mu> j"
   878   shows "emeasure M (G i) = \<mu> i"
   879 proof -
   880   interpret semiring_of_sets \<Omega> "G ` I"
   881     by fact
   882   have "\<forall>g\<in>G`I. \<exists>i\<in>I. g = G i"
   883     by auto
   884   then obtain sel where sel: "\<And>g. g \<in> G ` I \<Longrightarrow> sel g \<in> I" "\<And>g. g \<in> G ` I \<Longrightarrow> G (sel g) = g"
   885     by metis
   887   have "\<exists>\<mu>'. (\<forall>s\<in>G ` I. \<mu>' s = \<mu> (sel s)) \<and> measure_space \<Omega> (sigma_sets \<Omega> (G ` I)) \<mu>'"
   888   proof (rule caratheodory)
   889     show "positive (G ` I) (\<lambda>s. \<mu> (sel s))"
   890       by (auto simp: positive_def intro!: empty sel nonneg)
   891     show "countably_additive (G ` I) (\<lambda>s. \<mu> (sel s))"
   892     proof (rule countably_additiveI)
   893       fix A :: "nat \<Rightarrow> 'a set" assume "range A \<subseteq> G ` I" "disjoint_family A" "(\<Union>i. A i) \<in> G ` I"
   894       then show "(\<Sum>i. \<mu> (sel (A i))) = \<mu> (sel (\<Union>i. A i))"
   895         by (intro add) (auto simp: sel image_subset_iff_funcset comp_def Pi_iff intro!: sel)
   896     qed
   897   qed
   898   then obtain \<mu>' where \<mu>': "\<forall>s\<in>G ` I. \<mu>' s = \<mu> (sel s)" "measure_space \<Omega> (sigma_sets \<Omega> (G ` I)) \<mu>'"
   899     by metis
   901   show ?thesis
   902   proof (rule emeasure_extend_measure[OF M])
   903     { fix i assume "i \<in> I" then show "\<mu>' (G i) = \<mu> i"
   904       using \<mu>' by (auto intro!: inj sel) }
   905     show "G ` I \<subseteq> Pow \<Omega>"
   906       by fact
   907     then show "positive (sets M) \<mu>'" "countably_additive (sets M) \<mu>'"
   908       using \<mu>' by (simp_all add: M sets_extend_measure measure_space_def)
   909   qed fact
   910 qed
   912 lemma extend_measure_caratheodory_pair:
   913   fixes G :: "'i \<Rightarrow> 'j \<Rightarrow> 'a set"
   914   assumes M: "M = extend_measure \<Omega> {(a, b). P a b} (\<lambda>(a, b). G a b) (\<lambda>(a, b). \<mu> a b)"
   915   assumes "P i j"
   916   assumes semiring: "semiring_of_sets \<Omega> {G a b | a b. P a b}"
   917   assumes empty: "\<And>i j. P i j \<Longrightarrow> G i j = {} \<Longrightarrow> \<mu> i j = 0"
   918   assumes inj: "\<And>i j k l. P i j \<Longrightarrow> P k l \<Longrightarrow> G i j = G k l \<Longrightarrow> \<mu> i j = \<mu> k l"
   919   assumes nonneg: "\<And>i j. P i j \<Longrightarrow> 0 \<le> \<mu> i j"
   920   assumes add: "\<And>A::nat \<Rightarrow> 'i. \<And>B::nat \<Rightarrow> 'j. \<And>j k.
   921     (\<And>n. P (A n) (B n)) \<Longrightarrow> P j k \<Longrightarrow> disjoint_family (\<lambda>n. G (A n) (B n)) \<Longrightarrow>
   922     (\<Union>i. G (A i) (B i)) = G j k \<Longrightarrow> (\<Sum>n. \<mu> (A n) (B n)) = \<mu> j k"
   923   shows "emeasure M (G i j) = \<mu> i j"
   924 proof -
   925   have "emeasure M ((\<lambda>(a, b). G a b) (i, j)) = (\<lambda>(a, b). \<mu> a b) (i, j)"
   926   proof (rule extend_measure_caratheodory[OF M])
   927     show "semiring_of_sets \<Omega> ((\<lambda>(a, b). G a b) ` {(a, b). P a b})"
   928       using semiring by (simp add: image_def conj_commute)
   929   next
   930     fix A :: "nat \<Rightarrow> ('i \<times> 'j)" and j assume "A \<in> UNIV \<rightarrow> {(a, b). P a b}" "j \<in> {(a, b). P a b}"
   931       "disjoint_family ((\<lambda>(a, b). G a b) \<circ> A)"
   932       "(\<Union>i. case A i of (a, b) \<Rightarrow> G a b) = (case j of (a, b) \<Rightarrow> G a b)"
   933     then show "(\<Sum>n. case A n of (a, b) \<Rightarrow> \<mu> a b) = (case j of (a, b) \<Rightarrow> \<mu> a b)"
   934       using add[of "\<lambda>i. fst (A i)" "\<lambda>i. snd (A i)" "fst j" "snd j"]
   935       by (simp add: split_beta' comp_def Pi_iff)
   936   qed (auto split: prod.splits intro: assms)
   937   then show ?thesis by simp
   938 qed
   940 end