(* Title: HOL/Analysis/Caratheodory.thy Author: Lawrence C Paulson Author: Johannes Hölzl, TU München *) section ‹Caratheodory Extension Theorem› theory Caratheodory imports Measure_Space begin text ‹ Originally from the Hurd/Coble measure theory development, translated by Lawrence Paulson. › lemma suminf_ennreal_2dimen: fixes f:: "nat × nat ⇒ ennreal" assumes "⋀m. g m = (∑n. f (m,n))" shows "(∑i. f (prod_decode i)) = suminf g" proof - have g_def: "g = (λm. (∑n. f (m,n)))" using assms by (simp add: fun_eq_iff) have reindex: "⋀B. (∑x∈B. f (prod_decode x)) = sum f (prod_decode ` B)" by (simp add: sum.reindex[OF inj_prod_decode] comp_def) have "(SUP n. ∑i<n. f (prod_decode i)) = (SUP p ∈ UNIV × UNIV. ∑i<fst p. ∑n<snd p. f (i, n))" proof (intro SUP_eq; clarsimp simp: sum.cartesian_product reindex) fix n let ?M = "λf. Suc (Max (f ` prod_decode ` {..<n}))" { fix a b x assume "x < n" and [symmetric]: "(a, b) = prod_decode x" then have "a < ?M fst" "b < ?M snd" by (auto intro!: Max_ge le_imp_less_Suc image_eqI) } then have "sum f (prod_decode ` {..<n}) ≤ sum f ({..<?M fst} × {..<?M snd})" by (auto intro!: sum_mono2) then show "∃a b. sum f (prod_decode ` {..<n}) ≤ sum f ({..<a} × {..<b})" by auto next fix a b let ?M = "prod_decode ` {..<Suc (Max (prod_encode ` ({..<a} × {..<b})))}" { fix a' b' assume "a' < a" "b' < b" then have "(a', b') ∈ ?M" by (auto intro!: Max_ge le_imp_less_Suc image_eqI[where x="prod_encode (a', b')"]) } then have "sum f ({..<a} × {..<b}) ≤ sum f ?M" by (auto intro!: sum_mono2) then show "∃n. sum f ({..<a} × {..<b}) ≤ sum f (prod_decode ` {..<n})" by auto qed also have "… = (SUP p. ∑i<p. ∑n. f (i, n))" unfolding suminf_sum[OF summableI, symmetric] by (simp add: suminf_eq_SUP SUP_pair sum.swap[of _ "{..< fst _}"]) finally show ?thesis unfolding g_def by (simp add: suminf_eq_SUP) qed subsection ‹Characterizations of Measures› definition✐‹tag important› outer_measure_space where "outer_measure_space M f ⟷ positive M f ∧ increasing M f ∧ countably_subadditive M f" subsubsection✐‹tag important› ‹Lambda Systems› definition✐‹tag important› lambda_system :: "'a set ⇒ 'a set set ⇒ ('a set ⇒ ennreal) ⇒ 'a set set" where "lambda_system Ω M f = {l ∈ M. ∀x ∈ M. f (l ∩ x) + f ((Ω - l) ∩ x) = f x}" lemma (in algebra) lambda_system_eq: "lambda_system Ω M f = {l ∈ M. ∀x ∈ M. f (x ∩ l) + f (x - l) = f x}" proof - have [simp]: "⋀l x. l ∈ M ⟹ x ∈ M ⟹ (Ω - l) ∩ x = x - l" by (metis Int_Diff Int_absorb1 Int_commute sets_into_space) show ?thesis by (auto simp add: lambda_system_def) (metis Int_commute)+ qed lemma (in algebra) lambda_system_empty: "positive M f ⟹ {} ∈ lambda_system Ω M f" by (auto simp add: positive_def lambda_system_eq) lemma lambda_system_sets: "x ∈ lambda_system Ω M f ⟹ x ∈ M" by (simp add: lambda_system_def) lemma (in algebra) lambda_system_Compl: fixes f:: "'a set ⇒ ennreal" assumes x: "x ∈ lambda_system Ω M f" shows "Ω - x ∈ lambda_system Ω M f" proof - have "x ⊆ Ω" by (metis sets_into_space lambda_system_sets x) hence "Ω - (Ω - x) = x" by (metis double_diff equalityE) with x show ?thesis by (force simp add: lambda_system_def ac_simps) qed lemma (in algebra) lambda_system_Int: fixes f:: "'a set ⇒ ennreal" assumes xl: "x ∈ lambda_system Ω M f" and yl: "y ∈ lambda_system Ω M f" shows "x ∩ y ∈ lambda_system Ω M f" proof - from xl yl show ?thesis proof (auto simp add: positive_def lambda_system_eq Int) fix u assume x: "x ∈ M" and y: "y ∈ M" and u: "u ∈ M" and fx: "∀z∈M. f (z ∩ x) + f (z - x) = f z" and fy: "∀z∈M. f (z ∩ y) + f (z - y) = f z" have "u - x ∩ y ∈ M" by (metis Diff Diff_Int Un u x y) moreover have "(u - (x ∩ y)) ∩ y = u ∩ y - x" by blast moreover have "u - x ∩ y - y = u - y" by blast ultimately have ey: "f (u - x ∩ y) = f (u ∩ y - x) + f (u - y)" using fy by force have "f (u ∩ (x ∩ y)) + f (u - x ∩ y) = (f (u ∩ (x ∩ y)) + f (u ∩ y - x)) + f (u - y)" by (simp add: ey ac_simps) also have "... = (f ((u ∩ y) ∩ x) + f (u ∩ y - x)) + f (u - y)" by (simp add: Int_ac) also have "... = f (u ∩ y) + f (u - y)" using fx [THEN bspec, of "u ∩ y"] Int y u by force also have "... = f u" by (metis fy u) finally show "f (u ∩ (x ∩ y)) + f (u - x ∩ y) = f u" . qed qed lemma (in algebra) lambda_system_Un: fixes f:: "'a set ⇒ ennreal" assumes xl: "x ∈ lambda_system Ω M f" and yl: "y ∈ lambda_system Ω M f" shows "x ∪ y ∈ lambda_system Ω M f" proof - have "(Ω - x) ∩ (Ω - y) ∈ M" by (metis Diff_Un Un compl_sets lambda_system_sets xl yl) moreover have "x ∪ y = Ω - ((Ω - x) ∩ (Ω - y))" by auto (metis subsetD lambda_system_sets sets_into_space xl yl)+ ultimately show ?thesis by (metis lambda_system_Compl lambda_system_Int xl yl) qed lemma (in algebra) lambda_system_algebra: "positive M f ⟹ algebra Ω (lambda_system Ω M f)" apply (auto simp add: algebra_iff_Un) apply (metis lambda_system_sets subsetD sets_into_space) apply (metis lambda_system_empty) apply (metis lambda_system_Compl) apply (metis lambda_system_Un) done lemma (in algebra) lambda_system_strong_additive: assumes z: "z ∈ M" and disj: "x ∩ y = {}" and xl: "x ∈ lambda_system Ω M f" and yl: "y ∈ lambda_system Ω M f" shows "f (z ∩ (x ∪ y)) = f (z ∩ x) + f (z ∩ y)" proof - have "z ∩ x = (z ∩ (x ∪ y)) ∩ x" using disj by blast moreover have "z ∩ y = (z ∩ (x ∪ y)) - x" using disj by blast moreover have "(z ∩ (x ∪ y)) ∈ M" by (metis Int Un lambda_system_sets xl yl z) ultimately show ?thesis using xl yl by (simp add: lambda_system_eq) qed lemma (in algebra) lambda_system_additive: "additive (lambda_system Ω M f) f" proof (auto simp add: additive_def) fix x and y assume disj: "x ∩ y = {}" and xl: "x ∈ lambda_system Ω M f" and yl: "y ∈ lambda_system Ω M f" hence "x ∈ M" "y ∈ M" by (blast intro: lambda_system_sets)+ thus "f (x ∪ y) = f x + f y" using lambda_system_strong_additive [OF top disj xl yl] by (simp add: Un) qed lemma lambda_system_increasing: "increasing M f ⟹ increasing (lambda_system Ω M f) f" by (simp add: increasing_def lambda_system_def) lemma lambda_system_positive: "positive M f ⟹ positive (lambda_system Ω M f) f" by (simp add: positive_def lambda_system_def) lemma (in algebra) lambda_system_strong_sum: fixes A:: "nat ⇒ 'a set" and f :: "'a set ⇒ ennreal" assumes f: "positive M f" and a: "a ∈ M" and A: "range A ⊆ lambda_system Ω M f" and disj: "disjoint_family A" shows "(∑i = 0..<n. f (a ∩A i)) = f (a ∩ (⋃i∈{0..<n}. A i))" proof (induct n) case 0 show ?case using f by (simp add: positive_def) next case (Suc n) have 2: "A n ∩ ⋃ (A ` {0..<n}) = {}" using disj by (force simp add: disjoint_family_on_def neq_iff) have 3: "A n ∈ lambda_system Ω M f" using A by blast interpret l: algebra Ω "lambda_system Ω M f" using f by (rule lambda_system_algebra) have 4: "⋃ (A ` {0..<n}) ∈ lambda_system Ω M f" using A l.UNION_in_sets by simp from Suc.hyps show ?case by (simp add: atLeastLessThanSuc lambda_system_strong_additive [OF a 2 3 4]) qed proposition (in sigma_algebra) lambda_system_caratheodory: assumes oms: "outer_measure_space M f" and A: "range A ⊆ lambda_system Ω M f" and disj: "disjoint_family A" shows "(⋃i. A i) ∈ lambda_system Ω M f ∧ (∑i. f (A i)) = f (⋃i. A i)" proof - have pos: "positive M f" and inc: "increasing M f" and csa: "countably_subadditive M f" by (metis oms outer_measure_space_def)+ have sa: "subadditive M f" by (metis countably_subadditive_subadditive csa pos) have A': "⋀S. A`S ⊆ (lambda_system Ω M f)" using A by auto interpret ls: algebra Ω "lambda_system Ω M f" using pos by (rule lambda_system_algebra) have A'': "range A ⊆ M" by (metis A image_subset_iff lambda_system_sets) have U_in: "(⋃i. A i) ∈ M" by (metis A'' countable_UN) have U_eq: "f (⋃i. A i) = (∑i. f (A i))" proof (rule antisym) show "f (⋃i. A i) ≤ (∑i. f (A i))" using csa[unfolded countably_subadditive_def] A'' disj U_in by auto have dis: "⋀N. disjoint_family_on A {..<N}" by (intro disjoint_family_on_mono[OF _ disj]) auto show "(∑i. f (A i)) ≤ f (⋃i. A i)" using ls.additive_sum [OF lambda_system_positive[OF pos] lambda_system_additive _ A' dis] A'' by (intro suminf_le_const[OF summableI]) (auto intro!: increasingD[OF inc] countable_UN) qed have "f (a ∩ (⋃i. A i)) + f (a - (⋃i. A i)) = f a" if a [iff]: "a ∈ M" for a proof (rule antisym) have "range (λi. a ∩ A i) ⊆ M" using A'' by blast moreover have "disjoint_family (λi. a ∩ A i)" using disj by (auto simp add: disjoint_family_on_def) moreover have "a ∩ (⋃i. A i) ∈ M" by (metis Int U_in a) ultimately have "f (a ∩ (⋃i. A i)) ≤ (∑i. f (a ∩ A i))" using csa[unfolded countably_subadditive_def, rule_format, of "(λi. a ∩ A i)"] by (simp add: o_def) hence "f (a ∩ (⋃i. A i)) + f (a - (⋃i. A i)) ≤ (∑i. f (a ∩ A i)) + f (a - (⋃i. A i))" by (rule add_right_mono) also have "… ≤ f a" proof (intro ennreal_suminf_bound_add) fix n have UNION_in: "(⋃i∈{0..<n}. A i) ∈ M" by (metis A'' UNION_in_sets) have le_fa: "f (⋃ (A ` {0..<n}) ∩ a) ≤ f a" using A'' by (blast intro: increasingD [OF inc] A'' UNION_in_sets) have ls: "(⋃i∈{0..<n}. A i) ∈ lambda_system Ω M f" using ls.UNION_in_sets by (simp add: A) hence eq_fa: "f a = f (a ∩ (⋃i∈{0..<n}. A i)) + f (a - (⋃i∈{0..<n}. A i))" by (simp add: lambda_system_eq UNION_in) have "f (a - (⋃i. A i)) ≤ f (a - (⋃i∈{0..<n}. A i))" by (blast intro: increasingD [OF inc] UNION_in U_in) thus "(∑i<n. f (a ∩ A i)) + f (a - (⋃i. A i)) ≤ f a" by (simp add: lambda_system_strong_sum pos A disj eq_fa add_left_mono atLeast0LessThan[symmetric]) qed finally show "f (a ∩ (⋃i. A i)) + f (a - (⋃i. A i)) ≤ f a" by simp next have "f a ≤ f (a ∩ (⋃i. A i) ∪ (a - (⋃i. A i)))" by (blast intro: increasingD [OF inc] U_in) also have "... ≤ f (a ∩ (⋃i. A i)) + f (a - (⋃i. A i))" by (blast intro: subadditiveD [OF sa] U_in) finally show "f a ≤ f (a ∩ (⋃i. A i)) + f (a - (⋃i. A i))" . qed thus ?thesis by (simp add: lambda_system_eq sums_iff U_eq U_in) qed proposition (in sigma_algebra) caratheodory_lemma: assumes oms: "outer_measure_space M f" defines "L ≡ lambda_system Ω M f" shows "measure_space Ω L f" proof - have pos: "positive M f" by (metis oms outer_measure_space_def) have alg: "algebra Ω L" using lambda_system_algebra [of f, OF pos] by (simp add: algebra_iff_Un L_def) then have "sigma_algebra Ω L" using lambda_system_caratheodory [OF oms] by (simp add: sigma_algebra_disjoint_iff L_def) moreover have "countably_additive L f" "positive L f" using pos lambda_system_caratheodory [OF oms] by (auto simp add: lambda_system_sets L_def countably_additive_def positive_def) ultimately show ?thesis using pos by (simp add: measure_space_def) qed definition✐‹tag important› outer_measure :: "'a set set ⇒ ('a set ⇒ ennreal) ⇒ 'a set ⇒ ennreal" where "outer_measure M f X = (INF A∈{A. range A ⊆ M ∧ disjoint_family A ∧ X ⊆ (⋃i. A i)}. ∑i. f (A i))" lemma (in ring_of_sets) outer_measure_agrees: assumes posf: "positive M f" and ca: "countably_additive M f" and s: "s ∈ M" shows "outer_measure M f s = f s" unfolding outer_measure_def proof (safe intro!: antisym INF_greatest) fix A :: "nat ⇒ 'a set" assume A: "range A ⊆ M" and dA: "disjoint_family A" and sA: "s ⊆ (⋃x. A x)" have inc: "increasing M f" by (metis additive_increasing ca countably_additive_additive posf) have "f s = f (⋃i. A i ∩ s)" using sA by (auto simp: Int_absorb1) also have "… = (∑i. f (A i ∩ s))" using sA dA A s by (intro ca[unfolded countably_additive_def, rule_format, symmetric]) (auto simp: Int_absorb1 disjoint_family_on_def) also have "... ≤ (∑i. f (A i))" using A s by (auto intro!: suminf_le increasingD[OF inc]) finally show "f s ≤ (∑i. f (A i))" . next have "(∑i. f (if i = 0 then s else {})) ≤ f s" using positiveD1[OF posf] by (subst suminf_finite[of "{0}"]) auto with s show "(INF A∈{A. range A ⊆ M ∧ disjoint_family A ∧ s ⊆ ⋃(A ` UNIV)}. ∑i. f (A i)) ≤ f s" by (intro INF_lower2[of "λi. if i = 0 then s else {}"]) (auto simp: disjoint_family_on_def) qed lemma outer_measure_empty: "positive M f ⟹ {} ∈ M ⟹ outer_measure M f {} = 0" unfolding outer_measure_def by (intro antisym INF_lower2[of "λ_. {}"]) (auto simp: disjoint_family_on_def positive_def) lemma (in ring_of_sets) positive_outer_measure: assumes "positive M f" shows "positive (Pow Ω) (outer_measure M f)" unfolding positive_def by (auto simp: assms outer_measure_empty) lemma (in ring_of_sets) increasing_outer_measure: "increasing (Pow Ω) (outer_measure M f)" by (force simp: increasing_def outer_measure_def intro!: INF_greatest intro: INF_lower) lemma (in ring_of_sets) outer_measure_le: assumes pos: "positive M f" and inc: "increasing M f" and A: "range A ⊆ M" and X: "X ⊆ (⋃i. A i)" shows "outer_measure M f X ≤ (∑i. f (A i))" unfolding outer_measure_def proof (safe intro!: INF_lower2[of "disjointed A"] del: subsetI) show dA: "range (disjointed A) ⊆ M" by (auto intro!: A range_disjointed_sets) have "∀n. f (disjointed A n) ≤ f (A n)" by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A) then show "(∑i. f (disjointed A i)) ≤ (∑i. f (A i))" by (blast intro!: suminf_le) qed (auto simp: X UN_disjointed_eq disjoint_family_disjointed) lemma (in ring_of_sets) outer_measure_close: "outer_measure M f X < e ⟹ ∃A. range A ⊆ M ∧ disjoint_family A ∧ X ⊆ (⋃i. A i) ∧ (∑i. f (A i)) < e" unfolding outer_measure_def INF_less_iff by auto lemma (in ring_of_sets) countably_subadditive_outer_measure: assumes posf: "positive M f" and inc: "increasing M f" shows "countably_subadditive (Pow Ω) (outer_measure M f)" proof (simp add: countably_subadditive_def, safe) fix A :: "nat ⇒ _" assume A: "range A ⊆ Pow (Ω)" and sb: "(⋃i. A i) ⊆ Ω" let ?O = "outer_measure M f" show "?O (⋃i. A i) ≤ (∑n. ?O (A n))" proof (rule ennreal_le_epsilon) fix b and e :: real assume "0 < e" "(∑n. outer_measure M f (A n)) < top" then have *: "⋀n. outer_measure M f (A n) < outer_measure M f (A n) + e * (1/2)^Suc n" by (auto simp add: less_top dest!: ennreal_suminf_lessD) obtain B where B: "⋀n. range (B n) ⊆ M" and sbB: "⋀n. A n ⊆ (⋃i. B n i)" and Ble: "⋀n. (∑i. f (B n i)) ≤ ?O (A n) + e * (1/2)^(Suc n)" by (metis less_imp_le outer_measure_close[OF *]) define C where "C = case_prod B o prod_decode" from B have B_in_M: "⋀i j. B i j ∈ M" by (rule range_subsetD) then have C: "range C ⊆ M" by (auto simp add: C_def split_def) have A_C: "(⋃i. A i) ⊆ (⋃i. C i)" using sbB by (auto simp add: C_def subset_eq) (metis prod.case prod_encode_inverse) have "?O (⋃i. A i) ≤ ?O (⋃i. C i)" using A_C A C by (intro increasing_outer_measure[THEN increasingD]) (auto dest!: sets_into_space) also have "… ≤ (∑i. f (C i))" using C by (intro outer_measure_le[OF posf inc]) auto also have "… = (∑n. ∑i. f (B n i))" using B_in_M unfolding C_def comp_def by (intro suminf_ennreal_2dimen) auto also have "… ≤ (∑n. ?O (A n) + e * (1/2) ^ Suc n)" using B_in_M by (intro suminf_le suminf_nonneg allI Ble) auto also have "... = (∑n. ?O (A n)) + (∑n. ennreal e * ennreal ((1/2) ^ Suc n))" using ‹0 < e› by (subst suminf_add[symmetric]) (auto simp del: ennreal_suminf_cmult simp add: ennreal_mult[symmetric]) also have "… = (∑n. ?O (A n)) + e" unfolding ennreal_suminf_cmult by (subst suminf_ennreal_eq[OF zero_le_power power_half_series]) auto finally show "?O (⋃i. A i) ≤ (∑n. ?O (A n)) + e" . qed qed lemma (in ring_of_sets) outer_measure_space_outer_measure: "positive M f ⟹ increasing M f ⟹ outer_measure_space (Pow Ω) (outer_measure M f)" by (simp add: outer_measure_space_def positive_outer_measure increasing_outer_measure countably_subadditive_outer_measure) lemma (in ring_of_sets) algebra_subset_lambda_system: assumes posf: "positive M f" and inc: "increasing M f" and add: "additive M f" shows "M ⊆ lambda_system Ω (Pow Ω) (outer_measure M f)" proof (auto dest: sets_into_space simp add: algebra.lambda_system_eq [OF algebra_Pow]) fix x s assume x: "x ∈ M" and s: "s ⊆ Ω" have [simp]: "⋀x. x ∈ M ⟹ s ∩ (Ω - x) = s - x" using s by blast have "outer_measure M f (s ∩ x) + outer_measure M f (s - x) ≤ outer_measure M f s" unfolding outer_measure_def[of M f s] proof (safe intro!: INF_greatest) fix A :: "nat ⇒ 'a set" assume A: "disjoint_family A" "range A ⊆ M" "s ⊆ (⋃i. A i)" have "outer_measure M f (s ∩ x) ≤ (∑i. f (A i ∩ x))" unfolding outer_measure_def proof (safe intro!: INF_lower2[of "λi. A i ∩ x"]) from A(1) show "disjoint_family (λi. A i ∩ x)" by (rule disjoint_family_on_bisimulation) auto qed (insert x A, auto) moreover have "outer_measure M f (s - x) ≤ (∑i. f (A i - x))" unfolding outer_measure_def proof (safe intro!: INF_lower2[of "λi. A i - x"]) from A(1) show "disjoint_family (λi. A i - x)" by (rule disjoint_family_on_bisimulation) auto qed (insert x A, auto) ultimately have "outer_measure M f (s ∩ x) + outer_measure M f (s - x) ≤ (∑i. f (A i ∩ x)) + (∑i. f (A i - x))" by (rule add_mono) also have "… = (∑i. f (A i ∩ x) + f (A i - x))" using A(2) x posf by (subst suminf_add) (auto simp: positive_def) also have "… = (∑i. f (A i))" using A x by (subst add[THEN additiveD, symmetric]) (auto intro!: arg_cong[where f=suminf] arg_cong[where f=f]) finally show "outer_measure M f (s ∩ x) + outer_measure M f (s - x) ≤ (∑i. f (A i))" . qed moreover have "outer_measure M f s ≤ outer_measure M f (s ∩ x) + outer_measure M f (s - x)" proof - have "outer_measure M f s = outer_measure M f ((s ∩ x) ∪ (s - x))" by (metis Un_Diff_Int Un_commute) also have "... ≤ outer_measure M f (s ∩ x) + outer_measure M f (s - x)" apply (rule subadditiveD) apply (rule ring_of_sets.countably_subadditive_subadditive [OF ring_of_sets_Pow]) apply (simp add: positive_def outer_measure_empty[OF posf]) apply (rule countably_subadditive_outer_measure) using s by (auto intro!: posf inc) finally show ?thesis . qed ultimately show "outer_measure M f (s ∩ x) + outer_measure M f (s - x) = outer_measure M f s" by (rule order_antisym) qed lemma measure_down: "measure_space Ω N μ ⟹ sigma_algebra Ω M ⟹ M ⊆ N ⟹ measure_space Ω M μ" by (auto simp add: measure_space_def positive_def countably_additive_def subset_eq) subsection ‹Caratheodory's theorem› theorem (in ring_of_sets) caratheodory': assumes posf: "positive M f" and ca: "countably_additive M f" shows "∃μ :: 'a set ⇒ ennreal. (∀s ∈ M. μ s = f s) ∧ measure_space Ω (sigma_sets Ω M) μ" proof - have inc: "increasing M f" by (metis additive_increasing ca countably_additive_additive posf) let ?O = "outer_measure M f" define ls where "ls = lambda_system Ω (Pow Ω) ?O" have mls: "measure_space Ω ls ?O" using sigma_algebra.caratheodory_lemma [OF sigma_algebra_Pow outer_measure_space_outer_measure [OF posf inc]] by (simp add: ls_def) hence sls: "sigma_algebra Ω ls" by (simp add: measure_space_def) have "M ⊆ ls" by (simp add: ls_def) (metis ca posf inc countably_additive_additive algebra_subset_lambda_system) hence sgs_sb: "sigma_sets (Ω) (M) ⊆ ls" using sigma_algebra.sigma_sets_subset [OF sls, of "M"] by simp have "measure_space Ω (sigma_sets Ω M) ?O" by (rule measure_down [OF mls], rule sigma_algebra_sigma_sets) (simp_all add: sgs_sb space_closed) thus ?thesis using outer_measure_agrees [OF posf ca] by (intro exI[of _ ?O]) auto qed lemma (in ring_of_sets) caratheodory_empty_continuous: assumes f: "positive M f" "additive M f" and fin: "⋀A. A ∈ M ⟹ f A ≠ ∞" assumes cont: "⋀A. range A ⊆ M ⟹ decseq A ⟹ (⋂i. A i) = {} ⟹ (λi. f (A i)) ⇢ 0" shows "∃μ :: 'a set ⇒ ennreal. (∀s ∈ M. μ s = f s) ∧ measure_space Ω (sigma_sets Ω M) μ" proof (intro caratheodory' empty_continuous_imp_countably_additive f) show "∀A∈M. f A ≠ ∞" using fin by auto qed (rule cont) subsection ‹Volumes› definition✐‹tag important› volume :: "'a set set ⇒ ('a set ⇒ ennreal) ⇒ bool" where "volume M f ⟷ (f {} = 0) ∧ (∀a∈M. 0 ≤ f a) ∧ (∀C⊆M. disjoint C ⟶ finite C ⟶ ⋃C ∈ M ⟶ f (⋃C) = (∑c∈C. f c))" lemma volumeI: assumes "f {} = 0" assumes "⋀a. a ∈ M ⟹ 0 ≤ f a" assumes "⋀C. C ⊆ M ⟹ disjoint C ⟹ finite C ⟹ ⋃C ∈ M ⟹ f (⋃C) = (∑c∈C. f c)" shows "volume M f" using assms by (auto simp: volume_def) lemma volume_positive: "volume M f ⟹ a ∈ M ⟹ 0 ≤ f a" by (auto simp: volume_def) lemma volume_empty: "volume M f ⟹ f {} = 0" by (auto simp: volume_def) proposition volume_finite_additive: assumes "volume M f" assumes A: "⋀i. i ∈ I ⟹ A i ∈ M" "disjoint_family_on A I" "finite I" "⋃(A ` I) ∈ M" shows "f (⋃(A ` I)) = (∑i∈I. f (A i))" proof - have "A`I ⊆ M" "disjoint (A`I)" "finite (A`I)" "⋃(A`I) ∈ M" using A by (auto simp: disjoint_family_on_disjoint_image) with ‹volume M f› have "f (⋃(A`I)) = (∑a∈A`I. f a)" unfolding volume_def by blast also have "… = (∑i∈I. f (A i))" proof (subst sum.reindex_nontrivial) fix i j assume "i ∈ I" "j ∈ I" "i ≠ j" "A i = A j" with ‹disjoint_family_on A I› have "A i = {}" by (auto simp: disjoint_family_on_def) then show "f (A i) = 0" using volume_empty[OF ‹volume M f›] by simp qed (auto intro: ‹finite I›) finally show "f (⋃(A ` I)) = (∑i∈I. f (A i))" by simp qed lemma (in ring_of_sets) volume_additiveI: assumes pos: "⋀a. a ∈ M ⟹ 0 ≤ μ a" assumes [simp]: "μ {} = 0" assumes add: "⋀a b. a ∈ M ⟹ b ∈ M ⟹ a ∩ b = {} ⟹ μ (a ∪ b) = μ a + μ b" shows "volume M μ" proof (unfold volume_def, safe) fix C assume "finite C" "C ⊆ M" "disjoint C" then show "μ (⋃C) = sum μ C" proof (induct C) case (insert c C) from insert(1,2,4,5) have "μ (⋃(insert c C)) = μ c + μ (⋃C)" by (auto intro!: add simp: disjoint_def) with insert show ?case by (simp add: disjoint_def) qed simp qed fact+ proposition (in semiring_of_sets) extend_volume: assumes "volume M μ" shows "∃μ'. volume generated_ring μ' ∧ (∀a∈M. μ' a = μ a)" proof - let ?R = generated_ring have "∀a∈?R. ∃m. ∃C⊆M. a = ⋃C ∧ finite C ∧ disjoint C ∧ m = (∑c∈C. μ c)" by (auto simp: generated_ring_def) from bchoice[OF this] obtain μ' where μ'_spec: "∀x∈generated_ring. ∃C⊆M. x = ⋃ C ∧ finite C ∧ disjoint C ∧ μ' x = sum μ C" by blast { fix C assume C: "C ⊆ M" "finite C" "disjoint C" fix D assume D: "D ⊆ M" "finite D" "disjoint D" assume "⋃C = ⋃D" have "(∑d∈D. μ d) = (∑d∈D. ∑c∈C. μ (c ∩ d))" proof (intro sum.cong refl) fix d assume "d ∈ D" have Un_eq_d: "(⋃c∈C. c ∩ d) = d" using ‹d ∈ D› ‹⋃C = ⋃D› by auto moreover have "μ (⋃c∈C. c ∩ d) = (∑c∈C. μ (c ∩ d))" proof (rule volume_finite_additive) { fix c assume "c ∈ C" then show "c ∩ d ∈ M" using C D ‹d ∈ D› by auto } show "(⋃a∈C. a ∩ d) ∈ M" unfolding Un_eq_d using ‹d ∈ D› D by auto show "disjoint_family_on (λa. a ∩ d) C" using ‹disjoint C› by (auto simp: disjoint_family_on_def disjoint_def) qed fact+ ultimately show "μ d = (∑c∈C. μ (c ∩ d))" by simp qed } note split_sum = this { fix C assume C: "C ⊆ M" "finite C" "disjoint C" fix D assume D: "D ⊆ M" "finite D" "disjoint D" assume "⋃C = ⋃D" with split_sum[OF C D] split_sum[OF D C] have "(∑d∈D. μ d) = (∑c∈C. μ c)" by (simp, subst sum.swap, simp add: ac_simps) } note sum_eq = this { fix C assume C: "C ⊆ M" "finite C" "disjoint C" then have "⋃C ∈ ?R" by (auto simp: generated_ring_def) with μ'_spec[THEN bspec, of "⋃C"] obtain D where D: "D ⊆ M" "finite D" "disjoint D" "⋃C = ⋃D" and "μ' (⋃C) = (∑d∈D. μ d)" by auto with sum_eq[OF C D] have "μ' (⋃C) = (∑c∈C. μ c)" by simp } note μ' = this show ?thesis proof (intro exI conjI ring_of_sets.volume_additiveI[OF generating_ring] ballI) fix a assume "a ∈ M" with μ'[of "{a}"] show "μ' a = μ a" by (simp add: disjoint_def) next fix a assume "a ∈ ?R" then obtain Ca where Ca: "finite Ca" "disjoint Ca" "Ca ⊆ M" "a = ⋃ Ca" .. with μ'[of Ca] ‹volume M μ›[THEN volume_positive] show "0 ≤ μ' a" by (auto intro!: sum_nonneg) next show "μ' {} = 0" using μ'[of "{}"] by auto next fix a b assume "a ∈ ?R" "b ∈ ?R" then obtain Ca Cb where Ca: "finite Ca" "disjoint Ca" "Ca ⊆ M" "a = ⋃ Ca" and Cb: "finite Cb" "disjoint Cb" "Cb ⊆ M" "b = ⋃ Cb" by (meson generated_ringE) assume "a ∩ b = {}" with Ca Cb have "Ca ∩ Cb ⊆ {{}}" by auto then have C_Int_cases: "Ca ∩ Cb = {{}} ∨ Ca ∩ Cb = {}" by auto from ‹a ∩ b = {}› have "μ' (⋃(Ca ∪ Cb)) = (∑c∈Ca ∪ Cb. μ c)" using Ca Cb by (intro μ') (auto intro!: disjoint_union) also have "… = (∑c∈Ca ∪ Cb. μ c) + (∑c∈Ca ∩ Cb. μ c)" using C_Int_cases volume_empty[OF ‹volume M μ›] by (elim disjE) simp_all also have "… = (∑c∈Ca. μ c) + (∑c∈Cb. μ c)" using Ca Cb by (simp add: sum.union_inter) also have "… = μ' a + μ' b" using Ca Cb by (simp add: μ') finally show "μ' (a ∪ b) = μ' a + μ' b" using Ca Cb by simp qed qed subsubsection✐‹tag important› ‹Caratheodory on semirings› theorem (in semiring_of_sets) caratheodory: assumes pos: "positive M μ" and ca: "countably_additive M μ" shows "∃μ' :: 'a set ⇒ ennreal. (∀s ∈ M. μ' s = μ s) ∧ measure_space Ω (sigma_sets Ω M) μ'" proof - have "volume M μ" proof (rule volumeI) { fix a assume "a ∈ M" then show "0 ≤ μ a" using pos unfolding positive_def by auto } note p = this fix C assume sets_C: "C ⊆ M" "⋃C ∈ M" and "disjoint C" "finite C" have "∃F'. bij_betw F' {..<card C} C" by (rule finite_same_card_bij[OF _ ‹finite C›]) auto then obtain F' where "bij_betw F' {..<card C} C" .. then have F': "C = F' ` {..< card C}" "inj_on F' {..< card C}" by (auto simp: bij_betw_def) { fix i j assume *: "i < card C" "j < card C" "i ≠ j" with F' have "F' i ∈ C" "F' j ∈ C" "F' i ≠ F' j" unfolding inj_on_def by auto with ‹disjoint C›[THEN disjointD] have "F' i ∩ F' j = {}" by auto } note F'_disj = this define F where "F i = (if i < card C then F' i else {})" for i then have "disjoint_family F" using F'_disj by (auto simp: disjoint_family_on_def) moreover from F' have "(⋃i. F i) = ⋃C" by (auto simp add: F_def split: if_split_asm cong del: SUP_cong) moreover have sets_F: "⋀i. F i ∈ M" using F' sets_C by (auto simp: F_def) moreover note sets_C ultimately have "μ (⋃C) = (∑i. μ (F i))" using ca[unfolded countably_additive_def, THEN spec, of F] by auto also have "… = (∑i<card C. μ (F' i))" proof - have "(λi. if i ∈ {..< card C} then μ (F' i) else 0) sums (∑i<card C. μ (F' i))" by (rule sums_If_finite_set) auto also have "(λi. if i ∈ {..< card C} then μ (F' i) else 0) = (λi. μ (F i))" using pos by (auto simp: positive_def F_def) finally show "(∑i. μ (F i)) = (∑i<card C. μ (F' i))" by (simp add: sums_iff) qed also have "… = (∑c∈C. μ c)" using F'(2) by (subst (2) F') (simp add: sum.reindex) finally show "μ (⋃C) = (∑c∈C. μ c)" . next show "μ {} = 0" using ‹positive M μ› by (rule positiveD1) qed from extend_volume[OF this] obtain μ_r where V: "volume generated_ring μ_r" "⋀a. a ∈ M ⟹ μ a = μ_r a" by auto interpret G: ring_of_sets Ω generated_ring by (rule generating_ring) have pos: "positive generated_ring μ_r" using V unfolding positive_def by (auto simp: positive_def intro!: volume_positive volume_empty) have "countably_additive generated_ring μ_r" proof (rule countably_additiveI) fix A' :: "nat ⇒ 'a set" assume A': "range A' ⊆ generated_ring" "disjoint_family A'" and Un_A: "(⋃i. A' i) ∈ generated_ring" obtain C' where C': "finite C'" "disjoint C'" "C' ⊆ M" "⋃ (range A') = ⋃ C'" using generated_ringE[OF Un_A] by auto { fix c assume "c ∈ C'" moreover define A where [abs_def]: "A i = A' i ∩ c" for i ultimately have A: "range A ⊆ generated_ring" "disjoint_family A" and Un_A: "(⋃i. A i) ∈ generated_ring" using A' C' by (auto intro!: G.Int G.finite_Union intro: generated_ringI_Basic simp: disjoint_family_on_def) from A C' ‹c ∈ C'› have UN_eq: "(⋃i. A i) = c" by (auto simp: A_def) have "∀i::nat. ∃f::nat ⇒ 'a set. μ_r (A i) = (∑j. μ_r (f j)) ∧ disjoint_family f ∧ ⋃(range f) = A i ∧ (∀j. f j ∈ M)" (is "∀i. ?P i") proof fix i from A have Ai: "A i ∈ generated_ring" by auto from generated_ringE[OF this] obtain C where C: "finite C" "disjoint C" "C ⊆ M" "A i = ⋃ C" by auto have "∃F'. bij_betw F' {..<card C} C" by (rule finite_same_card_bij[OF _ ‹finite C›]) auto then obtain F where F: "bij_betw F {..<card C} C" .. define f where [abs_def]: "f i = (if i < card C then F i else {})" for i then have f: "bij_betw f {..< card C} C" by (intro bij_betw_cong[THEN iffD1, OF _ F]) auto with C have "∀j. f j ∈ M" by (auto simp: Pi_iff f_def dest!: bij_betw_imp_funcset) moreover from f C have d_f: "disjoint_family_on f {..<card C}" by (intro disjoint_image_disjoint_family_on) (auto simp: bij_betw_def) then have "disjoint_family f" by (auto simp: disjoint_family_on_def f_def) moreover have Ai_eq: "A i = (⋃x<card C. f x)" using f C Ai unfolding bij_betw_def by auto then have "⋃(range f) = A i" using f by (auto simp add: f_def) moreover { have "(∑j. μ_r (f j)) = (∑j. if j ∈ {..< card C} then μ_r (f j) else 0)" using volume_empty[OF V(1)] by (auto intro!: arg_cong[where f=suminf] simp: f_def) also have "… = (∑j<card C. μ_r (f j))" by (rule sums_If_finite_set[THEN sums_unique, symmetric]) simp also have "… = μ_r (A i)" using C f[THEN bij_betw_imp_funcset] unfolding Ai_eq by (intro volume_finite_additive[OF V(1) _ d_f, symmetric]) (auto simp: Pi_iff Ai_eq intro: generated_ringI_Basic) finally have "μ_r (A i) = (∑j. μ_r (f j))" .. } ultimately show "?P i" by blast qed from choice[OF this] obtain f where f: "∀x. μ_r (A x) = (∑j. μ_r (f x j)) ∧ disjoint_family (f x) ∧ ⋃ (range (f x)) = A x ∧ (∀j. f x j ∈ M)" .. then have UN_f_eq: "(⋃i. case_prod f (prod_decode i)) = (⋃i. A i)" unfolding UN_extend_simps surj_prod_decode by (auto simp: set_eq_iff) have d: "disjoint_family (λi. case_prod f (prod_decode i))" unfolding disjoint_family_on_def proof (intro ballI impI) fix m n :: nat assume "m ≠ n" then have neq: "prod_decode m ≠ prod_decode n" using inj_prod_decode[of UNIV] by (auto simp: inj_on_def) show "case_prod f (prod_decode m) ∩ case_prod f (prod_decode n) = {}" proof cases assume "fst (prod_decode m) = fst (prod_decode n)" then show ?thesis using neq f by (fastforce simp: disjoint_family_on_def) next assume neq: "fst (prod_decode m) ≠ fst (prod_decode n)" have "case_prod f (prod_decode m) ⊆ A (fst (prod_decode m))" "case_prod f (prod_decode n) ⊆ A (fst (prod_decode n))" using f[THEN spec, of "fst (prod_decode m)"] using f[THEN spec, of "fst (prod_decode n)"] by (auto simp: set_eq_iff) with f A neq show ?thesis by (fastforce simp: disjoint_family_on_def subset_eq set_eq_iff) qed qed from f have "(∑n. μ_r (A n)) = (∑n. μ_r (case_prod f (prod_decode n)))" by (intro suminf_ennreal_2dimen[symmetric] generated_ringI_Basic) (auto split: prod.split) also have "… = (∑n. μ (case_prod f (prod_decode n)))" using f V(2) by (auto intro!: arg_cong[where f=suminf] split: prod.split) also have "… = μ (⋃i. case_prod f (prod_decode i))" using f ‹c ∈ C'› C' by (intro ca[unfolded countably_additive_def, rule_format]) (auto split: prod.split simp: UN_f_eq d UN_eq) finally have "(∑n. μ_r (A' n ∩ c)) = μ c" using UN_f_eq UN_eq by (simp add: A_def) } note eq = this have "(∑n. μ_r (A' n)) = (∑n. ∑c∈C'. μ_r (A' n ∩ c))" using C' A' by (subst volume_finite_additive[symmetric, OF V(1)]) (auto simp: disjoint_def disjoint_family_on_def intro!: G.Int G.finite_Union arg_cong[where f="λX. suminf (λi. μ_r (X i))"] ext intro: generated_ringI_Basic) also have "… = (∑c∈C'. ∑n. μ_r (A' n ∩ c))" using C' A' by (intro suminf_sum G.Int G.finite_Union) (auto intro: generated_ringI_Basic) also have "… = (∑c∈C'. μ_r c)" using eq V C' by (auto intro!: sum.cong) also have "… = μ_r (⋃C')" using C' Un_A by (subst volume_finite_additive[symmetric, OF V(1)]) (auto simp: disjoint_family_on_def disjoint_def intro: generated_ringI_Basic) finally show "(∑n. μ_r (A' n)) = μ_r (⋃i. A' i)" using C' by simp qed obtain μ' where "(∀s∈generated_ring. μ' s = μ_r s) ∧ measure_space Ω (sigma_sets Ω generated_ring) μ'" using G.caratheodory'[OF pos ‹countably_additive generated_ring μ_r›] by auto with V show ?thesis unfolding sigma_sets_generated_ring_eq by (intro exI[of _ μ']) (auto intro: generated_ringI_Basic) qed lemma extend_measure_caratheodory: fixes G :: "'i ⇒ 'a set" assumes M: "M = extend_measure Ω I G μ" assumes "i ∈ I" assumes "semiring_of_sets Ω (G ` I)" assumes empty: "⋀i. i ∈ I ⟹ G i = {} ⟹ μ i = 0" assumes inj: "⋀i j. i ∈ I ⟹ j ∈ I ⟹ G i = G j ⟹ μ i = μ j" assumes nonneg: "⋀i. i ∈ I ⟹ 0 ≤ μ i" assumes add: "⋀A::nat ⇒ 'i. ⋀j. A ∈ UNIV → I ⟹ j ∈ I ⟹ disjoint_family (G ∘ A) ⟹ (⋃i. G (A i)) = G j ⟹ (∑n. μ (A n)) = μ j" shows "emeasure M (G i) = μ i" proof - interpret semiring_of_sets Ω "G ` I" by fact have "∀g∈G`I. ∃i∈I. g = G i" by auto then obtain sel where sel: "⋀g. g ∈ G ` I ⟹ sel g ∈ I" "⋀g. g ∈ G ` I ⟹ G (sel g) = g" by metis have "∃μ'. (∀s∈G ` I. μ' s = μ (sel s)) ∧ measure_space Ω (sigma_sets Ω (G ` I)) μ'" proof (rule caratheodory) show "positive (G ` I) (λs. μ (sel s))" by (auto simp: positive_def intro!: empty sel nonneg) show "countably_additive (G ` I) (λs. μ (sel s))" proof (rule countably_additiveI) fix A :: "nat ⇒ 'a set" assume "range A ⊆ G ` I" "disjoint_family A" "(⋃i. A i) ∈ G ` I" then show "(∑i. μ (sel (A i))) = μ (sel (⋃i. A i))" by (intro add) (auto simp: sel image_subset_iff_funcset comp_def Pi_iff intro!: sel) qed qed then obtain μ' where μ': "∀s∈G ` I. μ' s = μ (sel s)" "measure_space Ω (sigma_sets Ω (G ` I)) μ'" by metis show ?thesis proof (rule emeasure_extend_measure[OF M]) { fix i assume "i ∈ I" then show "μ' (G i) = μ i" using μ' by (auto intro!: inj sel) } show "G ` I ⊆ Pow Ω" by (rule space_closed) then show "positive (sets M) μ'" "countably_additive (sets M) μ'" using μ' by (simp_all add: M sets_extend_measure measure_space_def) qed fact qed proposition extend_measure_caratheodory_pair: fixes G :: "'i ⇒ 'j ⇒ 'a set" assumes M: "M = extend_measure Ω {(a, b). P a b} (λ(a, b). G a b) (λ(a, b). μ a b)" assumes "P i j" assumes semiring: "semiring_of_sets Ω {G a b | a b. P a b}" assumes empty: "⋀i j. P i j ⟹ G i j = {} ⟹ μ i j = 0" assumes inj: "⋀i j k l. P i j ⟹ P k l ⟹ G i j = G k l ⟹ μ i j = μ k l" assumes nonneg: "⋀i j. P i j ⟹ 0 ≤ μ i j" assumes add: "⋀A::nat ⇒ 'i. ⋀B::nat ⇒ 'j. ⋀j k. (⋀n. P (A n) (B n)) ⟹ P j k ⟹ disjoint_family (λn. G (A n) (B n)) ⟹ (⋃i. G (A i) (B i)) = G j k ⟹ (∑n. μ (A n) (B n)) = μ j k" shows "emeasure M (G i j) = μ i j" proof - have "emeasure M ((λ(a, b). G a b) (i, j)) = (λ(a, b). μ a b) (i, j)" proof (rule extend_measure_caratheodory[OF M]) show "semiring_of_sets Ω ((λ(a, b). G a b) ` {(a, b). P a b})" using semiring by (simp add: image_def conj_commute) next fix A :: "nat ⇒ ('i × 'j)" and j assume "A ∈ UNIV → {(a, b). P a b}" "j ∈ {(a, b). P a b}" "disjoint_family ((λ(a, b). G a b) ∘ A)" "(⋃i. case A i of (a, b) ⇒ G a b) = (case j of (a, b) ⇒ G a b)" then show "(∑n. case A n of (a, b) ⇒ μ a b) = (case j of (a, b) ⇒ μ a b)" using add[of "λi. fst (A i)" "λi. snd (A i)" "fst j" "snd j"] by (simp add: split_beta' comp_def Pi_iff) qed (auto split: prod.splits intro: assms) then show ?thesis by simp qed end