src/HOL/Analysis/Caratheodory.thy
 author haftmann Thu Nov 22 10:06:31 2018 +0000 (8 months ago) changeset 69325 4b6ddc5989fc parent 69313 b021008c5397 child 69517 dc20f278e8f3 permissions -rw-r--r--
removed legacy input syntax
 hoelzl@63627 ` 1` ```(* Title: HOL/Analysis/Caratheodory.thy ``` hoelzl@42067 ` 2` ``` Author: Lawrence C Paulson ``` hoelzl@42067 ` 3` ``` Author: Johannes Hölzl, TU München ``` hoelzl@42067 ` 4` ```*) ``` hoelzl@42067 ` 5` ak2110@68833 ` 6` ```section%important \Caratheodory Extension Theorem\ ``` paulson@33271 ` 7` paulson@33271 ` 8` ```theory Caratheodory ``` hoelzl@47694 ` 9` ``` imports Measure_Space ``` paulson@33271 ` 10` ```begin ``` paulson@33271 ` 11` wenzelm@61808 ` 12` ```text \ ``` hoelzl@42067 ` 13` ``` Originally from the Hurd/Coble measure theory development, translated by Lawrence Paulson. ``` wenzelm@61808 ` 14` ```\ ``` hoelzl@42067 ` 15` ak2110@68833 ` 16` ```lemma%unimportant suminf_ennreal_2dimen: ``` hoelzl@62975 ` 17` ``` fixes f:: "nat \ nat \ ennreal" ``` hoelzl@41981 ` 18` ``` assumes "\m. g m = (\n. f (m,n))" ``` hoelzl@41981 ` 19` ``` shows "(\i. f (prod_decode i)) = suminf g" ``` hoelzl@41981 ` 20` ```proof - ``` hoelzl@41981 ` 21` ``` have g_def: "g = (\m. (\n. f (m,n)))" ``` hoelzl@41981 ` 22` ``` using assms by (simp add: fun_eq_iff) ``` nipkow@64267 ` 23` ``` have reindex: "\B. (\x\B. f (prod_decode x)) = sum f (prod_decode ` B)" ``` nipkow@64267 ` 24` ``` by (simp add: sum.reindex[OF inj_prod_decode] comp_def) ``` haftmann@69260 ` 25` ``` have "(SUP n. \i UNIV \ UNIV. \in sum f ({.. {..a b. sum f (prod_decode ` {.. sum f ({.. {.. ?M" ``` hoelzl@41981 ` 39` ``` by (auto intro!: Max_ge le_imp_less_Suc image_eqI[where x="prod_encode (a', b')"]) } ``` nipkow@64267 ` 40` ``` then have "sum f ({.. {.. sum f ?M" ``` lp15@65680 ` 41` ``` by (auto intro!: sum_mono2) ``` nipkow@64267 ` 42` ``` then show "\n. sum f ({.. {.. sum f (prod_decode ` {.. = (SUP p. \in. f (i, n))" ``` nipkow@64267 ` 46` ``` unfolding suminf_sum[OF summableI, symmetric] ``` haftmann@66804 ` 47` ``` by (simp add: suminf_eq_SUP SUP_pair sum.swap[of _ "{..< fst _}"]) ``` hoelzl@62975 ` 48` ``` finally show ?thesis unfolding g_def ``` hoelzl@62975 ` 49` ``` by (simp add: suminf_eq_SUP) ``` hoelzl@41981 ` 50` ```qed ``` hoelzl@41981 ` 51` ak2110@68833 ` 52` ```subsection%important \Characterizations of Measures\ ``` paulson@33271 ` 53` ak2110@68833 ` 54` ```definition%important outer_measure_space where ``` hoelzl@61273 ` 55` ``` "outer_measure_space M f \ positive M f \ increasing M f \ countably_subadditive M f" ``` paulson@33271 ` 56` ak2110@68833 ` 57` ```subsubsection%important \Lambda Systems\ ``` hoelzl@56994 ` 58` ak2110@68833 ` 59` ```definition%important lambda_system :: "'a set \ 'a set set \ ('a set \ ennreal) \ 'a set set" ``` hoelzl@62975 ` 60` ```where ``` hoelzl@61273 ` 61` ``` "lambda_system \ M f = {l \ M. \x \ M. f (l \ x) + f ((\ - l) \ x) = f x}" ``` paulson@33271 ` 62` ak2110@68833 ` 63` ```lemma%unimportant (in algebra) lambda_system_eq: ``` hoelzl@61273 ` 64` ``` "lambda_system \ M f = {l \ M. \x \ M. f (x \ l) + f (x - l) = f x}" ``` paulson@33271 ` 65` ```proof - ``` hoelzl@61273 ` 66` ``` have [simp]: "\l x. l \ M \ x \ M \ (\ - l) \ x = x - l" ``` huffman@37032 ` 67` ``` by (metis Int_Diff Int_absorb1 Int_commute sets_into_space) ``` paulson@33271 ` 68` ``` show ?thesis ``` huffman@37032 ` 69` ``` by (auto simp add: lambda_system_def) (metis Int_commute)+ ``` paulson@33271 ` 70` ```qed ``` paulson@33271 ` 71` ak2110@68833 ` 72` ```lemma%unimportant (in algebra) lambda_system_empty: "positive M f \ {} \ lambda_system \ M f" ``` hoelzl@42066 ` 73` ``` by (auto simp add: positive_def lambda_system_eq) ``` paulson@33271 ` 74` ak2110@68833 ` 75` ```lemma%unimportant lambda_system_sets: "x \ lambda_system \ M f \ x \ M" ``` hoelzl@41689 ` 76` ``` by (simp add: lambda_system_def) ``` paulson@33271 ` 77` ak2110@68833 ` 78` ```lemma%unimportant (in algebra) lambda_system_Compl: ``` hoelzl@62975 ` 79` ``` fixes f:: "'a set \ ennreal" ``` hoelzl@47694 ` 80` ``` assumes x: "x \ lambda_system \ M f" ``` hoelzl@47694 ` 81` ``` shows "\ - x \ lambda_system \ M f" ``` hoelzl@41689 ` 82` ```proof - ``` hoelzl@47694 ` 83` ``` have "x \ \" ``` hoelzl@41689 ` 84` ``` by (metis sets_into_space lambda_system_sets x) ``` hoelzl@47694 ` 85` ``` hence "\ - (\ - x) = x" ``` hoelzl@41689 ` 86` ``` by (metis double_diff equalityE) ``` hoelzl@41689 ` 87` ``` with x show ?thesis ``` hoelzl@41689 ` 88` ``` by (force simp add: lambda_system_def ac_simps) ``` hoelzl@41689 ` 89` ```qed ``` paulson@33271 ` 90` ak2110@68833 ` 91` ```lemma%unimportant (in algebra) lambda_system_Int: ``` hoelzl@62975 ` 92` ``` fixes f:: "'a set \ ennreal" ``` hoelzl@47694 ` 93` ``` assumes xl: "x \ lambda_system \ M f" and yl: "y \ lambda_system \ M f" ``` hoelzl@47694 ` 94` ``` shows "x \ y \ lambda_system \ M f" ``` hoelzl@41689 ` 95` ```proof - ``` hoelzl@41689 ` 96` ``` from xl yl show ?thesis ``` hoelzl@41689 ` 97` ``` proof (auto simp add: positive_def lambda_system_eq Int) ``` hoelzl@41689 ` 98` ``` fix u ``` hoelzl@47694 ` 99` ``` assume x: "x \ M" and y: "y \ M" and u: "u \ M" ``` hoelzl@47694 ` 100` ``` and fx: "\z\M. f (z \ x) + f (z - x) = f z" ``` hoelzl@47694 ` 101` ``` and fy: "\z\M. f (z \ y) + f (z - y) = f z" ``` hoelzl@47694 ` 102` ``` have "u - x \ y \ M" ``` hoelzl@41689 ` 103` ``` by (metis Diff Diff_Int Un u x y) ``` hoelzl@41689 ` 104` ``` moreover ``` hoelzl@41689 ` 105` ``` have "(u - (x \ y)) \ y = u \ y - x" by blast ``` hoelzl@41689 ` 106` ``` moreover ``` hoelzl@41689 ` 107` ``` have "u - x \ y - y = u - y" by blast ``` hoelzl@41689 ` 108` ``` ultimately ``` hoelzl@41689 ` 109` ``` have ey: "f (u - x \ y) = f (u \ y - x) + f (u - y)" using fy ``` hoelzl@41689 ` 110` ``` by force ``` hoelzl@41689 ` 111` ``` have "f (u \ (x \ y)) + f (u - x \ y) ``` hoelzl@41689 ` 112` ``` = (f (u \ (x \ y)) + f (u \ y - x)) + f (u - y)" ``` hoelzl@41689 ` 113` ``` by (simp add: ey ac_simps) ``` hoelzl@41689 ` 114` ``` also have "... = (f ((u \ y) \ x) + f (u \ y - x)) + f (u - y)" ``` hoelzl@41689 ` 115` ``` by (simp add: Int_ac) ``` hoelzl@41689 ` 116` ``` also have "... = f (u \ y) + f (u - y)" ``` hoelzl@41689 ` 117` ``` using fx [THEN bspec, of "u \ y"] Int y u ``` hoelzl@41689 ` 118` ``` by force ``` hoelzl@41689 ` 119` ``` also have "... = f u" ``` hoelzl@41689 ` 120` ``` by (metis fy u) ``` hoelzl@41689 ` 121` ``` finally show "f (u \ (x \ y)) + f (u - x \ y) = f u" . ``` paulson@33271 ` 122` ``` qed ``` hoelzl@41689 ` 123` ```qed ``` paulson@33271 ` 124` ak2110@68833 ` 125` ```lemma%unimportant (in algebra) lambda_system_Un: ``` hoelzl@62975 ` 126` ``` fixes f:: "'a set \ ennreal" ``` hoelzl@47694 ` 127` ``` assumes xl: "x \ lambda_system \ M f" and yl: "y \ lambda_system \ M f" ``` hoelzl@47694 ` 128` ``` shows "x \ y \ lambda_system \ M f" ``` paulson@33271 ` 129` ```proof - ``` hoelzl@47694 ` 130` ``` have "(\ - x) \ (\ - y) \ M" ``` hoelzl@38656 ` 131` ``` by (metis Diff_Un Un compl_sets lambda_system_sets xl yl) ``` paulson@33271 ` 132` ``` moreover ``` hoelzl@47694 ` 133` ``` have "x \ y = \ - ((\ - x) \ (\ - y))" ``` wenzelm@46731 ` 134` ``` by auto (metis subsetD lambda_system_sets sets_into_space xl yl)+ ``` paulson@33271 ` 135` ``` ultimately show ?thesis ``` hoelzl@38656 ` 136` ``` by (metis lambda_system_Compl lambda_system_Int xl yl) ``` paulson@33271 ` 137` ```qed ``` paulson@33271 ` 138` ak2110@68833 ` 139` ```lemma%unimportant (in algebra) lambda_system_algebra: ``` hoelzl@47694 ` 140` ``` "positive M f \ algebra \ (lambda_system \ M f)" ``` hoelzl@42065 ` 141` ``` apply (auto simp add: algebra_iff_Un) ``` paulson@33271 ` 142` ``` apply (metis lambda_system_sets set_mp sets_into_space) ``` paulson@33271 ` 143` ``` apply (metis lambda_system_empty) ``` paulson@33271 ` 144` ``` apply (metis lambda_system_Compl) ``` hoelzl@38656 ` 145` ``` apply (metis lambda_system_Un) ``` paulson@33271 ` 146` ``` done ``` paulson@33271 ` 147` ak2110@68833 ` 148` ```lemma%unimportant (in algebra) lambda_system_strong_additive: ``` hoelzl@47694 ` 149` ``` assumes z: "z \ M" and disj: "x \ y = {}" ``` hoelzl@47694 ` 150` ``` and xl: "x \ lambda_system \ M f" and yl: "y \ lambda_system \ M f" ``` paulson@33271 ` 151` ``` shows "f (z \ (x \ y)) = f (z \ x) + f (z \ y)" ``` hoelzl@41689 ` 152` ```proof - ``` hoelzl@41689 ` 153` ``` have "z \ x = (z \ (x \ y)) \ x" using disj by blast ``` hoelzl@41689 ` 154` ``` moreover ``` hoelzl@41689 ` 155` ``` have "z \ y = (z \ (x \ y)) - x" using disj by blast ``` hoelzl@41689 ` 156` ``` moreover ``` hoelzl@47694 ` 157` ``` have "(z \ (x \ y)) \ M" ``` hoelzl@41689 ` 158` ``` by (metis Int Un lambda_system_sets xl yl z) ``` hoelzl@41689 ` 159` ``` ultimately show ?thesis using xl yl ``` hoelzl@41689 ` 160` ``` by (simp add: lambda_system_eq) ``` hoelzl@41689 ` 161` ```qed ``` paulson@33271 ` 162` ak2110@68833 ` 163` ```lemma%unimportant (in algebra) lambda_system_additive: "additive (lambda_system \ M f) f" ``` hoelzl@41689 ` 164` ```proof (auto simp add: additive_def) ``` hoelzl@41689 ` 165` ``` fix x and y ``` hoelzl@41689 ` 166` ``` assume disj: "x \ y = {}" ``` hoelzl@47694 ` 167` ``` and xl: "x \ lambda_system \ M f" and yl: "y \ lambda_system \ M f" ``` hoelzl@47694 ` 168` ``` hence "x \ M" "y \ M" by (blast intro: lambda_system_sets)+ ``` hoelzl@41689 ` 169` ``` thus "f (x \ y) = f x + f y" ``` hoelzl@41689 ` 170` ``` using lambda_system_strong_additive [OF top disj xl yl] ``` hoelzl@41689 ` 171` ``` by (simp add: Un) ``` hoelzl@41689 ` 172` ```qed ``` paulson@33271 ` 173` ak2110@68833 ` 174` ```lemma%unimportant lambda_system_increasing: "increasing M f \ increasing (lambda_system \ M f) f" ``` hoelzl@38656 ` 175` ``` by (simp add: increasing_def lambda_system_def) ``` paulson@33271 ` 176` ak2110@68833 ` 177` ```lemma%unimportant lambda_system_positive: "positive M f \ positive (lambda_system \ M f) f" ``` hoelzl@41689 ` 178` ``` by (simp add: positive_def lambda_system_def) ``` hoelzl@41689 ` 179` ak2110@68833 ` 180` ```lemma%unimportant (in algebra) lambda_system_strong_sum: ``` hoelzl@62975 ` 181` ``` fixes A:: "nat \ 'a set" and f :: "'a set \ ennreal" ``` hoelzl@47694 ` 182` ``` assumes f: "positive M f" and a: "a \ M" ``` hoelzl@47694 ` 183` ``` and A: "range A \ lambda_system \ M f" ``` paulson@33271 ` 184` ``` and disj: "disjoint_family A" ``` paulson@33271 ` 185` ``` shows "(\i = 0..A i)) = f (a \ (\i\{0.. \ (A ` {0.. lambda_system \ M f" using A ``` paulson@33271 ` 193` ``` by blast ``` hoelzl@47694 ` 194` ``` interpret l: algebra \ "lambda_system \ M f" ``` hoelzl@42065 ` 195` ``` using f by (rule lambda_system_algebra) ``` haftmann@69325 ` 196` ``` have 4: "\ (A ` {0.. lambda_system \ M f" ``` hoelzl@42065 ` 197` ``` using A l.UNION_in_sets by simp ``` paulson@33271 ` 198` ``` from Suc.hyps show ?case ``` paulson@33271 ` 199` ``` by (simp add: atLeastLessThanSuc lambda_system_strong_additive [OF a 2 3 4]) ``` paulson@33271 ` 200` ```qed ``` paulson@33271 ` 201` ak2110@68833 ` 202` ```lemma%important (in sigma_algebra) lambda_system_caratheodory: ``` paulson@33271 ` 203` ``` assumes oms: "outer_measure_space M f" ``` hoelzl@47694 ` 204` ``` and A: "range A \ lambda_system \ M f" ``` paulson@33271 ` 205` ``` and disj: "disjoint_family A" ``` hoelzl@47694 ` 206` ``` shows "(\i. A i) \ lambda_system \ M f \ (\i. f (A i)) = f (\i. A i)" ``` ak2110@68833 ` 207` ```proof%unimportant - ``` hoelzl@41689 ` 208` ``` have pos: "positive M f" and inc: "increasing M f" ``` hoelzl@38656 ` 209` ``` and csa: "countably_subadditive M f" ``` paulson@33271 ` 210` ``` by (metis oms outer_measure_space_def)+ ``` paulson@33271 ` 211` ``` have sa: "subadditive M f" ``` hoelzl@38656 ` 212` ``` by (metis countably_subadditive_subadditive csa pos) ``` hoelzl@47694 ` 213` ``` have A': "\S. A`S \ (lambda_system \ M f)" using A ``` hoelzl@47694 ` 214` ``` by auto ``` hoelzl@47694 ` 215` ``` interpret ls: algebra \ "lambda_system \ M f" ``` hoelzl@42065 ` 216` ``` using pos by (rule lambda_system_algebra) ``` hoelzl@47694 ` 217` ``` have A'': "range A \ M" ``` paulson@33271 ` 218` ``` by (metis A image_subset_iff lambda_system_sets) ``` hoelzl@38656 ` 219` hoelzl@47694 ` 220` ``` have U_in: "(\i. A i) \ M" ``` huffman@37032 ` 221` ``` by (metis A'' countable_UN) ``` hoelzl@41981 ` 222` ``` have U_eq: "f (\i. A i) = (\i. f (A i))" ``` hoelzl@41689 ` 223` ``` proof (rule antisym) ``` hoelzl@41981 ` 224` ``` show "f (\i. A i) \ (\i. f (A i))" ``` hoelzl@41981 ` 225` ``` using csa[unfolded countably_subadditive_def] A'' disj U_in by auto ``` hoelzl@41981 ` 226` ``` have dis: "\N. disjoint_family_on A {..i. f (A i)) \ f (\i. A i)" ``` hoelzl@61273 ` 228` ``` using ls.additive_sum [OF lambda_system_positive[OF pos] lambda_system_additive _ A' dis] A'' ``` hoelzl@62975 ` 229` ``` by (intro suminf_le_const[OF summableI]) (auto intro!: increasingD[OF inc] countable_UN) ``` hoelzl@41689 ` 230` ``` qed ``` hoelzl@61273 ` 231` ``` have "f (a \ (\i. A i)) + f (a - (\i. A i)) = f a" ``` hoelzl@61273 ` 232` ``` if a [iff]: "a \ M" for a ``` hoelzl@61273 ` 233` ``` proof (rule antisym) ``` hoelzl@61273 ` 234` ``` have "range (\i. a \ A i) \ M" using A'' ``` hoelzl@61273 ` 235` ``` by blast ``` hoelzl@61273 ` 236` ``` moreover ``` hoelzl@61273 ` 237` ``` have "disjoint_family (\i. a \ A i)" using disj ``` hoelzl@61273 ` 238` ``` by (auto simp add: disjoint_family_on_def) ``` hoelzl@61273 ` 239` ``` moreover ``` hoelzl@61273 ` 240` ``` have "a \ (\i. A i) \ M" ``` hoelzl@61273 ` 241` ``` by (metis Int U_in a) ``` hoelzl@61273 ` 242` ``` ultimately ``` hoelzl@61273 ` 243` ``` have "f (a \ (\i. A i)) \ (\i. f (a \ A i))" ``` hoelzl@61273 ` 244` ``` using csa[unfolded countably_subadditive_def, rule_format, of "(\i. a \ A i)"] ``` hoelzl@61273 ` 245` ``` by (simp add: o_def) ``` hoelzl@61273 ` 246` ``` hence "f (a \ (\i. A i)) + f (a - (\i. A i)) \ (\i. f (a \ A i)) + f (a - (\i. A i))" ``` hoelzl@61273 ` 247` ``` by (rule add_right_mono) ``` hoelzl@61273 ` 248` ``` also have "\ \ f a" ``` hoelzl@62975 ` 249` ``` proof (intro ennreal_suminf_bound_add) ``` hoelzl@61273 ` 250` ``` fix n ``` hoelzl@61273 ` 251` ``` have UNION_in: "(\i\{0.. M" ``` hoelzl@61273 ` 252` ``` by (metis A'' UNION_in_sets) ``` haftmann@69325 ` 253` ``` have le_fa: "f (\ (A ` {0.. a) \ f a" using A'' ``` hoelzl@61273 ` 254` ``` by (blast intro: increasingD [OF inc] A'' UNION_in_sets) ``` hoelzl@61273 ` 255` ``` have ls: "(\i\{0.. lambda_system \ M f" ``` hoelzl@61273 ` 256` ``` using ls.UNION_in_sets by (simp add: A) ``` hoelzl@61273 ` 257` ``` hence eq_fa: "f a = f (a \ (\i\{0..i\{0..i. A i)) \ f (a - (\i\{0..i A i)) + f (a - (\i. A i)) \ f a" ``` hoelzl@61273 ` 262` ``` by (simp add: lambda_system_strong_sum pos A disj eq_fa add_left_mono atLeast0LessThan[symmetric]) ``` hoelzl@61273 ` 263` ``` qed ``` hoelzl@62975 ` 264` ``` finally show "f (a \ (\i. A i)) + f (a - (\i. A i)) \ f a" ``` hoelzl@62975 ` 265` ``` by simp ``` hoelzl@61273 ` 266` ``` next ``` hoelzl@61273 ` 267` ``` have "f a \ f (a \ (\i. A i) \ (a - (\i. A i)))" ``` hoelzl@61273 ` 268` ``` by (blast intro: increasingD [OF inc] U_in) ``` hoelzl@61273 ` 269` ``` also have "... \ f (a \ (\i. A i)) + f (a - (\i. A i))" ``` hoelzl@61273 ` 270` ``` by (blast intro: subadditiveD [OF sa] U_in) ``` hoelzl@61273 ` 271` ``` finally show "f a \ f (a \ (\i. A i)) + f (a - (\i. A i))" . ``` hoelzl@61273 ` 272` ``` qed ``` paulson@33271 ` 273` ``` thus ?thesis ``` hoelzl@38656 ` 274` ``` by (simp add: lambda_system_eq sums_iff U_eq U_in) ``` paulson@33271 ` 275` ```qed ``` paulson@33271 ` 276` ak2110@68833 ` 277` ```lemma%important (in sigma_algebra) caratheodory_lemma: ``` paulson@33271 ` 278` ``` assumes oms: "outer_measure_space M f" ``` hoelzl@47694 ` 279` ``` defines "L \ lambda_system \ M f" ``` hoelzl@47694 ` 280` ``` shows "measure_space \ L f" ``` ak2110@68833 ` 281` ```proof%unimportant - ``` hoelzl@41689 ` 282` ``` have pos: "positive M f" ``` paulson@33271 ` 283` ``` by (metis oms outer_measure_space_def) ``` hoelzl@47694 ` 284` ``` have alg: "algebra \ L" ``` hoelzl@38656 ` 285` ``` using lambda_system_algebra [of f, OF pos] ``` hoelzl@47694 ` 286` ``` by (simp add: algebra_iff_Un L_def) ``` hoelzl@42065 ` 287` ``` then ``` hoelzl@47694 ` 288` ``` have "sigma_algebra \ L" ``` paulson@33271 ` 289` ``` using lambda_system_caratheodory [OF oms] ``` hoelzl@47694 ` 290` ``` by (simp add: sigma_algebra_disjoint_iff L_def) ``` hoelzl@38656 ` 291` ``` moreover ``` hoelzl@47694 ` 292` ``` have "countably_additive L f" "positive L f" ``` paulson@33271 ` 293` ``` using pos lambda_system_caratheodory [OF oms] ``` hoelzl@47694 ` 294` ``` by (auto simp add: lambda_system_sets L_def countably_additive_def positive_def) ``` hoelzl@38656 ` 295` ``` ultimately ``` paulson@33271 ` 296` ``` show ?thesis ``` hoelzl@47694 ` 297` ``` using pos by (simp add: measure_space_def) ``` hoelzl@38656 ` 298` ```qed ``` hoelzl@38656 ` 299` ak2110@68833 ` 300` ```definition%important outer_measure :: "'a set set \ ('a set \ ennreal) \ 'a set \ ennreal" where ``` hoelzl@61273 ` 301` ``` "outer_measure M f X = ``` haftmann@69260 ` 302` ``` (INF A\{A. range A \ M \ disjoint_family A \ X \ (\i. A i)}. \i. f (A i))" ``` hoelzl@39096 ` 303` ak2110@68833 ` 304` ```lemma%unimportant (in ring_of_sets) outer_measure_agrees: ``` hoelzl@61273 ` 305` ``` assumes posf: "positive M f" and ca: "countably_additive M f" and s: "s \ M" ``` hoelzl@61273 ` 306` ``` shows "outer_measure M f s = f s" ``` hoelzl@61273 ` 307` ``` unfolding outer_measure_def ``` hoelzl@61273 ` 308` ```proof (safe intro!: antisym INF_greatest) ``` hoelzl@61273 ` 309` ``` fix A :: "nat \ 'a set" assume A: "range A \ M" and dA: "disjoint_family A" and sA: "s \ (\x. A x)" ``` paulson@33271 ` 310` ``` have inc: "increasing M f" ``` paulson@33271 ` 311` ``` by (metis additive_increasing ca countably_additive_additive posf) ``` hoelzl@61273 ` 312` ``` have "f s = f (\i. A i \ s)" ``` hoelzl@61273 ` 313` ``` using sA by (auto simp: Int_absorb1) ``` hoelzl@61273 ` 314` ``` also have "\ = (\i. f (A i \ s))" ``` hoelzl@61273 ` 315` ``` using sA dA A s ``` hoelzl@61273 ` 316` ``` by (intro ca[unfolded countably_additive_def, rule_format, symmetric]) ``` hoelzl@61273 ` 317` ``` (auto simp: Int_absorb1 disjoint_family_on_def) ``` hoelzl@41981 ` 318` ``` also have "... \ (\i. f (A i))" ``` hoelzl@62975 ` 319` ``` using A s by (auto intro!: suminf_le increasingD[OF inc]) ``` hoelzl@61273 ` 320` ``` finally show "f s \ (\i. f (A i))" . ``` hoelzl@61273 ` 321` ```next ``` hoelzl@61273 ` 322` ``` have "(\i. f (if i = 0 then s else {})) \ f s" ``` hoelzl@61273 ` 323` ``` using positiveD1[OF posf] by (subst suminf_finite[of "{0}"]) auto ``` haftmann@69313 ` 324` ``` with s show "(INF A\{A. range A \ M \ disjoint_family A \ s \ \(A ` UNIV)}. \i. f (A i)) \ f s" ``` hoelzl@61273 ` 325` ``` by (intro INF_lower2[of "\i. if i = 0 then s else {}"]) ``` hoelzl@61273 ` 326` ``` (auto simp: disjoint_family_on_def) ``` hoelzl@41981 ` 327` ```qed ``` hoelzl@41981 ` 328` ak2110@68833 ` 329` ```lemma%unimportant outer_measure_empty: ``` hoelzl@62975 ` 330` ``` "positive M f \ {} \ M \ outer_measure M f {} = 0" ``` hoelzl@62975 ` 331` ``` unfolding outer_measure_def ``` hoelzl@62975 ` 332` ``` by (intro antisym INF_lower2[of "\_. {}"]) (auto simp: disjoint_family_on_def positive_def) ``` hoelzl@61273 ` 333` ak2110@68833 ` 334` ```lemma%unimportant (in ring_of_sets) positive_outer_measure: ``` hoelzl@61273 ` 335` ``` assumes "positive M f" shows "positive (Pow \) (outer_measure M f)" ``` hoelzl@62975 ` 336` ``` unfolding positive_def by (auto simp: assms outer_measure_empty) ``` hoelzl@61273 ` 337` ak2110@68833 ` 338` ```lemma%unimportant (in ring_of_sets) increasing_outer_measure: "increasing (Pow \) (outer_measure M f)" ``` hoelzl@61273 ` 339` ``` by (force simp: increasing_def outer_measure_def intro!: INF_greatest intro: INF_lower) ``` paulson@33271 ` 340` ak2110@68833 ` 341` ```lemma%unimportant (in ring_of_sets) outer_measure_le: ``` hoelzl@61273 ` 342` ``` assumes pos: "positive M f" and inc: "increasing M f" and A: "range A \ M" and X: "X \ (\i. A i)" ``` hoelzl@61273 ` 343` ``` shows "outer_measure M f X \ (\i. f (A i))" ``` hoelzl@61273 ` 344` ``` unfolding outer_measure_def ``` hoelzl@61273 ` 345` ```proof (safe intro!: INF_lower2[of "disjointed A"] del: subsetI) ``` hoelzl@61273 ` 346` ``` show dA: "range (disjointed A) \ M" ``` hoelzl@61273 ` 347` ``` by (auto intro!: A range_disjointed_sets) ``` hoelzl@61273 ` 348` ``` have "\n. f (disjointed A n) \ f (A n)" ``` hoelzl@61273 ` 349` ``` by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A) ``` hoelzl@62975 ` 350` ``` then show "(\i. f (disjointed A i)) \ (\i. f (A i))" ``` hoelzl@62975 ` 351` ``` by (blast intro!: suminf_le) ``` hoelzl@61273 ` 352` ```qed (auto simp: X UN_disjointed_eq disjoint_family_disjointed) ``` paulson@33271 ` 353` ak2110@68833 ` 354` ```lemma%unimportant (in ring_of_sets) outer_measure_close: ``` hoelzl@62975 ` 355` ``` "outer_measure M f X < e \ \A. range A \ M \ disjoint_family A \ X \ (\i. A i) \ (\i. f (A i)) < e" ``` hoelzl@62975 ` 356` ``` unfolding outer_measure_def INF_less_iff by auto ``` paulson@33271 ` 357` ak2110@68833 ` 358` ```lemma%unimportant (in ring_of_sets) countably_subadditive_outer_measure: ``` hoelzl@41689 ` 359` ``` assumes posf: "positive M f" and inc: "increasing M f" ``` hoelzl@61273 ` 360` ``` shows "countably_subadditive (Pow \) (outer_measure M f)" ``` hoelzl@42066 ` 361` ```proof (simp add: countably_subadditive_def, safe) ``` hoelzl@61273 ` 362` ``` fix A :: "nat \ _" assume A: "range A \ Pow (\)" and sb: "(\i. A i) \ \" ``` hoelzl@61273 ` 363` ``` let ?O = "outer_measure M f" ``` hoelzl@62975 ` 364` ``` show "?O (\i. A i) \ (\n. ?O (A n))" ``` hoelzl@62975 ` 365` ``` proof (rule ennreal_le_epsilon) ``` hoelzl@62975 ` 366` ``` fix b and e :: real assume "0 < e" "(\n. outer_measure M f (A n)) < top" ``` hoelzl@62975 ` 367` ``` then have *: "\n. outer_measure M f (A n) < outer_measure M f (A n) + e * (1/2)^Suc n" ``` hoelzl@62975 ` 368` ``` by (auto simp add: less_top dest!: ennreal_suminf_lessD) ``` hoelzl@62975 ` 369` ``` obtain B ``` hoelzl@61273 ` 370` ``` where B: "\n. range (B n) \ M" ``` hoelzl@61273 ` 371` ``` and sbB: "\n. A n \ (\i. B n i)" ``` hoelzl@61273 ` 372` ``` and Ble: "\n. (\i. f (B n i)) \ ?O (A n) + e * (1/2)^(Suc n)" ``` hoelzl@62975 ` 373` ``` by (metis less_imp_le outer_measure_close[OF *]) ``` hoelzl@61273 ` 374` wenzelm@63040 ` 375` ``` define C where "C = case_prod B o prod_decode" ``` hoelzl@61273 ` 376` ``` from B have B_in_M: "\i j. B i j \ M" ``` haftmann@61032 ` 377` ``` by (rule range_subsetD) ``` hoelzl@61273 ` 378` ``` then have C: "range C \ M" ``` hoelzl@61273 ` 379` ``` by (auto simp add: C_def split_def) ``` hoelzl@61273 ` 380` ``` have A_C: "(\i. A i) \ (\i. C i)" ``` hoelzl@61273 ` 381` ``` using sbB by (auto simp add: C_def subset_eq) (metis prod.case prod_encode_inverse) ``` hoelzl@42066 ` 382` hoelzl@62975 ` 383` ``` have "?O (\i. A i) \ ?O (\i. C i)" ``` hoelzl@61273 ` 384` ``` using A_C A C by (intro increasing_outer_measure[THEN increasingD]) (auto dest!: sets_into_space) ``` hoelzl@61273 ` 385` ``` also have "\ \ (\i. f (C i))" ``` hoelzl@61273 ` 386` ``` using C by (intro outer_measure_le[OF posf inc]) auto ``` hoelzl@61273 ` 387` ``` also have "\ = (\n. \i. f (B n i))" ``` hoelzl@62975 ` 388` ``` using B_in_M unfolding C_def comp_def by (intro suminf_ennreal_2dimen) auto ``` hoelzl@62975 ` 389` ``` also have "\ \ (\n. ?O (A n) + e * (1/2) ^ Suc n)" ``` hoelzl@62975 ` 390` ``` using B_in_M by (intro suminf_le suminf_nonneg allI Ble) auto ``` hoelzl@62975 ` 391` ``` also have "... = (\n. ?O (A n)) + (\n. ennreal e * ennreal ((1/2) ^ Suc n))" ``` hoelzl@62975 ` 392` ``` using \0 < e\ by (subst suminf_add[symmetric]) ``` hoelzl@62975 ` 393` ``` (auto simp del: ennreal_suminf_cmult simp add: ennreal_mult[symmetric]) ``` hoelzl@62975 ` 394` ``` also have "\ = (\n. ?O (A n)) + e" ``` hoelzl@62975 ` 395` ``` unfolding ennreal_suminf_cmult ``` hoelzl@62975 ` 396` ``` by (subst suminf_ennreal_eq[OF zero_le_power power_half_series]) auto ``` hoelzl@62975 ` 397` ``` finally show "?O (\i. A i) \ (\n. ?O (A n)) + e" . ``` hoelzl@62975 ` 398` ``` qed ``` paulson@33271 ` 399` ```qed ``` paulson@33271 ` 400` ak2110@68833 ` 401` ```lemma%unimportant (in ring_of_sets) outer_measure_space_outer_measure: ``` hoelzl@61273 ` 402` ``` "positive M f \ increasing M f \ outer_measure_space (Pow \) (outer_measure M f)" ``` hoelzl@61273 ` 403` ``` by (simp add: outer_measure_space_def ``` hoelzl@61273 ` 404` ``` positive_outer_measure increasing_outer_measure countably_subadditive_outer_measure) ``` paulson@33271 ` 405` ak2110@68833 ` 406` ```lemma%unimportant (in ring_of_sets) algebra_subset_lambda_system: ``` hoelzl@41689 ` 407` ``` assumes posf: "positive M f" and inc: "increasing M f" ``` paulson@33271 ` 408` ``` and add: "additive M f" ``` hoelzl@61273 ` 409` ``` shows "M \ lambda_system \ (Pow \) (outer_measure M f)" ``` hoelzl@38656 ` 410` ```proof (auto dest: sets_into_space ``` hoelzl@38656 ` 411` ``` simp add: algebra.lambda_system_eq [OF algebra_Pow]) ``` hoelzl@61273 ` 412` ``` fix x s assume x: "x \ M" and s: "s \ \" ``` hoelzl@61273 ` 413` ``` have [simp]: "\x. x \ M \ s \ (\ - x) = s - x" using s ``` paulson@33271 ` 414` ``` by blast ``` hoelzl@61273 ` 415` ``` have "outer_measure M f (s \ x) + outer_measure M f (s - x) \ outer_measure M f s" ``` hoelzl@61273 ` 416` ``` unfolding outer_measure_def[of M f s] ``` hoelzl@61273 ` 417` ``` proof (safe intro!: INF_greatest) ``` hoelzl@61273 ` 418` ``` fix A :: "nat \ 'a set" assume A: "disjoint_family A" "range A \ M" "s \ (\i. A i)" ``` hoelzl@61273 ` 419` ``` have "outer_measure M f (s \ x) \ (\i. f (A i \ x))" ``` hoelzl@61273 ` 420` ``` unfolding outer_measure_def ``` hoelzl@61273 ` 421` ``` proof (safe intro!: INF_lower2[of "\i. A i \ x"]) ``` hoelzl@61273 ` 422` ``` from A(1) show "disjoint_family (\i. A i \ x)" ``` hoelzl@61273 ` 423` ``` by (rule disjoint_family_on_bisimulation) auto ``` hoelzl@61273 ` 424` ``` qed (insert x A, auto) ``` hoelzl@61273 ` 425` ``` moreover ``` hoelzl@61273 ` 426` ``` have "outer_measure M f (s - x) \ (\i. f (A i - x))" ``` hoelzl@61273 ` 427` ``` unfolding outer_measure_def ``` hoelzl@61273 ` 428` ``` proof (safe intro!: INF_lower2[of "\i. A i - x"]) ``` hoelzl@61273 ` 429` ``` from A(1) show "disjoint_family (\i. A i - x)" ``` hoelzl@61273 ` 430` ``` by (rule disjoint_family_on_bisimulation) auto ``` hoelzl@61273 ` 431` ``` qed (insert x A, auto) ``` hoelzl@61273 ` 432` ``` ultimately have "outer_measure M f (s \ x) + outer_measure M f (s - x) \ ``` hoelzl@61273 ` 433` ``` (\i. f (A i \ x)) + (\i. f (A i - x))" by (rule add_mono) ``` hoelzl@61273 ` 434` ``` also have "\ = (\i. f (A i \ x) + f (A i - x))" ``` hoelzl@62975 ` 435` ``` using A(2) x posf by (subst suminf_add) (auto simp: positive_def) ``` hoelzl@61273 ` 436` ``` also have "\ = (\i. f (A i))" ``` hoelzl@61273 ` 437` ``` using A x ``` hoelzl@61273 ` 438` ``` by (subst add[THEN additiveD, symmetric]) ``` hoelzl@61273 ` 439` ``` (auto intro!: arg_cong[where f=suminf] arg_cong[where f=f]) ``` hoelzl@61273 ` 440` ``` finally show "outer_measure M f (s \ x) + outer_measure M f (s - x) \ (\i. f (A i))" . ``` hoelzl@42066 ` 441` ``` qed ``` hoelzl@38656 ` 442` ``` moreover ``` hoelzl@61273 ` 443` ``` have "outer_measure M f s \ outer_measure M f (s \ x) + outer_measure M f (s - x)" ``` hoelzl@42145 ` 444` ``` proof - ``` hoelzl@61273 ` 445` ``` have "outer_measure M f s = outer_measure M f ((s \ x) \ (s - x))" ``` paulson@33271 ` 446` ``` by (metis Un_Diff_Int Un_commute) ``` hoelzl@61273 ` 447` ``` also have "... \ outer_measure M f (s \ x) + outer_measure M f (s - x)" ``` hoelzl@38656 ` 448` ``` apply (rule subadditiveD) ``` hoelzl@42145 ` 449` ``` apply (rule ring_of_sets.countably_subadditive_subadditive [OF ring_of_sets_Pow]) ``` hoelzl@62975 ` 450` ``` apply (simp add: positive_def outer_measure_empty[OF posf]) ``` hoelzl@61273 ` 451` ``` apply (rule countably_subadditive_outer_measure) ``` hoelzl@41689 ` 452` ``` using s by (auto intro!: posf inc) ``` paulson@33271 ` 453` ``` finally show ?thesis . ``` hoelzl@42145 ` 454` ``` qed ``` hoelzl@38656 ` 455` ``` ultimately ``` hoelzl@61273 ` 456` ``` show "outer_measure M f (s \ x) + outer_measure M f (s - x) = outer_measure M f s" ``` paulson@33271 ` 457` ``` by (rule order_antisym) ``` paulson@33271 ` 458` ```qed ``` paulson@33271 ` 459` ak2110@68833 ` 460` ```lemma%unimportant measure_down: "measure_space \ N \ \ sigma_algebra \ M \ M \ N \ measure_space \ M \" ``` hoelzl@57446 ` 461` ``` by (auto simp add: measure_space_def positive_def countably_additive_def subset_eq) ``` paulson@33271 ` 462` ak2110@68833 ` 463` ```subsection%important \Caratheodory's theorem\ ``` hoelzl@56994 ` 464` ak2110@68833 ` 465` ```theorem%important (in ring_of_sets) caratheodory': ``` hoelzl@41689 ` 466` ``` assumes posf: "positive M f" and ca: "countably_additive M f" ``` hoelzl@62975 ` 467` ``` shows "\\ :: 'a set \ ennreal. (\s \ M. \ s = f s) \ measure_space \ (sigma_sets \ M) \" ``` ak2110@68833 ` 468` ```proof%unimportant - ``` hoelzl@41689 ` 469` ``` have inc: "increasing M f" ``` hoelzl@41689 ` 470` ``` by (metis additive_increasing ca countably_additive_additive posf) ``` hoelzl@61273 ` 471` ``` let ?O = "outer_measure M f" ``` wenzelm@63040 ` 472` ``` define ls where "ls = lambda_system \ (Pow \) ?O" ``` hoelzl@61273 ` 473` ``` have mls: "measure_space \ ls ?O" ``` hoelzl@41689 ` 474` ``` using sigma_algebra.caratheodory_lemma ``` hoelzl@61273 ` 475` ``` [OF sigma_algebra_Pow outer_measure_space_outer_measure [OF posf inc]] ``` hoelzl@41689 ` 476` ``` by (simp add: ls_def) ``` hoelzl@47694 ` 477` ``` hence sls: "sigma_algebra \ ls" ``` hoelzl@41689 ` 478` ``` by (simp add: measure_space_def) ``` hoelzl@47694 ` 479` ``` have "M \ ls" ``` hoelzl@41689 ` 480` ``` by (simp add: ls_def) ``` hoelzl@41689 ` 481` ``` (metis ca posf inc countably_additive_additive algebra_subset_lambda_system) ``` hoelzl@47694 ` 482` ``` hence sgs_sb: "sigma_sets (\) (M) \ ls" ``` hoelzl@47694 ` 483` ``` using sigma_algebra.sigma_sets_subset [OF sls, of "M"] ``` hoelzl@41689 ` 484` ``` by simp ``` hoelzl@61273 ` 485` ``` have "measure_space \ (sigma_sets \ M) ?O" ``` hoelzl@41689 ` 486` ``` by (rule measure_down [OF mls], rule sigma_algebra_sigma_sets) ``` hoelzl@41689 ` 487` ``` (simp_all add: sgs_sb space_closed) ``` hoelzl@61273 ` 488` ``` thus ?thesis using outer_measure_agrees [OF posf ca] ``` hoelzl@61273 ` 489` ``` by (intro exI[of _ ?O]) auto ``` hoelzl@41689 ` 490` ```qed ``` paulson@33271 ` 491` ak2110@68833 ` 492` ```lemma%important (in ring_of_sets) caratheodory_empty_continuous: ``` hoelzl@47694 ` 493` ``` assumes f: "positive M f" "additive M f" and fin: "\A. A \ M \ f A \ \" ``` wenzelm@61969 ` 494` ``` assumes cont: "\A. range A \ M \ decseq A \ (\i. A i) = {} \ (\i. f (A i)) \ 0" ``` hoelzl@62975 ` 495` ``` shows "\\ :: 'a set \ ennreal. (\s \ M. \ s = f s) \ measure_space \ (sigma_sets \ M) \" ``` ak2110@68833 ` 496` ```proof%unimportant (intro caratheodory' empty_continuous_imp_countably_additive f) ``` hoelzl@47694 ` 497` ``` show "\A\M. f A \ \" using fin by auto ``` hoelzl@42145 ` 498` ```qed (rule cont) ``` hoelzl@42145 ` 499` ak2110@68833 ` 500` ```subsection%important \Volumes\ ``` hoelzl@47762 ` 501` ak2110@68833 ` 502` ```definition%important volume :: "'a set set \ ('a set \ ennreal) \ bool" where ``` hoelzl@47762 ` 503` ``` "volume M f \ ``` hoelzl@47762 ` 504` ``` (f {} = 0) \ (\a\M. 0 \ f a) \ ``` hoelzl@47762 ` 505` ``` (\C\M. disjoint C \ finite C \ \C \ M \ f (\C) = (\c\C. f c))" ``` hoelzl@47762 ` 506` ak2110@68833 ` 507` ```lemma%unimportant volumeI: ``` hoelzl@47762 ` 508` ``` assumes "f {} = 0" ``` hoelzl@47762 ` 509` ``` assumes "\a. a \ M \ 0 \ f a" ``` hoelzl@47762 ` 510` ``` assumes "\C. C \ M \ disjoint C \ finite C \ \C \ M \ f (\C) = (\c\C. f c)" ``` hoelzl@47762 ` 511` ``` shows "volume M f" ``` hoelzl@47762 ` 512` ``` using assms by (auto simp: volume_def) ``` hoelzl@47762 ` 513` ak2110@68833 ` 514` ```lemma%unimportant volume_positive: ``` hoelzl@47762 ` 515` ``` "volume M f \ a \ M \ 0 \ f a" ``` hoelzl@47762 ` 516` ``` by (auto simp: volume_def) ``` hoelzl@47762 ` 517` ak2110@68833 ` 518` ```lemma%unimportant volume_empty: ``` hoelzl@47762 ` 519` ``` "volume M f \ f {} = 0" ``` hoelzl@47762 ` 520` ``` by (auto simp: volume_def) ``` hoelzl@47762 ` 521` ak2110@68833 ` 522` ```lemma%unimportant volume_finite_additive: ``` hoelzl@62975 ` 523` ``` assumes "volume M f" ``` haftmann@69313 ` 524` ``` assumes A: "\i. i \ I \ A i \ M" "disjoint_family_on A I" "finite I" "\(A ` I) \ M" ``` haftmann@69313 ` 525` ``` shows "f (\(A ` I)) = (\i\I. f (A i))" ``` hoelzl@47762 ` 526` ```proof - ``` haftmann@52141 ` 527` ``` have "A`I \ M" "disjoint (A`I)" "finite (A`I)" "\(A`I) \ M" ``` haftmann@62343 ` 528` ``` using A by (auto simp: disjoint_family_on_disjoint_image) ``` wenzelm@61808 ` 529` ``` with \volume M f\ have "f (\(A`I)) = (\a\A`I. f a)" ``` hoelzl@47762 ` 530` ``` unfolding volume_def by blast ``` hoelzl@47762 ` 531` ``` also have "\ = (\i\I. f (A i))" ``` nipkow@64267 ` 532` ``` proof (subst sum.reindex_nontrivial) ``` hoelzl@47762 ` 533` ``` fix i j assume "i \ I" "j \ I" "i \ j" "A i = A j" ``` wenzelm@61808 ` 534` ``` with \disjoint_family_on A I\ have "A i = {}" ``` hoelzl@47762 ` 535` ``` by (auto simp: disjoint_family_on_def) ``` hoelzl@47762 ` 536` ``` then show "f (A i) = 0" ``` wenzelm@61808 ` 537` ``` using volume_empty[OF \volume M f\] by simp ``` wenzelm@61808 ` 538` ``` qed (auto intro: \finite I\) ``` haftmann@69313 ` 539` ``` finally show "f (\(A ` I)) = (\i\I. f (A i))" ``` hoelzl@47762 ` 540` ``` by simp ``` hoelzl@47762 ` 541` ```qed ``` hoelzl@47762 ` 542` ak2110@68833 ` 543` ```lemma%unimportant (in ring_of_sets) volume_additiveI: ``` hoelzl@62975 ` 544` ``` assumes pos: "\a. a \ M \ 0 \ \ a" ``` hoelzl@47762 ` 545` ``` assumes [simp]: "\ {} = 0" ``` hoelzl@47762 ` 546` ``` assumes add: "\a b. a \ M \ b \ M \ a \ b = {} \ \ (a \ b) = \ a + \ b" ``` hoelzl@47762 ` 547` ``` shows "volume M \" ``` hoelzl@47762 ` 548` ```proof (unfold volume_def, safe) ``` hoelzl@47762 ` 549` ``` fix C assume "finite C" "C \ M" "disjoint C" ``` nipkow@64267 ` 550` ``` then show "\ (\C) = sum \ C" ``` hoelzl@47762 ` 551` ``` proof (induct C) ``` hoelzl@47762 ` 552` ``` case (insert c C) ``` hoelzl@47762 ` 553` ``` from insert(1,2,4,5) have "\ (\insert c C) = \ c + \ (\C)" ``` hoelzl@47762 ` 554` ``` by (auto intro!: add simp: disjoint_def) ``` hoelzl@47762 ` 555` ``` with insert show ?case ``` hoelzl@47762 ` 556` ``` by (simp add: disjoint_def) ``` hoelzl@47762 ` 557` ``` qed simp ``` hoelzl@47762 ` 558` ```qed fact+ ``` hoelzl@47762 ` 559` ak2110@68833 ` 560` ```lemma%important (in semiring_of_sets) extend_volume: ``` hoelzl@47762 ` 561` ``` assumes "volume M \" ``` hoelzl@47762 ` 562` ``` shows "\\'. volume generated_ring \' \ (\a\M. \' a = \ a)" ``` ak2110@68833 ` 563` ```proof%unimportant - ``` hoelzl@47762 ` 564` ``` let ?R = generated_ring ``` hoelzl@47762 ` 565` ``` have "\a\?R. \m. \C\M. a = \C \ finite C \ disjoint C \ m = (\c\C. \ c)" ``` hoelzl@47762 ` 566` ``` by (auto simp: generated_ring_def) ``` hoelzl@47762 ` 567` ``` from bchoice[OF this] guess \' .. note \'_spec = this ``` hoelzl@62975 ` 568` hoelzl@47762 ` 569` ``` { fix C assume C: "C \ M" "finite C" "disjoint C" ``` hoelzl@47762 ` 570` ``` fix D assume D: "D \ M" "finite D" "disjoint D" ``` hoelzl@47762 ` 571` ``` assume "\C = \D" ``` hoelzl@47762 ` 572` ``` have "(\d\D. \ d) = (\d\D. \c\C. \ (c \ d))" ``` nipkow@64267 ` 573` ``` proof (intro sum.cong refl) ``` hoelzl@47762 ` 574` ``` fix d assume "d \ D" ``` hoelzl@47762 ` 575` ``` have Un_eq_d: "(\c\C. c \ d) = d" ``` wenzelm@61808 ` 576` ``` using \d \ D\ \\C = \D\ by auto ``` hoelzl@47762 ` 577` ``` moreover have "\ (\c\C. c \ d) = (\c\C. \ (c \ d))" ``` hoelzl@47762 ` 578` ``` proof (rule volume_finite_additive) ``` hoelzl@47762 ` 579` ``` { fix c assume "c \ C" then show "c \ d \ M" ``` wenzelm@61808 ` 580` ``` using C D \d \ D\ by auto } ``` hoelzl@47762 ` 581` ``` show "(\a\C. a \ d) \ M" ``` wenzelm@61808 ` 582` ``` unfolding Un_eq_d using \d \ D\ D by auto ``` hoelzl@47762 ` 583` ``` show "disjoint_family_on (\a. a \ d) C" ``` wenzelm@61808 ` 584` ``` using \disjoint C\ by (auto simp: disjoint_family_on_def disjoint_def) ``` hoelzl@47762 ` 585` ``` qed fact+ ``` hoelzl@47762 ` 586` ``` ultimately show "\ d = (\c\C. \ (c \ d))" by simp ``` hoelzl@47762 ` 587` ``` qed } ``` hoelzl@47762 ` 588` ``` note split_sum = this ``` hoelzl@47762 ` 589` hoelzl@47762 ` 590` ``` { fix C assume C: "C \ M" "finite C" "disjoint C" ``` hoelzl@47762 ` 591` ``` fix D assume D: "D \ M" "finite D" "disjoint D" ``` hoelzl@47762 ` 592` ``` assume "\C = \D" ``` hoelzl@47762 ` 593` ``` with split_sum[OF C D] split_sum[OF D C] ``` hoelzl@47762 ` 594` ``` have "(\d\D. \ d) = (\c\C. \ c)" ``` haftmann@66804 ` 595` ``` by (simp, subst sum.swap, simp add: ac_simps) } ``` hoelzl@47762 ` 596` ``` note sum_eq = this ``` hoelzl@47762 ` 597` hoelzl@47762 ` 598` ``` { fix C assume C: "C \ M" "finite C" "disjoint C" ``` hoelzl@47762 ` 599` ``` then have "\C \ ?R" by (auto simp: generated_ring_def) ``` hoelzl@47762 ` 600` ``` with \'_spec[THEN bspec, of "\C"] ``` hoelzl@47762 ` 601` ``` obtain D where ``` hoelzl@47762 ` 602` ``` D: "D \ M" "finite D" "disjoint D" "\C = \D" and "\' (\C) = (\d\D. \ d)" ``` lp15@61427 ` 603` ``` by auto ``` hoelzl@47762 ` 604` ``` with sum_eq[OF C D] have "\' (\C) = (\c\C. \ c)" by simp } ``` hoelzl@47762 ` 605` ``` note \' = this ``` hoelzl@47762 ` 606` hoelzl@47762 ` 607` ``` show ?thesis ``` hoelzl@47762 ` 608` ``` proof (intro exI conjI ring_of_sets.volume_additiveI[OF generating_ring] ballI) ``` hoelzl@47762 ` 609` ``` fix a assume "a \ M" with \'[of "{a}"] show "\' a = \ a" ``` hoelzl@47762 ` 610` ``` by (simp add: disjoint_def) ``` hoelzl@47762 ` 611` ``` next ``` hoelzl@47762 ` 612` ``` fix a assume "a \ ?R" then guess Ca .. note Ca = this ``` wenzelm@61808 ` 613` ``` with \'[of Ca] \volume M \\[THEN volume_positive] ``` hoelzl@47762 ` 614` ``` show "0 \ \' a" ``` nipkow@64267 ` 615` ``` by (auto intro!: sum_nonneg) ``` hoelzl@47762 ` 616` ``` next ``` hoelzl@47762 ` 617` ``` show "\' {} = 0" using \'[of "{}"] by auto ``` hoelzl@47762 ` 618` ``` next ``` hoelzl@47762 ` 619` ``` fix a assume "a \ ?R" then guess Ca .. note Ca = this ``` hoelzl@47762 ` 620` ``` fix b assume "b \ ?R" then guess Cb .. note Cb = this ``` hoelzl@47762 ` 621` ``` assume "a \ b = {}" ``` hoelzl@47762 ` 622` ``` with Ca Cb have "Ca \ Cb \ {{}}" by auto ``` hoelzl@47762 ` 623` ``` then have C_Int_cases: "Ca \ Cb = {{}} \ Ca \ Cb = {}" by auto ``` hoelzl@47762 ` 624` wenzelm@61808 ` 625` ``` from \a \ b = {}\ have "\' (\(Ca \ Cb)) = (\c\Ca \ Cb. \ c)" ``` hoelzl@47762 ` 626` ``` using Ca Cb by (intro \') (auto intro!: disjoint_union) ``` hoelzl@47762 ` 627` ``` also have "\ = (\c\Ca \ Cb. \ c) + (\c\Ca \ Cb. \ c)" ``` wenzelm@61808 ` 628` ``` using C_Int_cases volume_empty[OF \volume M \\] by (elim disjE) simp_all ``` hoelzl@47762 ` 629` ``` also have "\ = (\c\Ca. \ c) + (\c\Cb. \ c)" ``` nipkow@64267 ` 630` ``` using Ca Cb by (simp add: sum.union_inter) ``` hoelzl@47762 ` 631` ``` also have "\ = \' a + \' b" ``` hoelzl@47762 ` 632` ``` using Ca Cb by (simp add: \') ``` hoelzl@47762 ` 633` ``` finally show "\' (a \ b) = \' a + \' b" ``` hoelzl@47762 ` 634` ``` using Ca Cb by simp ``` hoelzl@47762 ` 635` ``` qed ``` hoelzl@47762 ` 636` ```qed ``` hoelzl@47762 ` 637` ak2110@68833 ` 638` ```subsubsection%important \Caratheodory on semirings\ ``` hoelzl@47762 ` 639` ak2110@68833 ` 640` ```theorem%important (in semiring_of_sets) caratheodory: ``` hoelzl@47762 ` 641` ``` assumes pos: "positive M \" and ca: "countably_additive M \" ``` hoelzl@62975 ` 642` ``` shows "\\' :: 'a set \ ennreal. (\s \ M. \' s = \ s) \ measure_space \ (sigma_sets \ M) \'" ``` ak2110@68833 ` 643` ```proof%unimportant - ``` hoelzl@47762 ` 644` ``` have "volume M \" ``` hoelzl@47762 ` 645` ``` proof (rule volumeI) ``` hoelzl@47762 ` 646` ``` { fix a assume "a \ M" then show "0 \ \ a" ``` hoelzl@47762 ` 647` ``` using pos unfolding positive_def by auto } ``` hoelzl@47762 ` 648` ``` note p = this ``` hoelzl@47762 ` 649` hoelzl@47762 ` 650` ``` fix C assume sets_C: "C \ M" "\C \ M" and "disjoint C" "finite C" ``` hoelzl@47762 ` 651` ``` have "\F'. bij_betw F' {..finite C\]) auto ``` hoelzl@47762 ` 653` ``` then guess F' .. note F' = this ``` hoelzl@47762 ` 654` ``` then have F': "C = F' ` {..< card C}" "inj_on F' {..< card C}" ``` hoelzl@47762 ` 655` ``` by (auto simp: bij_betw_def) ``` hoelzl@47762 ` 656` ``` { fix i j assume *: "i < card C" "j < card C" "i \ j" ``` hoelzl@47762 ` 657` ``` with F' have "F' i \ C" "F' j \ C" "F' i \ F' j" ``` hoelzl@47762 ` 658` ``` unfolding inj_on_def by auto ``` wenzelm@61808 ` 659` ``` with \disjoint C\[THEN disjointD] ``` hoelzl@47762 ` 660` ``` have "F' i \ F' j = {}" ``` hoelzl@47762 ` 661` ``` by auto } ``` hoelzl@47762 ` 662` ``` note F'_disj = this ``` wenzelm@63040 ` 663` ``` define F where "F i = (if i < card C then F' i else {})" for i ``` hoelzl@47762 ` 664` ``` then have "disjoint_family F" ``` hoelzl@47762 ` 665` ``` using F'_disj by (auto simp: disjoint_family_on_def) ``` hoelzl@47762 ` 666` ``` moreover from F' have "(\i. F i) = \C" ``` nipkow@62390 ` 667` ``` by (auto simp add: F_def split: if_split_asm) blast ``` hoelzl@47762 ` 668` ``` moreover have sets_F: "\i. F i \ M" ``` hoelzl@47762 ` 669` ``` using F' sets_C by (auto simp: F_def) ``` hoelzl@47762 ` 670` ``` moreover note sets_C ``` hoelzl@47762 ` 671` ``` ultimately have "\ (\C) = (\i. \ (F i))" ``` hoelzl@47762 ` 672` ``` using ca[unfolded countably_additive_def, THEN spec, of F] by auto ``` hoelzl@47762 ` 673` ``` also have "\ = (\i (F' i))" ``` hoelzl@47762 ` 674` ``` proof - ``` hoelzl@47762 ` 675` ``` have "(\i. if i \ {..< card C} then \ (F' i) else 0) sums (\i (F' i))" ``` hoelzl@47762 ` 676` ``` by (rule sums_If_finite_set) auto ``` hoelzl@47762 ` 677` ``` also have "(\i. if i \ {..< card C} then \ (F' i) else 0) = (\i. \ (F i))" ``` hoelzl@47762 ` 678` ``` using pos by (auto simp: positive_def F_def) ``` hoelzl@47762 ` 679` ``` finally show "(\i. \ (F i)) = (\i (F' i))" ``` hoelzl@47762 ` 680` ``` by (simp add: sums_iff) ``` hoelzl@47762 ` 681` ``` qed ``` hoelzl@47762 ` 682` ``` also have "\ = (\c\C. \ c)" ``` nipkow@64267 ` 683` ``` using F'(2) by (subst (2) F') (simp add: sum.reindex) ``` hoelzl@47762 ` 684` ``` finally show "\ (\C) = (\c\C. \ c)" . ``` hoelzl@47762 ` 685` ``` next ``` hoelzl@47762 ` 686` ``` show "\ {} = 0" ``` wenzelm@61808 ` 687` ``` using \positive M \\ by (rule positiveD1) ``` hoelzl@47762 ` 688` ``` qed ``` hoelzl@47762 ` 689` ``` from extend_volume[OF this] obtain \_r where ``` hoelzl@47762 ` 690` ``` V: "volume generated_ring \_r" "\a. a \ M \ \ a = \_r a" ``` hoelzl@47762 ` 691` ``` by auto ``` hoelzl@47762 ` 692` hoelzl@47762 ` 693` ``` interpret G: ring_of_sets \ generated_ring ``` hoelzl@47762 ` 694` ``` by (rule generating_ring) ``` hoelzl@47762 ` 695` hoelzl@47762 ` 696` ``` have pos: "positive generated_ring \_r" ``` hoelzl@47762 ` 697` ``` using V unfolding positive_def by (auto simp: positive_def intro!: volume_positive volume_empty) ``` hoelzl@47762 ` 698` hoelzl@47762 ` 699` ``` have "countably_additive generated_ring \_r" ``` hoelzl@47762 ` 700` ``` proof (rule countably_additiveI) ``` hoelzl@47762 ` 701` ``` fix A' :: "nat \ 'a set" assume A': "range A' \ generated_ring" "disjoint_family A'" ``` hoelzl@47762 ` 702` ``` and Un_A: "(\i. A' i) \ generated_ring" ``` hoelzl@47762 ` 703` hoelzl@47762 ` 704` ``` from generated_ringE[OF Un_A] guess C' . note C' = this ``` hoelzl@47762 ` 705` hoelzl@47762 ` 706` ``` { fix c assume "c \ C'" ``` wenzelm@63040 ` 707` ``` moreover define A where [abs_def]: "A i = A' i \ c" for i ``` hoelzl@47762 ` 708` ``` ultimately have A: "range A \ generated_ring" "disjoint_family A" ``` hoelzl@47762 ` 709` ``` and Un_A: "(\i. A i) \ generated_ring" ``` hoelzl@47762 ` 710` ``` using A' C' ``` hoelzl@47762 ` 711` ``` by (auto intro!: G.Int G.finite_Union intro: generated_ringI_Basic simp: disjoint_family_on_def) ``` wenzelm@61808 ` 712` ``` from A C' \c \ C'\ have UN_eq: "(\i. A i) = c" ``` hoelzl@47762 ` 713` ``` by (auto simp: A_def) ``` hoelzl@47762 ` 714` hoelzl@47762 ` 715` ``` 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)" ``` hoelzl@47762 ` 716` ``` (is "\i. ?P i") ``` hoelzl@47762 ` 717` ``` proof ``` hoelzl@47762 ` 718` ``` fix i ``` hoelzl@47762 ` 719` ``` from A have Ai: "A i \ generated_ring" by auto ``` hoelzl@47762 ` 720` ``` from generated_ringE[OF this] guess C . note C = this ``` hoelzl@47762 ` 721` hoelzl@47762 ` 722` ``` have "\F'. bij_betw F' {..finite C\]) auto ``` hoelzl@47762 ` 724` ``` then guess F .. note F = this ``` wenzelm@63040 ` 725` ``` define f where [abs_def]: "f i = (if i < card C then F i else {})" for i ``` hoelzl@47762 ` 726` ``` then have f: "bij_betw f {..< card C} C" ``` hoelzl@47762 ` 727` ``` by (intro bij_betw_cong[THEN iffD1, OF _ F]) auto ``` hoelzl@47762 ` 728` ``` with C have "\j. f j \ M" ``` hoelzl@47762 ` 729` ``` by (auto simp: Pi_iff f_def dest!: bij_betw_imp_funcset) ``` hoelzl@47762 ` 730` ``` moreover ``` hoelzl@47762 ` 731` ``` from f C have d_f: "disjoint_family_on f {..xrange f = A i" ``` haftmann@62343 ` 739` ``` using f C Ai unfolding bij_betw_def ``` nipkow@69164 ` 740` ``` by (auto simp add: f_def cong del: SUP_cong_strong) ``` hoelzl@62975 ` 741` ``` moreover ``` hoelzl@47762 ` 742` ``` { have "(\j. \_r (f j)) = (\j. if j \ {..< card C} then \_r (f j) else 0)" ``` hoelzl@47762 ` 743` ``` using volume_empty[OF V(1)] by (auto intro!: arg_cong[where f=suminf] simp: f_def) ``` hoelzl@47762 ` 744` ``` also have "\ = (\j_r (f j))" ``` hoelzl@47762 ` 745` ``` by (rule sums_If_finite_set[THEN sums_unique, symmetric]) simp ``` hoelzl@47762 ` 746` ``` also have "\ = \_r (A i)" ``` hoelzl@47762 ` 747` ``` using C f[THEN bij_betw_imp_funcset] unfolding Ai_eq ``` hoelzl@47762 ` 748` ``` by (intro volume_finite_additive[OF V(1) _ d_f, symmetric]) ``` hoelzl@47762 ` 749` ``` (auto simp: Pi_iff Ai_eq intro: generated_ringI_Basic) ``` hoelzl@47762 ` 750` ``` finally have "\_r (A i) = (\j. \_r (f j))" .. } ``` hoelzl@47762 ` 751` ``` ultimately show "?P i" ``` hoelzl@47762 ` 752` ``` by blast ``` hoelzl@47762 ` 753` ``` qed ``` hoelzl@47762 ` 754` ``` from choice[OF this] guess f .. note f = this ``` haftmann@61424 ` 755` ``` then have UN_f_eq: "(\i. case_prod f (prod_decode i)) = (\i. A i)" ``` hoelzl@47762 ` 756` ``` unfolding UN_extend_simps surj_prod_decode by (auto simp: set_eq_iff) ``` hoelzl@47762 ` 757` haftmann@61424 ` 758` ``` have d: "disjoint_family (\i. case_prod f (prod_decode i))" ``` hoelzl@47762 ` 759` ``` unfolding disjoint_family_on_def ``` hoelzl@47762 ` 760` ``` proof (intro ballI impI) ``` hoelzl@47762 ` 761` ``` fix m n :: nat assume "m \ n" ``` hoelzl@47762 ` 762` ``` then have neq: "prod_decode m \ prod_decode n" ``` hoelzl@47762 ` 763` ``` using inj_prod_decode[of UNIV] by (auto simp: inj_on_def) ``` haftmann@61424 ` 764` ``` show "case_prod f (prod_decode m) \ case_prod f (prod_decode n) = {}" ``` hoelzl@47762 ` 765` ``` proof cases ``` hoelzl@47762 ` 766` ``` assume "fst (prod_decode m) = fst (prod_decode n)" ``` hoelzl@47762 ` 767` ``` then show ?thesis ``` hoelzl@47762 ` 768` ``` using neq f by (fastforce simp: disjoint_family_on_def) ``` hoelzl@47762 ` 769` ``` next ``` hoelzl@47762 ` 770` ``` assume neq: "fst (prod_decode m) \ fst (prod_decode n)" ``` haftmann@61424 ` 771` ``` have "case_prod f (prod_decode m) \ A (fst (prod_decode m))" ``` haftmann@61424 ` 772` ``` "case_prod f (prod_decode n) \ A (fst (prod_decode n))" ``` hoelzl@47762 ` 773` ``` using f[THEN spec, of "fst (prod_decode m)"] ``` hoelzl@47762 ` 774` ``` using f[THEN spec, of "fst (prod_decode n)"] ``` hoelzl@47762 ` 775` ``` by (auto simp: set_eq_iff) ``` hoelzl@47762 ` 776` ``` with f A neq show ?thesis ``` hoelzl@47762 ` 777` ``` by (fastforce simp: disjoint_family_on_def subset_eq set_eq_iff) ``` hoelzl@47762 ` 778` ``` qed ``` hoelzl@47762 ` 779` ``` qed ``` haftmann@61424 ` 780` ``` from f have "(\n. \_r (A n)) = (\n. \_r (case_prod f (prod_decode n)))" ``` hoelzl@62975 ` 781` ``` by (intro suminf_ennreal_2dimen[symmetric] generated_ringI_Basic) ``` hoelzl@47762 ` 782` ``` (auto split: prod.split) ``` haftmann@61424 ` 783` ``` also have "\ = (\n. \ (case_prod f (prod_decode n)))" ``` hoelzl@47762 ` 784` ``` using f V(2) by (auto intro!: arg_cong[where f=suminf] split: prod.split) ``` haftmann@61424 ` 785` ``` also have "\ = \ (\i. case_prod f (prod_decode i))" ``` wenzelm@61808 ` 786` ``` using f \c \ C'\ C' ``` hoelzl@47762 ` 787` ``` by (intro ca[unfolded countably_additive_def, rule_format]) ``` hoelzl@47762 ` 788` ``` (auto split: prod.split simp: UN_f_eq d UN_eq) ``` hoelzl@47762 ` 789` ``` finally have "(\n. \_r (A' n \ c)) = \ c" ``` hoelzl@47762 ` 790` ``` using UN_f_eq UN_eq by (simp add: A_def) } ``` hoelzl@47762 ` 791` ``` note eq = this ``` hoelzl@47762 ` 792` hoelzl@47762 ` 793` ``` have "(\n. \_r (A' n)) = (\n. \c\C'. \_r (A' n \ c))" ``` bulwahn@49394 ` 794` ``` using C' A' ``` hoelzl@47762 ` 795` ``` by (subst volume_finite_additive[symmetric, OF V(1)]) ``` haftmann@62343 ` 796` ``` (auto simp: disjoint_def disjoint_family_on_def ``` hoelzl@47762 ` 797` ``` intro!: G.Int G.finite_Union arg_cong[where f="\X. suminf (\i. \_r (X i))"] ext ``` hoelzl@47762 ` 798` ``` intro: generated_ringI_Basic) ``` hoelzl@47762 ` 799` ``` also have "\ = (\c\C'. \n. \_r (A' n \ c))" ``` hoelzl@47762 ` 800` ``` using C' A' ``` nipkow@64267 ` 801` ``` by (intro suminf_sum G.Int G.finite_Union) (auto intro: generated_ringI_Basic) ``` hoelzl@47762 ` 802` ``` also have "\ = (\c\C'. \_r c)" ``` nipkow@64267 ` 803` ``` using eq V C' by (auto intro!: sum.cong) ``` hoelzl@47762 ` 804` ``` also have "\ = \_r (\C')" ``` hoelzl@47762 ` 805` ``` using C' Un_A ``` hoelzl@47762 ` 806` ``` by (subst volume_finite_additive[symmetric, OF V(1)]) ``` haftmann@62343 ` 807` ``` (auto simp: disjoint_family_on_def disjoint_def ``` hoelzl@47762 ` 808` ``` intro: generated_ringI_Basic) ``` hoelzl@47762 ` 809` ``` finally show "(\n. \_r (A' n)) = \_r (\i. A' i)" ``` hoelzl@47762 ` 810` ``` using C' by simp ``` hoelzl@47762 ` 811` ``` qed ``` wenzelm@61808 ` 812` ``` from G.caratheodory'[OF \positive generated_ring \_r\ \countably_additive generated_ring \_r\] ``` hoelzl@47762 ` 813` ``` guess \' .. ``` hoelzl@47762 ` 814` ``` with V show ?thesis ``` hoelzl@47762 ` 815` ``` unfolding sigma_sets_generated_ring_eq ``` hoelzl@47762 ` 816` ``` by (intro exI[of _ \']) (auto intro: generated_ringI_Basic) ``` hoelzl@47762 ` 817` ```qed ``` hoelzl@47762 ` 818` ak2110@68833 ` 819` ```lemma%important extend_measure_caratheodory: ``` hoelzl@57447 ` 820` ``` fixes G :: "'i \ 'a set" ``` hoelzl@57447 ` 821` ``` assumes M: "M = extend_measure \ I G \" ``` hoelzl@57447 ` 822` ``` assumes "i \ I" ``` hoelzl@57447 ` 823` ``` assumes "semiring_of_sets \ (G ` I)" ``` hoelzl@57447 ` 824` ``` assumes empty: "\i. i \ I \ G i = {} \ \ i = 0" ``` hoelzl@57447 ` 825` ``` assumes inj: "\i j. i \ I \ j \ I \ G i = G j \ \ i = \ j" ``` hoelzl@57447 ` 826` ``` assumes nonneg: "\i. i \ I \ 0 \ \ i" ``` hoelzl@57447 ` 827` ``` assumes add: "\A::nat \ 'i. \j. A \ UNIV \ I \ j \ I \ disjoint_family (G \ A) \ ``` hoelzl@57447 ` 828` ``` (\i. G (A i)) = G j \ (\n. \ (A n)) = \ j" ``` hoelzl@57447 ` 829` ``` shows "emeasure M (G i) = \ i" ``` ak2110@68833 ` 830` ak2110@68833 ` 831` ```proof%unimportant - ``` hoelzl@57447 ` 832` ``` interpret semiring_of_sets \ "G ` I" ``` hoelzl@57447 ` 833` ``` by fact ``` hoelzl@57447 ` 834` ``` have "\g\G`I. \i\I. g = G i" ``` hoelzl@57447 ` 835` ``` by auto ``` hoelzl@57447 ` 836` ``` then obtain sel where sel: "\g. g \ G ` I \ sel g \ I" "\g. g \ G ` I \ G (sel g) = g" ``` hoelzl@57447 ` 837` ``` by metis ``` hoelzl@57447 ` 838` hoelzl@57447 ` 839` ``` have "\\'. (\s\G ` I. \' s = \ (sel s)) \ measure_space \ (sigma_sets \ (G ` I)) \'" ``` hoelzl@57447 ` 840` ``` proof (rule caratheodory) ``` hoelzl@57447 ` 841` ``` show "positive (G ` I) (\s. \ (sel s))" ``` hoelzl@57447 ` 842` ``` by (auto simp: positive_def intro!: empty sel nonneg) ``` hoelzl@57447 ` 843` ``` show "countably_additive (G ` I) (\s. \ (sel s))" ``` hoelzl@57447 ` 844` ``` proof (rule countably_additiveI) ``` hoelzl@57447 ` 845` ``` fix A :: "nat \ 'a set" assume "range A \ G ` I" "disjoint_family A" "(\i. A i) \ G ` I" ``` hoelzl@57447 ` 846` ``` then show "(\i. \ (sel (A i))) = \ (sel (\i. A i))" ``` hoelzl@57447 ` 847` ``` by (intro add) (auto simp: sel image_subset_iff_funcset comp_def Pi_iff intro!: sel) ``` hoelzl@57447 ` 848` ``` qed ``` hoelzl@57447 ` 849` ``` qed ``` hoelzl@57447 ` 850` ``` then obtain \' where \': "\s\G ` I. \' s = \ (sel s)" "measure_space \ (sigma_sets \ (G ` I)) \'" ``` hoelzl@57447 ` 851` ``` by metis ``` hoelzl@57447 ` 852` hoelzl@57447 ` 853` ``` show ?thesis ``` hoelzl@57447 ` 854` ``` proof (rule emeasure_extend_measure[OF M]) ``` hoelzl@57447 ` 855` ``` { fix i assume "i \ I" then show "\' (G i) = \ i" ``` hoelzl@57447 ` 856` ``` using \' by (auto intro!: inj sel) } ``` hoelzl@57447 ` 857` ``` show "G ` I \ Pow \" ``` wenzelm@67682 ` 858` ``` by (rule space_closed) ``` hoelzl@57447 ` 859` ``` then show "positive (sets M) \'" "countably_additive (sets M) \'" ``` hoelzl@57447 ` 860` ``` using \' by (simp_all add: M sets_extend_measure measure_space_def) ``` hoelzl@57447 ` 861` ``` qed fact ``` hoelzl@57447 ` 862` ```qed ``` hoelzl@62975 ` 863` ak2110@68833 ` 864` ```lemma%important extend_measure_caratheodory_pair: ``` hoelzl@57447 ` 865` ``` fixes G :: "'i \ 'j \ 'a set" ``` hoelzl@57447 ` 866` ``` assumes M: "M = extend_measure \ {(a, b). P a b} (\(a, b). G a b) (\(a, b). \ a b)" ``` hoelzl@57447 ` 867` ``` assumes "P i j" ``` hoelzl@57447 ` 868` ``` assumes semiring: "semiring_of_sets \ {G a b | a b. P a b}" ``` hoelzl@57447 ` 869` ``` assumes empty: "\i j. P i j \ G i j = {} \ \ i j = 0" ``` hoelzl@57447 ` 870` ``` assumes inj: "\i j k l. P i j \ P k l \ G i j = G k l \ \ i j = \ k l" ``` hoelzl@57447 ` 871` ``` assumes nonneg: "\i j. P i j \ 0 \ \ i j" ``` hoelzl@57447 ` 872` ``` assumes add: "\A::nat \ 'i. \B::nat \ 'j. \j k. ``` hoelzl@57447 ` 873` ``` (\n. P (A n) (B n)) \ P j k \ disjoint_family (\n. G (A n) (B n)) \ ``` hoelzl@57447 ` 874` ``` (\i. G (A i) (B i)) = G j k \ (\n. \ (A n) (B n)) = \ j k" ``` hoelzl@57447 ` 875` ``` shows "emeasure M (G i j) = \ i j" ``` ak2110@68833 ` 876` ```proof%unimportant - ``` hoelzl@57447 ` 877` ``` have "emeasure M ((\(a, b). G a b) (i, j)) = (\(a, b). \ a b) (i, j)" ``` hoelzl@57447 ` 878` ``` proof (rule extend_measure_caratheodory[OF M]) ``` hoelzl@57447 ` 879` ``` show "semiring_of_sets \ ((\(a, b). G a b) ` {(a, b). P a b})" ``` hoelzl@57447 ` 880` ``` using semiring by (simp add: image_def conj_commute) ``` hoelzl@57447 ` 881` ``` next ``` hoelzl@57447 ` 882` ``` fix A :: "nat \ ('i \ 'j)" and j assume "A \ UNIV \ {(a, b). P a b}" "j \ {(a, b). P a b}" ``` hoelzl@57447 ` 883` ``` "disjoint_family ((\(a, b). G a b) \ A)" ``` hoelzl@57447 ` 884` ``` "(\i. case A i of (a, b) \ G a b) = (case j of (a, b) \ G a b)" ``` hoelzl@57447 ` 885` ``` then show "(\n. case A n of (a, b) \ \ a b) = (case j of (a, b) \ \ a b)" ``` hoelzl@57447 ` 886` ``` using add[of "\i. fst (A i)" "\i. snd (A i)" "fst j" "snd j"] ``` hoelzl@57447 ` 887` ``` by (simp add: split_beta' comp_def Pi_iff) ``` hoelzl@57447 ` 888` ``` qed (auto split: prod.splits intro: assms) ``` hoelzl@57447 ` 889` ``` then show ?thesis by simp ``` hoelzl@57447 ` 890` ```qed ``` hoelzl@57447 ` 891` paulson@33271 ` 892` ```end ```