src/HOL/Probability/Caratheodory.thy
 author hoelzl Tue Mar 29 14:27:31 2011 +0200 (2011-03-29) changeset 42145 8448713d48b7 parent 42067 66c8281349ec child 42950 6e5c2a3c69da permissions -rw-r--r--
proved caratheodory_empty_continuous
 hoelzl@42067 ` 1` ```(* Title: HOL/Probability/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` paulson@33271 ` 6` ```header {*Caratheodory Extension Theorem*} ``` paulson@33271 ` 7` paulson@33271 ` 8` ```theory Caratheodory ``` hoelzl@41981 ` 9` ``` imports Sigma_Algebra Extended_Real_Limits ``` paulson@33271 ` 10` ```begin ``` paulson@33271 ` 11` hoelzl@42067 ` 12` ```text {* ``` hoelzl@42067 ` 13` ``` Originally from the Hurd/Coble measure theory development, translated by Lawrence Paulson. ``` hoelzl@42067 ` 14` ```*} ``` hoelzl@42067 ` 15` hoelzl@41981 ` 16` ```lemma suminf_extreal_2dimen: ``` hoelzl@41981 ` 17` ``` fixes f:: "nat \ nat \ extreal" ``` hoelzl@41981 ` 18` ``` assumes pos: "\p. 0 \ f p" ``` hoelzl@41981 ` 19` ``` assumes "\m. g m = (\n. f (m,n))" ``` hoelzl@41981 ` 20` ``` shows "(\i. f (prod_decode i)) = suminf g" ``` hoelzl@41981 ` 21` ```proof - ``` hoelzl@41981 ` 22` ``` have g_def: "g = (\m. (\n. f (m,n)))" ``` hoelzl@41981 ` 23` ``` using assms by (simp add: fun_eq_iff) ``` hoelzl@41981 ` 24` ``` have reindex: "\B. (\x\B. f (prod_decode x)) = setsum f (prod_decode ` B)" ``` hoelzl@41981 ` 25` ``` by (simp add: setsum_reindex[OF inj_prod_decode] comp_def) ``` hoelzl@41981 ` 26` ``` { fix n ``` hoelzl@41981 ` 27` ``` let ?M = "\f. Suc (Max (f ` prod_decode ` {.. setsum f ({.. {..a b. setsum f (prod_decode ` {.. setsum f ({.. {.. ?M" ``` hoelzl@41981 ` 38` ``` by (auto intro!: Max_ge le_imp_less_Suc image_eqI[where x="prod_encode (a', b')"]) } ``` hoelzl@41981 ` 39` ``` then have "setsum f ({.. {.. setsum f ?M" ``` hoelzl@41981 ` 40` ``` by (auto intro!: setsum_mono3 simp: pos) } ``` hoelzl@41981 ` 41` ``` ultimately ``` hoelzl@41981 ` 42` ``` show ?thesis unfolding g_def using pos ``` hoelzl@41981 ` 43` ``` by (auto intro!: SUPR_eq simp: setsum_cartesian_product reindex le_SUPI2 ``` hoelzl@41981 ` 44` ``` setsum_nonneg suminf_extreal_eq_SUPR SUPR_pair ``` hoelzl@41981 ` 45` ``` SUPR_extreal_setsum[symmetric] incseq_setsumI setsum_nonneg) ``` hoelzl@41981 ` 46` ```qed ``` hoelzl@41981 ` 47` paulson@33271 ` 48` ```subsection {* Measure Spaces *} ``` paulson@33271 ` 49` hoelzl@41689 ` 50` ```record 'a measure_space = "'a algebra" + ``` hoelzl@41981 ` 51` ``` measure :: "'a set \ extreal" ``` paulson@33271 ` 52` hoelzl@41981 ` 53` ```definition positive where "positive M f \ f {} = (0::extreal) \ (\A\sets M. 0 \ f A)" ``` paulson@33271 ` 54` hoelzl@41689 ` 55` ```definition additive where "additive M f \ ``` hoelzl@41689 ` 56` ``` (\x \ sets M. \y \ sets M. x \ y = {} \ f (x \ y) = f x + f y)" ``` paulson@33271 ` 57` hoelzl@41981 ` 58` ```definition countably_additive :: "('a, 'b) algebra_scheme \ ('a set \ extreal) \ bool" where ``` hoelzl@41981 ` 59` ``` "countably_additive M f \ (\A. range A \ sets M \ disjoint_family A \ (\i. A i) \ sets M \ ``` hoelzl@41981 ` 60` ``` (\i. f (A i)) = f (\i. A i))" ``` paulson@33271 ` 61` hoelzl@41689 ` 62` ```definition increasing where "increasing M f \ ``` hoelzl@41689 ` 63` ``` (\x \ sets M. \y \ sets M. x \ y \ f x \ f y)" ``` paulson@33271 ` 64` hoelzl@41689 ` 65` ```definition subadditive where "subadditive M f \ ``` hoelzl@41981 ` 66` ``` (\x \ sets M. \y \ sets M. x \ y = {} \ f (x \ y) \ f x + f y)" ``` paulson@33271 ` 67` hoelzl@41689 ` 68` ```definition countably_subadditive where "countably_subadditive M f \ ``` hoelzl@41689 ` 69` ``` (\A. range A \ sets M \ disjoint_family A \ (\i. A i) \ sets M \ ``` hoelzl@41981 ` 70` ``` (f (\i. A i) \ (\i. f (A i))))" ``` hoelzl@41689 ` 71` hoelzl@41689 ` 72` ```definition lambda_system where "lambda_system M f = {l \ sets M. ``` hoelzl@41689 ` 73` ``` \x \ sets M. f (l \ x) + f ((space M - l) \ x) = f x}" ``` paulson@33271 ` 74` hoelzl@41689 ` 75` ```definition outer_measure_space where "outer_measure_space M f \ ``` hoelzl@41689 ` 76` ``` positive M f \ increasing M f \ countably_subadditive M f" ``` hoelzl@41689 ` 77` hoelzl@41689 ` 78` ```definition measure_set where "measure_set M f X = {r. ``` hoelzl@41981 ` 79` ``` \A. range A \ sets M \ disjoint_family A \ X \ (\i. A i) \ (\i. f (A i)) = r}" ``` paulson@33271 ` 80` hoelzl@41689 ` 81` ```locale measure_space = sigma_algebra M for M :: "('a, 'b) measure_space_scheme" + ``` hoelzl@41981 ` 82` ``` assumes measure_positive: "positive M (measure M)" ``` hoelzl@41689 ` 83` ``` and ca: "countably_additive M (measure M)" ``` paulson@33271 ` 84` hoelzl@41689 ` 85` ```abbreviation (in measure_space) "\ \ measure M" ``` paulson@33271 ` 86` hoelzl@41981 ` 87` ```lemma (in measure_space) ``` hoelzl@41981 ` 88` ``` shows empty_measure[simp, intro]: "\ {} = 0" ``` hoelzl@41981 ` 89` ``` and positive_measure[simp, intro!]: "\A. A \ sets M \ 0 \ \ A" ``` hoelzl@41981 ` 90` ``` using measure_positive unfolding positive_def by auto ``` hoelzl@41981 ` 91` paulson@33271 ` 92` ```lemma increasingD: ``` hoelzl@41689 ` 93` ``` "increasing M f \ x \ y \ x\sets M \ y\sets M \ f x \ f y" ``` paulson@33271 ` 94` ``` by (auto simp add: increasing_def) ``` paulson@33271 ` 95` paulson@33271 ` 96` ```lemma subadditiveD: ``` hoelzl@41689 ` 97` ``` "subadditive M f \ x \ y = {} \ x \ sets M \ y \ sets M ``` hoelzl@41689 ` 98` ``` \ f (x \ y) \ f x + f y" ``` paulson@33271 ` 99` ``` by (auto simp add: subadditive_def) ``` paulson@33271 ` 100` paulson@33271 ` 101` ```lemma additiveD: ``` hoelzl@41689 ` 102` ``` "additive M f \ x \ y = {} \ x \ sets M \ y \ sets M ``` hoelzl@41689 ` 103` ``` \ f (x \ y) = f x + f y" ``` paulson@33271 ` 104` ``` by (auto simp add: additive_def) ``` paulson@33271 ` 105` hoelzl@41689 ` 106` ```lemma countably_additiveI: ``` hoelzl@41981 ` 107` ``` assumes "\A x. range A \ sets M \ disjoint_family A \ (\i. A i) \ sets M ``` hoelzl@41981 ` 108` ``` \ (\i. f (A i)) = f (\i. A i)" ``` hoelzl@41981 ` 109` ``` shows "countably_additive M f" ``` hoelzl@41981 ` 110` ``` using assms by (simp add: countably_additive_def) ``` paulson@33271 ` 111` hoelzl@38656 ` 112` ```section "Extend binary sets" ``` paulson@33271 ` 113` hoelzl@35582 ` 114` ```lemma LIMSEQ_binaryset: ``` paulson@33271 ` 115` ``` assumes f: "f {} = 0" ``` hoelzl@41981 ` 116` ``` shows "(\n. \i f A + f B" ``` paulson@33271 ` 117` ```proof - ``` hoelzl@41981 ` 118` ``` have "(\n. \i < Suc (Suc n). f (binaryset A B i)) = (\n. f A + f B)" ``` hoelzl@35582 ` 119` ``` proof ``` paulson@33271 ` 120` ``` fix n ``` hoelzl@41981 ` 121` ``` show "(\i < Suc (Suc n). f (binaryset A B i)) = f A + f B" ``` hoelzl@35582 ` 122` ``` by (induct n) (auto simp add: binaryset_def f) ``` paulson@33271 ` 123` ``` qed ``` paulson@33271 ` 124` ``` moreover ``` hoelzl@35582 ` 125` ``` have "... ----> f A + f B" by (rule LIMSEQ_const) ``` paulson@33271 ` 126` ``` ultimately ``` hoelzl@41981 ` 127` ``` have "(\n. \i< Suc (Suc n). f (binaryset A B i)) ----> f A + f B" ``` paulson@33271 ` 128` ``` by metis ``` hoelzl@41981 ` 129` ``` hence "(\n. \i< n+2. f (binaryset A B i)) ----> f A + f B" ``` paulson@33271 ` 130` ``` by simp ``` paulson@33271 ` 131` ``` thus ?thesis by (rule LIMSEQ_offset [where k=2]) ``` paulson@33271 ` 132` ```qed ``` paulson@33271 ` 133` paulson@33271 ` 134` ```lemma binaryset_sums: ``` paulson@33271 ` 135` ``` assumes f: "f {} = 0" ``` paulson@33271 ` 136` ``` shows "(\n. f (binaryset A B n)) sums (f A + f B)" ``` hoelzl@41981 ` 137` ``` by (simp add: sums_def LIMSEQ_binaryset [where f=f, OF f] atLeast0LessThan) ``` paulson@33271 ` 138` paulson@33271 ` 139` ```lemma suminf_binaryset_eq: ``` hoelzl@41981 ` 140` ``` fixes f :: "'a set \ 'b::{comm_monoid_add, t2_space}" ``` hoelzl@41689 ` 141` ``` shows "f {} = 0 \ (\n. f (binaryset A B n)) = f A + f B" ``` paulson@33271 ` 142` ``` by (metis binaryset_sums sums_unique) ``` paulson@33271 ` 143` paulson@33271 ` 144` ```subsection {* Lambda Systems *} ``` paulson@33271 ` 145` paulson@33271 ` 146` ```lemma (in algebra) lambda_system_eq: ``` hoelzl@41689 ` 147` ``` shows "lambda_system M f = {l \ sets M. ``` hoelzl@41689 ` 148` ``` \x \ sets M. f (x \ l) + f (x - l) = f x}" ``` paulson@33271 ` 149` ```proof - ``` paulson@33271 ` 150` ``` have [simp]: "!!l x. l \ sets M \ x \ sets M \ (space M - l) \ x = x - l" ``` huffman@37032 ` 151` ``` by (metis Int_Diff Int_absorb1 Int_commute sets_into_space) ``` paulson@33271 ` 152` ``` show ?thesis ``` huffman@37032 ` 153` ``` by (auto simp add: lambda_system_def) (metis Int_commute)+ ``` paulson@33271 ` 154` ```qed ``` paulson@33271 ` 155` paulson@33271 ` 156` ```lemma (in algebra) lambda_system_empty: ``` hoelzl@41689 ` 157` ``` "positive M f \ {} \ lambda_system M f" ``` hoelzl@42066 ` 158` ``` by (auto simp add: positive_def lambda_system_eq) ``` paulson@33271 ` 159` paulson@33271 ` 160` ```lemma lambda_system_sets: ``` hoelzl@41689 ` 161` ``` "x \ lambda_system M f \ x \ sets M" ``` hoelzl@41689 ` 162` ``` by (simp add: lambda_system_def) ``` paulson@33271 ` 163` paulson@33271 ` 164` ```lemma (in algebra) lambda_system_Compl: ``` hoelzl@41981 ` 165` ``` fixes f:: "'a set \ extreal" ``` paulson@33271 ` 166` ``` assumes x: "x \ lambda_system M f" ``` paulson@33271 ` 167` ``` shows "space M - x \ lambda_system M f" ``` hoelzl@41689 ` 168` ```proof - ``` hoelzl@41689 ` 169` ``` have "x \ space M" ``` hoelzl@41689 ` 170` ``` by (metis sets_into_space lambda_system_sets x) ``` hoelzl@41689 ` 171` ``` hence "space M - (space M - x) = x" ``` hoelzl@41689 ` 172` ``` by (metis double_diff equalityE) ``` hoelzl@41689 ` 173` ``` with x show ?thesis ``` hoelzl@41689 ` 174` ``` by (force simp add: lambda_system_def ac_simps) ``` hoelzl@41689 ` 175` ```qed ``` paulson@33271 ` 176` paulson@33271 ` 177` ```lemma (in algebra) lambda_system_Int: ``` hoelzl@41981 ` 178` ``` fixes f:: "'a set \ extreal" ``` paulson@33271 ` 179` ``` assumes xl: "x \ lambda_system M f" and yl: "y \ lambda_system M f" ``` paulson@33271 ` 180` ``` shows "x \ y \ lambda_system M f" ``` hoelzl@41689 ` 181` ```proof - ``` hoelzl@41689 ` 182` ``` from xl yl show ?thesis ``` hoelzl@41689 ` 183` ``` proof (auto simp add: positive_def lambda_system_eq Int) ``` hoelzl@41689 ` 184` ``` fix u ``` hoelzl@41689 ` 185` ``` assume x: "x \ sets M" and y: "y \ sets M" and u: "u \ sets M" ``` hoelzl@41689 ` 186` ``` and fx: "\z\sets M. f (z \ x) + f (z - x) = f z" ``` hoelzl@41689 ` 187` ``` and fy: "\z\sets M. f (z \ y) + f (z - y) = f z" ``` hoelzl@41689 ` 188` ``` have "u - x \ y \ sets M" ``` hoelzl@41689 ` 189` ``` by (metis Diff Diff_Int Un u x y) ``` hoelzl@41689 ` 190` ``` moreover ``` hoelzl@41689 ` 191` ``` have "(u - (x \ y)) \ y = u \ y - x" by blast ``` hoelzl@41689 ` 192` ``` moreover ``` hoelzl@41689 ` 193` ``` have "u - x \ y - y = u - y" by blast ``` hoelzl@41689 ` 194` ``` ultimately ``` hoelzl@41689 ` 195` ``` have ey: "f (u - x \ y) = f (u \ y - x) + f (u - y)" using fy ``` hoelzl@41689 ` 196` ``` by force ``` hoelzl@41689 ` 197` ``` have "f (u \ (x \ y)) + f (u - x \ y) ``` hoelzl@41689 ` 198` ``` = (f (u \ (x \ y)) + f (u \ y - x)) + f (u - y)" ``` hoelzl@41689 ` 199` ``` by (simp add: ey ac_simps) ``` hoelzl@41689 ` 200` ``` also have "... = (f ((u \ y) \ x) + f (u \ y - x)) + f (u - y)" ``` hoelzl@41689 ` 201` ``` by (simp add: Int_ac) ``` hoelzl@41689 ` 202` ``` also have "... = f (u \ y) + f (u - y)" ``` hoelzl@41689 ` 203` ``` using fx [THEN bspec, of "u \ y"] Int y u ``` hoelzl@41689 ` 204` ``` by force ``` hoelzl@41689 ` 205` ``` also have "... = f u" ``` hoelzl@41689 ` 206` ``` by (metis fy u) ``` hoelzl@41689 ` 207` ``` finally show "f (u \ (x \ y)) + f (u - x \ y) = f u" . ``` paulson@33271 ` 208` ``` qed ``` hoelzl@41689 ` 209` ```qed ``` paulson@33271 ` 210` paulson@33271 ` 211` ```lemma (in algebra) lambda_system_Un: ``` hoelzl@41981 ` 212` ``` fixes f:: "'a set \ extreal" ``` paulson@33271 ` 213` ``` assumes xl: "x \ lambda_system M f" and yl: "y \ lambda_system M f" ``` paulson@33271 ` 214` ``` shows "x \ y \ lambda_system M f" ``` paulson@33271 ` 215` ```proof - ``` paulson@33271 ` 216` ``` have "(space M - x) \ (space M - y) \ sets M" ``` hoelzl@38656 ` 217` ``` by (metis Diff_Un Un compl_sets lambda_system_sets xl yl) ``` paulson@33271 ` 218` ``` moreover ``` paulson@33271 ` 219` ``` have "x \ y = space M - ((space M - x) \ (space M - y))" ``` paulson@33271 ` 220` ``` by auto (metis subsetD lambda_system_sets sets_into_space xl yl)+ ``` paulson@33271 ` 221` ``` ultimately show ?thesis ``` hoelzl@38656 ` 222` ``` by (metis lambda_system_Compl lambda_system_Int xl yl) ``` paulson@33271 ` 223` ```qed ``` paulson@33271 ` 224` paulson@33271 ` 225` ```lemma (in algebra) lambda_system_algebra: ``` hoelzl@41689 ` 226` ``` "positive M f \ algebra (M\sets := lambda_system M f\)" ``` hoelzl@42065 ` 227` ``` apply (auto simp add: algebra_iff_Un) ``` paulson@33271 ` 228` ``` apply (metis lambda_system_sets set_mp sets_into_space) ``` paulson@33271 ` 229` ``` apply (metis lambda_system_empty) ``` paulson@33271 ` 230` ``` apply (metis lambda_system_Compl) ``` hoelzl@38656 ` 231` ``` apply (metis lambda_system_Un) ``` paulson@33271 ` 232` ``` done ``` paulson@33271 ` 233` paulson@33271 ` 234` ```lemma (in algebra) lambda_system_strong_additive: ``` paulson@33271 ` 235` ``` assumes z: "z \ sets M" and disj: "x \ y = {}" ``` paulson@33271 ` 236` ``` and xl: "x \ lambda_system M f" and yl: "y \ lambda_system M f" ``` paulson@33271 ` 237` ``` shows "f (z \ (x \ y)) = f (z \ x) + f (z \ y)" ``` hoelzl@41689 ` 238` ```proof - ``` hoelzl@41689 ` 239` ``` have "z \ x = (z \ (x \ y)) \ x" using disj by blast ``` hoelzl@41689 ` 240` ``` moreover ``` hoelzl@41689 ` 241` ``` have "z \ y = (z \ (x \ y)) - x" using disj by blast ``` hoelzl@41689 ` 242` ``` moreover ``` hoelzl@41689 ` 243` ``` have "(z \ (x \ y)) \ sets M" ``` hoelzl@41689 ` 244` ``` by (metis Int Un lambda_system_sets xl yl z) ``` hoelzl@41689 ` 245` ``` ultimately show ?thesis using xl yl ``` hoelzl@41689 ` 246` ``` by (simp add: lambda_system_eq) ``` hoelzl@41689 ` 247` ```qed ``` paulson@33271 ` 248` paulson@33271 ` 249` ```lemma (in algebra) lambda_system_additive: ``` paulson@33271 ` 250` ``` "additive (M (|sets := lambda_system M f|)) f" ``` hoelzl@41689 ` 251` ```proof (auto simp add: additive_def) ``` hoelzl@41689 ` 252` ``` fix x and y ``` hoelzl@41689 ` 253` ``` assume disj: "x \ y = {}" ``` hoelzl@41689 ` 254` ``` and xl: "x \ lambda_system M f" and yl: "y \ lambda_system M f" ``` hoelzl@41689 ` 255` ``` hence "x \ sets M" "y \ sets M" by (blast intro: lambda_system_sets)+ ``` hoelzl@41689 ` 256` ``` thus "f (x \ y) = f x + f y" ``` hoelzl@41689 ` 257` ``` using lambda_system_strong_additive [OF top disj xl yl] ``` hoelzl@41689 ` 258` ``` by (simp add: Un) ``` hoelzl@41689 ` 259` ```qed ``` paulson@33271 ` 260` hoelzl@42145 ` 261` ```lemma (in ring_of_sets) disjointed_additive: ``` hoelzl@42145 ` 262` ``` assumes f: "positive M f" "additive M f" and A: "range A \ sets M" "incseq A" ``` hoelzl@42145 ` 263` ``` shows "(\i\n. f (disjointed A i)) = f (A n)" ``` hoelzl@42145 ` 264` ```proof (induct n) ``` hoelzl@42145 ` 265` ``` case (Suc n) ``` hoelzl@42145 ` 266` ``` then have "(\i\Suc n. f (disjointed A i)) = f (A n) + f (disjointed A (Suc n))" ``` hoelzl@42145 ` 267` ``` by simp ``` hoelzl@42145 ` 268` ``` also have "\ = f (A n \ disjointed A (Suc n))" ``` hoelzl@42145 ` 269` ``` using A by (subst f(2)[THEN additiveD]) (auto simp: disjointed_incseq) ``` hoelzl@42145 ` 270` ``` also have "A n \ disjointed A (Suc n) = A (Suc n)" ``` hoelzl@42145 ` 271` ``` using `incseq A` by (auto dest: incseq_SucD simp: disjointed_incseq) ``` hoelzl@42145 ` 272` ``` finally show ?case . ``` hoelzl@42145 ` 273` ```qed simp ``` hoelzl@42145 ` 274` hoelzl@42145 ` 275` ```lemma (in ring_of_sets) countably_subadditive_subadditive: ``` hoelzl@41689 ` 276` ``` assumes f: "positive M f" and cs: "countably_subadditive M f" ``` paulson@33271 ` 277` ``` shows "subadditive M f" ``` hoelzl@35582 ` 278` ```proof (auto simp add: subadditive_def) ``` paulson@33271 ` 279` ``` fix x y ``` paulson@33271 ` 280` ``` assume x: "x \ sets M" and y: "y \ sets M" and "x \ y = {}" ``` paulson@33271 ` 281` ``` hence "disjoint_family (binaryset x y)" ``` hoelzl@35582 ` 282` ``` by (auto simp add: disjoint_family_on_def binaryset_def) ``` hoelzl@35582 ` 283` ``` hence "range (binaryset x y) \ sets M \ ``` hoelzl@35582 ` 284` ``` (\i. binaryset x y i) \ sets M \ ``` hoelzl@41981 ` 285` ``` f (\i. binaryset x y i) \ (\ n. f (binaryset x y n))" ``` hoelzl@41981 ` 286` ``` using cs by (auto simp add: countably_subadditive_def) ``` hoelzl@35582 ` 287` ``` hence "{x,y,{}} \ sets M \ x \ y \ sets M \ ``` hoelzl@41981 ` 288` ``` f (x \ y) \ (\ n. f (binaryset x y n))" ``` paulson@33271 ` 289` ``` by (simp add: range_binaryset_eq UN_binaryset_eq) ``` hoelzl@38656 ` 290` ``` thus "f (x \ y) \ f x + f y" using f x y ``` hoelzl@41981 ` 291` ``` by (auto simp add: Un o_def suminf_binaryset_eq positive_def) ``` paulson@33271 ` 292` ```qed ``` paulson@33271 ` 293` hoelzl@42145 ` 294` ```lemma (in ring_of_sets) additive_sum: ``` paulson@33271 ` 295` ``` fixes A:: "nat \ 'a set" ``` hoelzl@41981 ` 296` ``` assumes f: "positive M f" and ad: "additive M f" and "finite S" ``` paulson@33271 ` 297` ``` and A: "range A \ sets M" ``` hoelzl@41981 ` 298` ``` and disj: "disjoint_family_on A S" ``` hoelzl@41981 ` 299` ``` shows "(\i\S. f (A i)) = f (\i\S. A i)" ``` hoelzl@41981 ` 300` ```using `finite S` disj proof induct ``` hoelzl@41981 ` 301` ``` case empty show ?case using f by (simp add: positive_def) ``` paulson@33271 ` 302` ```next ``` hoelzl@41981 ` 303` ``` case (insert s S) ``` hoelzl@41981 ` 304` ``` then have "A s \ (\i\S. A i) = {}" ``` hoelzl@41981 ` 305` ``` by (auto simp add: disjoint_family_on_def neq_iff) ``` hoelzl@38656 ` 306` ``` moreover ``` hoelzl@41981 ` 307` ``` have "A s \ sets M" using A by blast ``` hoelzl@41981 ` 308` ``` moreover have "(\i\S. A i) \ sets M" ``` hoelzl@41981 ` 309` ``` using A `finite S` by auto ``` hoelzl@38656 ` 310` ``` moreover ``` hoelzl@41981 ` 311` ``` ultimately have "f (A s \ (\i\S. A i)) = f (A s) + f(\i\S. A i)" ``` hoelzl@38656 ` 312` ``` using ad UNION_in_sets A by (auto simp add: additive_def) ``` hoelzl@41981 ` 313` ``` with insert show ?case using ad disjoint_family_on_mono[of S "insert s S" A] ``` hoelzl@41981 ` 314` ``` by (auto simp add: additive_def subset_insertI) ``` paulson@33271 ` 315` ```qed ``` paulson@33271 ` 316` hoelzl@38656 ` 317` ```lemma (in algebra) increasing_additive_bound: ``` hoelzl@41981 ` 318` ``` fixes A:: "nat \ 'a set" and f :: "'a set \ extreal" ``` hoelzl@41689 ` 319` ``` assumes f: "positive M f" and ad: "additive M f" ``` paulson@33271 ` 320` ``` and inc: "increasing M f" ``` paulson@33271 ` 321` ``` and A: "range A \ sets M" ``` paulson@33271 ` 322` ``` and disj: "disjoint_family A" ``` hoelzl@41981 ` 323` ``` shows "(\i. f (A i)) \ f (space M)" ``` hoelzl@41981 ` 324` ```proof (safe intro!: suminf_bound) ``` hoelzl@38656 ` 325` ``` fix N ``` hoelzl@41981 ` 326` ``` note disj_N = disjoint_family_on_mono[OF _ disj, of "{..ii\{.. f (space M)" using space_closed A ``` hoelzl@41981 ` 330` ``` by (intro increasingD[OF inc] finite_UN) auto ``` hoelzl@41981 ` 331` ``` finally show "(\i f (space M)" by simp ``` hoelzl@41981 ` 332` ```qed (insert f A, auto simp: positive_def) ``` paulson@33271 ` 333` paulson@33271 ` 334` ```lemma lambda_system_increasing: ``` hoelzl@41689 ` 335` ``` "increasing M f \ increasing (M (|sets := lambda_system M f|)) f" ``` hoelzl@38656 ` 336` ``` by (simp add: increasing_def lambda_system_def) ``` paulson@33271 ` 337` hoelzl@41689 ` 338` ```lemma lambda_system_positive: ``` hoelzl@41689 ` 339` ``` "positive M f \ positive (M (|sets := lambda_system M f|)) f" ``` hoelzl@41689 ` 340` ``` by (simp add: positive_def lambda_system_def) ``` hoelzl@41689 ` 341` paulson@33271 ` 342` ```lemma (in algebra) lambda_system_strong_sum: ``` hoelzl@41981 ` 343` ``` fixes A:: "nat \ 'a set" and f :: "'a set \ extreal" ``` hoelzl@41689 ` 344` ``` assumes f: "positive M f" and a: "a \ sets M" ``` paulson@33271 ` 345` ``` and A: "range A \ lambda_system M f" ``` paulson@33271 ` 346` ``` and disj: "disjoint_family A" ``` paulson@33271 ` 347` ``` shows "(\i = 0..A i)) = f (a \ (\i\{0.. UNION {0.. lambda_system M f" using A ``` paulson@33271 ` 355` ``` by blast ``` hoelzl@42065 ` 356` ``` interpret l: algebra "M\sets := lambda_system M f\" ``` hoelzl@42065 ` 357` ``` using f by (rule lambda_system_algebra) ``` paulson@33271 ` 358` ``` have 4: "UNION {0.. lambda_system M f" ``` hoelzl@42065 ` 359` ``` using A l.UNION_in_sets by simp ``` paulson@33271 ` 360` ``` from Suc.hyps show ?case ``` paulson@33271 ` 361` ``` by (simp add: atLeastLessThanSuc lambda_system_strong_additive [OF a 2 3 4]) ``` paulson@33271 ` 362` ```qed ``` paulson@33271 ` 363` paulson@33271 ` 364` ```lemma (in sigma_algebra) lambda_system_caratheodory: ``` paulson@33271 ` 365` ``` assumes oms: "outer_measure_space M f" ``` paulson@33271 ` 366` ``` and A: "range A \ lambda_system M f" ``` paulson@33271 ` 367` ``` and disj: "disjoint_family A" ``` hoelzl@41981 ` 368` ``` shows "(\i. A i) \ lambda_system M f \ (\i. f (A i)) = f (\i. A i)" ``` paulson@33271 ` 369` ```proof - ``` hoelzl@41689 ` 370` ``` have pos: "positive M f" and inc: "increasing M f" ``` hoelzl@38656 ` 371` ``` and csa: "countably_subadditive M f" ``` paulson@33271 ` 372` ``` by (metis oms outer_measure_space_def)+ ``` paulson@33271 ` 373` ``` have sa: "subadditive M f" ``` hoelzl@38656 ` 374` ``` by (metis countably_subadditive_subadditive csa pos) ``` hoelzl@38656 ` 375` ``` have A': "range A \ sets (M(|sets := lambda_system M f|))" using A ``` paulson@33271 ` 376` ``` by simp ``` hoelzl@42065 ` 377` ``` interpret ls: algebra "M\sets := lambda_system M f\" ``` hoelzl@42065 ` 378` ``` using pos by (rule lambda_system_algebra) ``` paulson@33271 ` 379` ``` have A'': "range A \ sets M" ``` paulson@33271 ` 380` ``` by (metis A image_subset_iff lambda_system_sets) ``` hoelzl@38656 ` 381` paulson@33271 ` 382` ``` have U_in: "(\i. A i) \ sets M" ``` huffman@37032 ` 383` ``` by (metis A'' countable_UN) ``` hoelzl@41981 ` 384` ``` have U_eq: "f (\i. A i) = (\i. f (A i))" ``` hoelzl@41689 ` 385` ``` proof (rule antisym) ``` hoelzl@41981 ` 386` ``` show "f (\i. A i) \ (\i. f (A i))" ``` hoelzl@41981 ` 387` ``` using csa[unfolded countably_subadditive_def] A'' disj U_in by auto ``` hoelzl@41981 ` 388` ``` have *: "\i. 0 \ f (A i)" using pos A'' unfolding positive_def by auto ``` hoelzl@41981 ` 389` ``` have dis: "\N. disjoint_family_on A {..i. f (A i)) \ f (\i. A i)" ``` hoelzl@42065 ` 391` ``` using ls.additive_sum [OF lambda_system_positive[OF pos] lambda_system_additive _ A' dis] ``` hoelzl@41981 ` 392` ``` using A'' ``` hoelzl@41981 ` 393` ``` by (intro suminf_bound[OF _ *]) (auto intro!: increasingD[OF inc] allI countable_UN) ``` hoelzl@41689 ` 394` ``` qed ``` paulson@33271 ` 395` ``` { ``` hoelzl@38656 ` 396` ``` fix a ``` hoelzl@38656 ` 397` ``` assume a [iff]: "a \ sets M" ``` paulson@33271 ` 398` ``` have "f (a \ (\i. A i)) + f (a - (\i. A i)) = f a" ``` paulson@33271 ` 399` ``` proof - ``` paulson@33271 ` 400` ``` show ?thesis ``` paulson@33271 ` 401` ``` proof (rule antisym) ``` wenzelm@33536 ` 402` ``` have "range (\i. a \ A i) \ sets M" using A'' ``` wenzelm@33536 ` 403` ``` by blast ``` hoelzl@38656 ` 404` ``` moreover ``` wenzelm@33536 ` 405` ``` have "disjoint_family (\i. a \ A i)" using disj ``` hoelzl@38656 ` 406` ``` by (auto simp add: disjoint_family_on_def) ``` hoelzl@38656 ` 407` ``` moreover ``` wenzelm@33536 ` 408` ``` have "a \ (\i. A i) \ sets M" ``` wenzelm@33536 ` 409` ``` by (metis Int U_in a) ``` hoelzl@38656 ` 410` ``` ultimately ``` hoelzl@41981 ` 411` ``` have "f (a \ (\i. A i)) \ (\i. f (a \ A i))" ``` hoelzl@41981 ` 412` ``` using csa[unfolded countably_subadditive_def, rule_format, of "(\i. a \ A i)"] ``` hoelzl@38656 ` 413` ``` by (simp add: o_def) ``` hoelzl@38656 ` 414` ``` hence "f (a \ (\i. A i)) + f (a - (\i. A i)) \ ``` hoelzl@41981 ` 415` ``` (\i. f (a \ A i)) + f (a - (\i. A i))" ``` hoelzl@38656 ` 416` ``` by (rule add_right_mono) ``` hoelzl@38656 ` 417` ``` moreover ``` hoelzl@41981 ` 418` ``` have "(\i. f (a \ A i)) + f (a - (\i. A i)) \ f a" ``` hoelzl@41981 ` 419` ``` proof (intro suminf_bound_add allI) ``` wenzelm@33536 ` 420` ``` fix n ``` wenzelm@33536 ` 421` ``` have UNION_in: "(\i\{0.. sets M" ``` hoelzl@38656 ` 422` ``` by (metis A'' UNION_in_sets) ``` wenzelm@33536 ` 423` ``` have le_fa: "f (UNION {0.. a) \ f a" using A'' ``` huffman@37032 ` 424` ``` by (blast intro: increasingD [OF inc] A'' UNION_in_sets) ``` wenzelm@33536 ` 425` ``` have ls: "(\i\{0.. lambda_system M f" ``` hoelzl@42065 ` 426` ``` using ls.UNION_in_sets by (simp add: A) ``` hoelzl@38656 ` 427` ``` 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@38656 ` 433` ``` by (simp add: lambda_system_strong_sum pos A disj eq_fa add_left_mono atLeast0LessThan[symmetric]) ``` hoelzl@41981 ` 434` ``` next ``` hoelzl@41981 ` 435` ``` have "\i. a \ A i \ sets M" using A'' by auto ``` hoelzl@41981 ` 436` ``` then show "\i. 0 \ f (a \ A i)" using pos[unfolded positive_def] by auto ``` hoelzl@41981 ` 437` ``` have "\i. a - (\i. A i) \ sets M" using A'' by auto ``` hoelzl@41981 ` 438` ``` then have "\i. 0 \ f (a - (\i. A i))" using pos[unfolded positive_def] by auto ``` hoelzl@41981 ` 439` ``` then show "f (a - (\i. A i)) \ -\" by auto ``` wenzelm@33536 ` 440` ``` qed ``` hoelzl@38656 ` 441` ``` ultimately show "f (a \ (\i. A i)) + f (a - (\i. A i)) \ f a" ``` hoelzl@38656 ` 442` ``` by (rule order_trans) ``` paulson@33271 ` 443` ``` next ``` hoelzl@38656 ` 444` ``` have "f a \ f (a \ (\i. A i) \ (a - (\i. A i)))" ``` huffman@37032 ` 445` ``` by (blast intro: increasingD [OF inc] U_in) ``` wenzelm@33536 ` 446` ``` also have "... \ f (a \ (\i. A i)) + f (a - (\i. A i))" ``` huffman@37032 ` 447` ``` by (blast intro: subadditiveD [OF sa] U_in) ``` wenzelm@33536 ` 448` ``` finally show "f a \ f (a \ (\i. A i)) + f (a - (\i. A i))" . ``` paulson@33271 ` 449` ``` qed ``` paulson@33271 ` 450` ``` qed ``` paulson@33271 ` 451` ``` } ``` paulson@33271 ` 452` ``` thus ?thesis ``` hoelzl@38656 ` 453` ``` by (simp add: lambda_system_eq sums_iff U_eq U_in) ``` paulson@33271 ` 454` ```qed ``` paulson@33271 ` 455` paulson@33271 ` 456` ```lemma (in sigma_algebra) caratheodory_lemma: ``` paulson@33271 ` 457` ``` assumes oms: "outer_measure_space M f" ``` hoelzl@41689 ` 458` ``` shows "measure_space \ space = space M, sets = lambda_system M f, measure = f \" ``` hoelzl@41689 ` 459` ``` (is "measure_space ?M") ``` paulson@33271 ` 460` ```proof - ``` hoelzl@41689 ` 461` ``` have pos: "positive M f" ``` paulson@33271 ` 462` ``` by (metis oms outer_measure_space_def) ``` hoelzl@41689 ` 463` ``` have alg: "algebra ?M" ``` hoelzl@38656 ` 464` ``` using lambda_system_algebra [of f, OF pos] ``` hoelzl@42065 ` 465` ``` by (simp add: algebra_iff_Un) ``` hoelzl@42065 ` 466` ``` then ``` hoelzl@41689 ` 467` ``` have "sigma_algebra ?M" ``` paulson@33271 ` 468` ``` using lambda_system_caratheodory [OF oms] ``` hoelzl@38656 ` 469` ``` by (simp add: sigma_algebra_disjoint_iff) ``` hoelzl@38656 ` 470` ``` moreover ``` hoelzl@41689 ` 471` ``` have "measure_space_axioms ?M" ``` paulson@33271 ` 472` ``` using pos lambda_system_caratheodory [OF oms] ``` hoelzl@38656 ` 473` ``` by (simp add: measure_space_axioms_def positive_def lambda_system_sets ``` hoelzl@38656 ` 474` ``` countably_additive_def o_def) ``` hoelzl@38656 ` 475` ``` ultimately ``` paulson@33271 ` 476` ``` show ?thesis ``` hoelzl@42065 ` 477` ``` by (simp add: measure_space_def) ``` paulson@33271 ` 478` ```qed ``` paulson@33271 ` 479` hoelzl@42066 ` 480` ```lemma (in ring_of_sets) additive_increasing: ``` hoelzl@41689 ` 481` ``` assumes posf: "positive M f" and addf: "additive M f" ``` paulson@33271 ` 482` ``` shows "increasing M f" ``` hoelzl@38656 ` 483` ```proof (auto simp add: increasing_def) ``` paulson@33271 ` 484` ``` fix x y ``` paulson@33271 ` 485` ``` assume xy: "x \ sets M" "y \ sets M" "x \ y" ``` hoelzl@41981 ` 486` ``` then have "y - x \ sets M" by auto ``` hoelzl@41981 ` 487` ``` then have "0 \ f (y-x)" using posf[unfolded positive_def] by auto ``` hoelzl@41981 ` 488` ``` then have "f x + 0 \ f x + f (y-x)" by (intro add_left_mono) auto ``` paulson@33271 ` 489` ``` also have "... = f (x \ (y-x))" using addf ``` huffman@37032 ` 490` ``` by (auto simp add: additive_def) (metis Diff_disjoint Un_Diff_cancel Diff xy(1,2)) ``` paulson@33271 ` 491` ``` also have "... = f y" ``` huffman@37032 ` 492` ``` by (metis Un_Diff_cancel Un_absorb1 xy(3)) ``` hoelzl@41981 ` 493` ``` finally show "f x \ f y" by simp ``` paulson@33271 ` 494` ```qed ``` paulson@33271 ` 495` hoelzl@42066 ` 496` ```lemma (in ring_of_sets) countably_additive_additive: ``` hoelzl@41689 ` 497` ``` assumes posf: "positive M f" and ca: "countably_additive M f" ``` paulson@33271 ` 498` ``` shows "additive M f" ``` hoelzl@38656 ` 499` ```proof (auto simp add: additive_def) ``` paulson@33271 ` 500` ``` fix x y ``` paulson@33271 ` 501` ``` assume x: "x \ sets M" and y: "y \ sets M" and "x \ y = {}" ``` paulson@33271 ` 502` ``` hence "disjoint_family (binaryset x y)" ``` hoelzl@38656 ` 503` ``` by (auto simp add: disjoint_family_on_def binaryset_def) ``` hoelzl@38656 ` 504` ``` hence "range (binaryset x y) \ sets M \ ``` hoelzl@38656 ` 505` ``` (\i. binaryset x y i) \ sets M \ ``` hoelzl@41981 ` 506` ``` f (\i. binaryset x y i) = (\ n. f (binaryset x y n))" ``` paulson@33271 ` 507` ``` using ca ``` hoelzl@38656 ` 508` ``` by (simp add: countably_additive_def) ``` hoelzl@38656 ` 509` ``` hence "{x,y,{}} \ sets M \ x \ y \ sets M \ ``` hoelzl@41981 ` 510` ``` f (x \ y) = (\n. f (binaryset x y n))" ``` paulson@33271 ` 511` ``` by (simp add: range_binaryset_eq UN_binaryset_eq) ``` paulson@33271 ` 512` ``` thus "f (x \ y) = f x + f y" using posf x y ``` hoelzl@41981 ` 513` ``` by (auto simp add: Un suminf_binaryset_eq positive_def) ``` hoelzl@38656 ` 514` ```qed ``` hoelzl@38656 ` 515` hoelzl@39096 ` 516` ```lemma inf_measure_nonempty: ``` hoelzl@41689 ` 517` ``` assumes f: "positive M f" and b: "b \ sets M" and a: "a \ b" "{} \ sets M" ``` hoelzl@39096 ` 518` ``` shows "f b \ measure_set M f a" ``` hoelzl@39096 ` 519` ```proof - ``` hoelzl@41981 ` 520` ``` let ?A = "\i::nat. (if i = 0 then b else {})" ``` hoelzl@41981 ` 521` ``` have "(\i. f (?A i)) = (\i<1::nat. f (?A i))" ``` hoelzl@41981 ` 522` ``` by (rule suminf_finite) (simp add: f[unfolded positive_def]) ``` hoelzl@39096 ` 523` ``` also have "... = f b" ``` hoelzl@39096 ` 524` ``` by simp ``` hoelzl@41981 ` 525` ``` finally show ?thesis using assms ``` hoelzl@41981 ` 526` ``` by (auto intro!: exI [of _ ?A] ``` hoelzl@39096 ` 527` ``` simp: measure_set_def disjoint_family_on_def split_if_mem2 comp_def) ``` hoelzl@39096 ` 528` ```qed ``` hoelzl@39096 ` 529` hoelzl@42066 ` 530` ```lemma (in ring_of_sets) inf_measure_agrees: ``` hoelzl@41689 ` 531` ``` assumes posf: "positive M f" and ca: "countably_additive M f" ``` hoelzl@38656 ` 532` ``` and s: "s \ sets M" ``` paulson@33271 ` 533` ``` shows "Inf (measure_set M f s) = f s" ``` hoelzl@41981 ` 534` ``` unfolding Inf_extreal_def ``` hoelzl@38656 ` 535` ```proof (safe intro!: Greatest_equality) ``` paulson@33271 ` 536` ``` fix z ``` paulson@33271 ` 537` ``` assume z: "z \ measure_set M f s" ``` hoelzl@38656 ` 538` ``` from this obtain A where ``` paulson@33271 ` 539` ``` A: "range A \ sets M" and disj: "disjoint_family A" ``` hoelzl@41981 ` 540` ``` and "s \ (\x. A x)" and si: "(\i. f (A i)) = z" ``` hoelzl@38656 ` 541` ``` by (auto simp add: measure_set_def comp_def) ``` paulson@33271 ` 542` ``` hence seq: "s = (\i. A i \ s)" by blast ``` paulson@33271 ` 543` ``` have inc: "increasing M f" ``` paulson@33271 ` 544` ``` by (metis additive_increasing ca countably_additive_additive posf) ``` hoelzl@41981 ` 545` ``` have sums: "(\i. f (A i \ s)) = f (\i. A i \ s)" ``` hoelzl@41981 ` 546` ``` proof (rule ca[unfolded countably_additive_def, rule_format]) ``` paulson@33271 ` 547` ``` show "range (\n. A n \ s) \ sets M" using A s ``` wenzelm@33536 ` 548` ``` by blast ``` paulson@33271 ` 549` ``` show "disjoint_family (\n. A n \ s)" using disj ``` hoelzl@35582 ` 550` ``` by (auto simp add: disjoint_family_on_def) ``` paulson@33271 ` 551` ``` show "(\i. A i \ s) \ sets M" using A s ``` wenzelm@33536 ` 552` ``` by (metis UN_extend_simps(4) s seq) ``` paulson@33271 ` 553` ``` qed ``` hoelzl@41981 ` 554` ``` hence "f s = (\i. f (A i \ s))" ``` huffman@37032 ` 555` ``` using seq [symmetric] by (simp add: sums_iff) ``` hoelzl@41981 ` 556` ``` also have "... \ (\i. f (A i))" ``` hoelzl@41981 ` 557` ``` proof (rule suminf_le_pos) ``` hoelzl@41981 ` 558` ``` fix n show "f (A n \ s) \ f (A n)" using A s ``` hoelzl@38656 ` 559` ``` by (force intro: increasingD [OF inc]) ``` hoelzl@41981 ` 560` ``` fix N have "A N \ s \ sets M" using A s by auto ``` hoelzl@41981 ` 561` ``` then show "0 \ f (A N \ s)" using posf unfolding positive_def by auto ``` paulson@33271 ` 562` ``` qed ``` hoelzl@38656 ` 563` ``` also have "... = z" by (rule si) ``` paulson@33271 ` 564` ``` finally show "f s \ z" . ``` paulson@33271 ` 565` ```next ``` paulson@33271 ` 566` ``` fix y ``` hoelzl@38656 ` 567` ``` assume y: "\u \ measure_set M f s. y \ u" ``` paulson@33271 ` 568` ``` thus "y \ f s" ``` hoelzl@41689 ` 569` ``` by (blast intro: inf_measure_nonempty [of _ f, OF posf s subset_refl]) ``` paulson@33271 ` 570` ```qed ``` paulson@33271 ` 571` hoelzl@41981 ` 572` ```lemma measure_set_pos: ``` hoelzl@41981 ` 573` ``` assumes posf: "positive M f" "r \ measure_set M f X" ``` hoelzl@41981 ` 574` ``` shows "0 \ r" ``` hoelzl@41981 ` 575` ```proof - ``` hoelzl@41981 ` 576` ``` obtain A where "range A \ sets M" and r: "r = (\i. f (A i))" ``` hoelzl@41981 ` 577` ``` using `r \ measure_set M f X` unfolding measure_set_def by auto ``` hoelzl@41981 ` 578` ``` then show "0 \ r" using posf unfolding r positive_def ``` hoelzl@41981 ` 579` ``` by (intro suminf_0_le) auto ``` hoelzl@41981 ` 580` ```qed ``` hoelzl@41981 ` 581` hoelzl@41981 ` 582` ```lemma inf_measure_pos: ``` hoelzl@41981 ` 583` ``` assumes posf: "positive M f" ``` hoelzl@41981 ` 584` ``` shows "0 \ Inf (measure_set M f X)" ``` hoelzl@41981 ` 585` ```proof (rule complete_lattice_class.Inf_greatest) ``` hoelzl@41981 ` 586` ``` fix r assume "r \ measure_set M f X" with posf show "0 \ r" ``` hoelzl@41981 ` 587` ``` by (rule measure_set_pos) ``` hoelzl@41981 ` 588` ```qed ``` hoelzl@41981 ` 589` hoelzl@41689 ` 590` ```lemma inf_measure_empty: ``` hoelzl@41981 ` 591` ``` assumes posf: "positive M f" and "{} \ sets M" ``` paulson@33271 ` 592` ``` shows "Inf (measure_set M f {}) = 0" ``` paulson@33271 ` 593` ```proof (rule antisym) ``` paulson@33271 ` 594` ``` show "Inf (measure_set M f {}) \ 0" ``` hoelzl@41689 ` 595` ``` by (metis complete_lattice_class.Inf_lower `{} \ sets M` ``` hoelzl@41689 ` 596` ``` inf_measure_nonempty[OF posf] subset_refl posf[unfolded positive_def]) ``` hoelzl@41981 ` 597` ```qed (rule inf_measure_pos[OF posf]) ``` paulson@33271 ` 598` hoelzl@42066 ` 599` ```lemma (in ring_of_sets) inf_measure_positive: ``` hoelzl@41981 ` 600` ``` assumes p: "positive M f" and "{} \ sets M" ``` hoelzl@41981 ` 601` ``` shows "positive M (\x. Inf (measure_set M f x))" ``` hoelzl@41981 ` 602` ```proof (unfold positive_def, intro conjI ballI) ``` hoelzl@41981 ` 603` ``` show "Inf (measure_set M f {}) = 0" using inf_measure_empty[OF assms] by auto ``` hoelzl@41981 ` 604` ``` fix A assume "A \ sets M" ``` hoelzl@41981 ` 605` ```qed (rule inf_measure_pos[OF p]) ``` paulson@33271 ` 606` hoelzl@42066 ` 607` ```lemma (in ring_of_sets) inf_measure_increasing: ``` hoelzl@41689 ` 608` ``` assumes posf: "positive M f" ``` hoelzl@41689 ` 609` ``` shows "increasing \ space = space M, sets = Pow (space M) \ ``` paulson@33271 ` 610` ``` (\x. Inf (measure_set M f x))" ``` hoelzl@38656 ` 611` ```apply (auto simp add: increasing_def) ``` hoelzl@38656 ` 612` ```apply (rule complete_lattice_class.Inf_greatest) ``` hoelzl@38656 ` 613` ```apply (rule complete_lattice_class.Inf_lower) ``` huffman@37032 ` 614` ```apply (clarsimp simp add: measure_set_def, rule_tac x=A in exI, blast) ``` paulson@33271 ` 615` ```done ``` paulson@33271 ` 616` hoelzl@42066 ` 617` ```lemma (in ring_of_sets) inf_measure_le: ``` hoelzl@41689 ` 618` ``` assumes posf: "positive M f" and inc: "increasing M f" ``` hoelzl@41981 ` 619` ``` and x: "x \ {r . \A. range A \ sets M \ s \ (\i. A i) \ (\i. f (A i)) = r}" ``` paulson@33271 ` 620` ``` shows "Inf (measure_set M f s) \ x" ``` paulson@33271 ` 621` ```proof - ``` hoelzl@38656 ` 622` ``` obtain A where A: "range A \ sets M" and ss: "s \ (\i. A i)" ``` hoelzl@41981 ` 623` ``` and xeq: "(\i. f (A i)) = x" ``` hoelzl@41981 ` 624` ``` using x by auto ``` paulson@33271 ` 625` ``` have dA: "range (disjointed A) \ sets M" ``` paulson@33271 ` 626` ``` by (metis A range_disjointed_sets) ``` hoelzl@41981 ` 627` ``` have "\n. f (disjointed A n) \ f (A n)" ``` hoelzl@38656 ` 628` ``` by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A comp_def) ``` hoelzl@41981 ` 629` ``` moreover have "\i. 0 \ f (disjointed A i)" ``` hoelzl@41981 ` 630` ``` using posf dA unfolding positive_def by auto ``` hoelzl@41981 ` 631` ``` ultimately have sda: "(\i. f (disjointed A i)) \ (\i. f (A i))" ``` hoelzl@41981 ` 632` ``` by (blast intro!: suminf_le_pos) ``` hoelzl@41981 ` 633` ``` hence ley: "(\i. f (disjointed A i)) \ x" ``` hoelzl@38656 ` 634` ``` by (metis xeq) ``` hoelzl@41981 ` 635` ``` hence y: "(\i. f (disjointed A i)) \ measure_set M f s" ``` paulson@33271 ` 636` ``` apply (auto simp add: measure_set_def) ``` hoelzl@38656 ` 637` ``` apply (rule_tac x="disjointed A" in exI) ``` hoelzl@38656 ` 638` ``` apply (simp add: disjoint_family_disjointed UN_disjointed_eq ss dA comp_def) ``` paulson@33271 ` 639` ``` done ``` paulson@33271 ` 640` ``` show ?thesis ``` hoelzl@38656 ` 641` ``` by (blast intro: y order_trans [OF _ ley] posf complete_lattice_class.Inf_lower) ``` paulson@33271 ` 642` ```qed ``` paulson@33271 ` 643` hoelzl@42066 ` 644` ```lemma (in ring_of_sets) inf_measure_close: ``` hoelzl@41981 ` 645` ``` fixes e :: extreal ``` hoelzl@42066 ` 646` ``` assumes posf: "positive M f" and e: "0 < e" and ss: "s \ (space M)" and "Inf (measure_set M f s) \ \" ``` hoelzl@38656 ` 647` ``` shows "\A. range A \ sets M \ disjoint_family A \ s \ (\i. A i) \ ``` hoelzl@41981 ` 648` ``` (\i. f (A i)) \ Inf (measure_set M f s) + e" ``` hoelzl@42066 ` 649` ```proof - ``` hoelzl@42066 ` 650` ``` from `Inf (measure_set M f s) \ \` have fin: "\Inf (measure_set M f s)\ \ \" ``` hoelzl@41981 ` 651` ``` using inf_measure_pos[OF posf, of s] by auto ``` hoelzl@38656 ` 652` ``` obtain l where "l \ measure_set M f s" "l \ Inf (measure_set M f s) + e" ``` hoelzl@41981 ` 653` ``` using Inf_extreal_close[OF fin e] by auto ``` hoelzl@38656 ` 654` ``` thus ?thesis ``` hoelzl@38656 ` 655` ``` by (auto intro!: exI[of _ l] simp: measure_set_def comp_def) ``` paulson@33271 ` 656` ```qed ``` paulson@33271 ` 657` hoelzl@42066 ` 658` ```lemma (in ring_of_sets) inf_measure_countably_subadditive: ``` hoelzl@41689 ` 659` ``` assumes posf: "positive M f" and inc: "increasing M f" ``` paulson@33271 ` 660` ``` shows "countably_subadditive (| space = space M, sets = Pow (space M) |) ``` paulson@33271 ` 661` ``` (\x. Inf (measure_set M f x))" ``` hoelzl@42066 ` 662` ```proof (simp add: countably_subadditive_def, safe) ``` hoelzl@42066 ` 663` ``` fix A :: "nat \ 'a set" ``` hoelzl@42066 ` 664` ``` let "?outer B" = "Inf (measure_set M f B)" ``` hoelzl@38656 ` 665` ``` assume A: "range A \ Pow (space M)" ``` hoelzl@38656 ` 666` ``` and disj: "disjoint_family A" ``` hoelzl@38656 ` 667` ``` and sb: "(\i. A i) \ space M" ``` hoelzl@42066 ` 668` hoelzl@42066 ` 669` ``` { fix e :: extreal assume e: "0 < e" and "\i. ?outer (A i) \ \" ``` hoelzl@42066 ` 670` ``` hence "\BB. \n. range (BB n) \ sets M \ disjoint_family (BB n) \ ``` hoelzl@42066 ` 671` ``` A n \ (\i. BB n i) \ (\i. f (BB n i)) \ ?outer (A n) + e * (1/2)^(Suc n)" ``` hoelzl@42066 ` 672` ``` apply (safe intro!: choice inf_measure_close [of f, OF posf]) ``` hoelzl@42066 ` 673` ``` using e sb by (auto simp: extreal_zero_less_0_iff one_extreal_def) ``` hoelzl@42066 ` 674` ``` then obtain BB ``` hoelzl@42066 ` 675` ``` where BB: "\n. (range (BB n) \ sets M)" ``` hoelzl@38656 ` 676` ``` and disjBB: "\n. disjoint_family (BB n)" ``` hoelzl@38656 ` 677` ``` and sbBB: "\n. A n \ (\i. BB n i)" ``` hoelzl@42066 ` 678` ``` and BBle: "\n. (\i. f (BB n i)) \ ?outer (A n) + e * (1/2)^(Suc n)" ``` hoelzl@42066 ` 679` ``` by auto blast ``` hoelzl@42066 ` 680` ``` have sll: "(\n. \i. (f (BB n i))) \ (\n. ?outer (A n)) + e" ``` hoelzl@38656 ` 681` ``` proof - ``` hoelzl@41981 ` 682` ``` have sum_eq_1: "(\n. e*(1/2) ^ Suc n) = e" ``` hoelzl@41981 ` 683` ``` using suminf_half_series_extreal e ``` hoelzl@41981 ` 684` ``` by (simp add: extreal_zero_le_0_iff zero_le_divide_extreal suminf_cmult_extreal) ``` hoelzl@41981 ` 685` ``` have "\n i. 0 \ f (BB n i)" using posf[unfolded positive_def] BB by auto ``` hoelzl@41981 ` 686` ``` then have "\n. 0 \ (\i. f (BB n i))" by (rule suminf_0_le) ``` hoelzl@42066 ` 687` ``` then have "(\n. \i. (f (BB n i))) \ (\n. ?outer (A n) + e*(1/2) ^ Suc n)" ``` hoelzl@41981 ` 688` ``` by (rule suminf_le_pos[OF BBle]) ``` hoelzl@42066 ` 689` ``` also have "... = (\n. ?outer (A n)) + e" ``` hoelzl@41981 ` 690` ``` using sum_eq_1 inf_measure_pos[OF posf] e ``` hoelzl@41981 ` 691` ``` by (subst suminf_add_extreal) (auto simp add: extreal_zero_le_0_iff) ``` hoelzl@38656 ` 692` ``` finally show ?thesis . ``` hoelzl@38656 ` 693` ``` qed ``` hoelzl@42066 ` 694` ``` def C \ "(split BB) o prod_decode" ``` hoelzl@42066 ` 695` ``` have C: "!!n. C n \ sets M" ``` hoelzl@42066 ` 696` ``` apply (rule_tac p="prod_decode n" in PairE) ``` hoelzl@42066 ` 697` ``` apply (simp add: C_def) ``` hoelzl@42066 ` 698` ``` apply (metis BB subsetD rangeI) ``` hoelzl@42066 ` 699` ``` done ``` hoelzl@42066 ` 700` ``` have sbC: "(\i. A i) \ (\i. C i)" ``` hoelzl@38656 ` 701` ``` proof (auto simp add: C_def) ``` hoelzl@38656 ` 702` ``` fix x i ``` hoelzl@38656 ` 703` ``` assume x: "x \ A i" ``` hoelzl@38656 ` 704` ``` with sbBB [of i] obtain j where "x \ BB i j" ``` hoelzl@38656 ` 705` ``` by blast ``` hoelzl@38656 ` 706` ``` thus "\i. x \ split BB (prod_decode i)" ``` hoelzl@38656 ` 707` ``` by (metis prod_encode_inverse prod.cases) ``` hoelzl@38656 ` 708` ``` qed ``` hoelzl@42066 ` 709` ``` have "(f \ C) = (f \ (\(x, y). BB x y)) \ prod_decode" ``` hoelzl@42066 ` 710` ``` by (rule ext) (auto simp add: C_def) ``` hoelzl@42066 ` 711` ``` moreover have "suminf ... = (\n. \i. f (BB n i))" using BBle ``` hoelzl@42066 ` 712` ``` using BB posf[unfolded positive_def] ``` hoelzl@42066 ` 713` ``` by (force intro!: suminf_extreal_2dimen simp: o_def) ``` hoelzl@42066 ` 714` ``` ultimately have Csums: "(\i. f (C i)) = (\n. \i. f (BB n i))" by (simp add: o_def) ``` hoelzl@42066 ` 715` ``` have "?outer (\i. A i) \ (\n. \i. f (BB n i))" ``` hoelzl@42066 ` 716` ``` apply (rule inf_measure_le [OF posf(1) inc], auto) ``` hoelzl@42066 ` 717` ``` apply (rule_tac x="C" in exI) ``` hoelzl@42066 ` 718` ``` apply (auto simp add: C sbC Csums) ``` hoelzl@42066 ` 719` ``` done ``` hoelzl@42066 ` 720` ``` also have "... \ (\n. ?outer (A n)) + e" using sll ``` hoelzl@42066 ` 721` ``` by blast ``` hoelzl@42066 ` 722` ``` finally have "?outer (\i. A i) \ (\n. ?outer (A n)) + e" . } ``` hoelzl@42066 ` 723` ``` note for_finite_Inf = this ``` hoelzl@42066 ` 724` hoelzl@42066 ` 725` ``` show "?outer (\i. A i) \ (\n. ?outer (A n))" ``` hoelzl@42066 ` 726` ``` proof cases ``` hoelzl@42066 ` 727` ``` assume "\i. ?outer (A i) \ \" ``` hoelzl@42066 ` 728` ``` with for_finite_Inf show ?thesis ``` hoelzl@42066 ` 729` ``` by (intro extreal_le_epsilon) auto ``` hoelzl@42066 ` 730` ``` next ``` hoelzl@42066 ` 731` ``` assume "\ (\i. ?outer (A i) \ \)" ``` hoelzl@42066 ` 732` ``` then have "\i. ?outer (A i) = \" ``` hoelzl@42066 ` 733` ``` by auto ``` hoelzl@42066 ` 734` ``` then have "(\n. ?outer (A n)) = \" ``` hoelzl@42066 ` 735` ``` using suminf_PInfty[OF inf_measure_pos, OF posf] ``` hoelzl@42066 ` 736` ``` by metis ``` hoelzl@42066 ` 737` ``` then show ?thesis by simp ``` hoelzl@42066 ` 738` ``` qed ``` paulson@33271 ` 739` ```qed ``` paulson@33271 ` 740` hoelzl@42066 ` 741` ```lemma (in ring_of_sets) inf_measure_outer: ``` hoelzl@41689 ` 742` ``` "\ positive M f ; increasing M f \ ``` hoelzl@41689 ` 743` ``` \ outer_measure_space \ space = space M, sets = Pow (space M) \ ``` paulson@33271 ` 744` ``` (\x. Inf (measure_set M f x))" ``` hoelzl@41981 ` 745` ``` using inf_measure_pos[of M f] ``` hoelzl@38656 ` 746` ``` by (simp add: outer_measure_space_def inf_measure_empty ``` hoelzl@38656 ` 747` ``` inf_measure_increasing inf_measure_countably_subadditive positive_def) ``` paulson@33271 ` 748` hoelzl@42066 ` 749` ```lemma (in ring_of_sets) algebra_subset_lambda_system: ``` hoelzl@41689 ` 750` ``` assumes posf: "positive M f" and inc: "increasing M f" ``` paulson@33271 ` 751` ``` and add: "additive M f" ``` hoelzl@42066 ` 752` ``` shows "sets M \ lambda_system \ space = space M, sets = Pow (space M) \ ``` paulson@33271 ` 753` ``` (\x. Inf (measure_set M f x))" ``` hoelzl@38656 ` 754` ```proof (auto dest: sets_into_space ``` hoelzl@38656 ` 755` ``` simp add: algebra.lambda_system_eq [OF algebra_Pow]) ``` paulson@33271 ` 756` ``` fix x s ``` paulson@33271 ` 757` ``` assume x: "x \ sets M" ``` paulson@33271 ` 758` ``` and s: "s \ space M" ``` hoelzl@38656 ` 759` ``` have [simp]: "!!x. x \ sets M \ s \ (space M - x) = s-x" using s ``` paulson@33271 ` 760` ``` by blast ``` paulson@33271 ` 761` ``` have "Inf (measure_set M f (s\x)) + Inf (measure_set M f (s-x)) ``` paulson@33271 ` 762` ``` \ Inf (measure_set M f s)" ``` hoelzl@42066 ` 763` ``` proof cases ``` hoelzl@42066 ` 764` ``` assume "Inf (measure_set M f s) = \" then show ?thesis by simp ``` hoelzl@42066 ` 765` ``` next ``` hoelzl@42066 ` 766` ``` assume fin: "Inf (measure_set M f s) \ \" ``` hoelzl@42066 ` 767` ``` then have "measure_set M f s \ {}" ``` hoelzl@42066 ` 768` ``` by (auto simp: top_extreal_def) ``` hoelzl@42066 ` 769` ``` show ?thesis ``` hoelzl@42066 ` 770` ``` proof (rule complete_lattice_class.Inf_greatest) ``` hoelzl@42066 ` 771` ``` fix r assume "r \ measure_set M f s" ``` hoelzl@42066 ` 772` ``` then obtain A where A: "disjoint_family A" "range A \ sets M" "s \ (\i. A i)" ``` hoelzl@42066 ` 773` ``` and r: "r = (\i. f (A i))" unfolding measure_set_def by auto ``` hoelzl@42066 ` 774` ``` have "Inf (measure_set M f (s \ x)) \ (\i. f (A i \ x))" ``` hoelzl@42066 ` 775` ``` unfolding measure_set_def ``` hoelzl@42066 ` 776` ``` proof (safe intro!: complete_lattice_class.Inf_lower exI[of _ "\i. A i \ x"]) ``` hoelzl@42066 ` 777` ``` from A(1) show "disjoint_family (\i. A i \ x)" ``` hoelzl@42066 ` 778` ``` by (rule disjoint_family_on_bisimulation) auto ``` hoelzl@42066 ` 779` ``` qed (insert x A, auto) ``` hoelzl@42066 ` 780` ``` moreover ``` hoelzl@42066 ` 781` ``` have "Inf (measure_set M f (s - x)) \ (\i. f (A i - x))" ``` hoelzl@42066 ` 782` ``` unfolding measure_set_def ``` hoelzl@42066 ` 783` ``` proof (safe intro!: complete_lattice_class.Inf_lower exI[of _ "\i. A i - x"]) ``` hoelzl@42066 ` 784` ``` from A(1) show "disjoint_family (\i. A i - x)" ``` hoelzl@42066 ` 785` ``` by (rule disjoint_family_on_bisimulation) auto ``` hoelzl@42066 ` 786` ``` qed (insert x A, auto) ``` hoelzl@42066 ` 787` ``` ultimately have "Inf (measure_set M f (s \ x)) + Inf (measure_set M f (s - x)) \ ``` hoelzl@42066 ` 788` ``` (\i. f (A i \ x)) + (\i. f (A i - x))" by (rule add_mono) ``` hoelzl@42066 ` 789` ``` also have "\ = (\i. f (A i \ x) + f (A i - x))" ``` hoelzl@42066 ` 790` ``` using A(2) x posf by (subst suminf_add_extreal) (auto simp: positive_def) ``` hoelzl@42066 ` 791` ``` also have "\ = (\i. f (A i))" ``` hoelzl@42066 ` 792` ``` using A x ``` hoelzl@42066 ` 793` ``` by (subst add[THEN additiveD, symmetric]) ``` hoelzl@42066 ` 794` ``` (auto intro!: arg_cong[where f=suminf] arg_cong[where f=f]) ``` hoelzl@42066 ` 795` ``` finally show "Inf (measure_set M f (s \ x)) + Inf (measure_set M f (s - x)) \ r" ``` hoelzl@42066 ` 796` ``` using r by simp ``` paulson@33271 ` 797` ``` qed ``` hoelzl@42066 ` 798` ``` qed ``` hoelzl@38656 ` 799` ``` moreover ``` paulson@33271 ` 800` ``` have "Inf (measure_set M f s) ``` paulson@33271 ` 801` ``` \ Inf (measure_set M f (s\x)) + Inf (measure_set M f (s-x))" ``` hoelzl@42145 ` 802` ``` proof - ``` paulson@33271 ` 803` ``` have "Inf (measure_set M f s) = Inf (measure_set M f ((s\x) \ (s-x)))" ``` paulson@33271 ` 804` ``` by (metis Un_Diff_Int Un_commute) ``` hoelzl@38656 ` 805` ``` also have "... \ Inf (measure_set M f (s\x)) + Inf (measure_set M f (s-x))" ``` hoelzl@38656 ` 806` ``` apply (rule subadditiveD) ``` hoelzl@42145 ` 807` ``` apply (rule ring_of_sets.countably_subadditive_subadditive [OF ring_of_sets_Pow]) ``` hoelzl@41981 ` 808` ``` apply (simp add: positive_def inf_measure_empty[OF posf] inf_measure_pos[OF posf]) ``` hoelzl@41689 ` 809` ``` apply (rule inf_measure_countably_subadditive) ``` hoelzl@41689 ` 810` ``` using s by (auto intro!: posf inc) ``` paulson@33271 ` 811` ``` finally show ?thesis . ``` hoelzl@42145 ` 812` ``` qed ``` hoelzl@38656 ` 813` ``` ultimately ``` paulson@33271 ` 814` ``` show "Inf (measure_set M f (s\x)) + Inf (measure_set M f (s-x)) ``` paulson@33271 ` 815` ``` = Inf (measure_set M f s)" ``` paulson@33271 ` 816` ``` by (rule order_antisym) ``` paulson@33271 ` 817` ```qed ``` paulson@33271 ` 818` paulson@33271 ` 819` ```lemma measure_down: ``` hoelzl@41689 ` 820` ``` "measure_space N \ sigma_algebra M \ sets M \ sets N \ measure N = measure M \ measure_space M" ``` hoelzl@38656 ` 821` ``` by (simp add: measure_space_def measure_space_axioms_def positive_def ``` hoelzl@38656 ` 822` ``` countably_additive_def) ``` paulson@33271 ` 823` ``` blast ``` paulson@33271 ` 824` hoelzl@42066 ` 825` ```theorem (in ring_of_sets) caratheodory: ``` hoelzl@41689 ` 826` ``` assumes posf: "positive M f" and ca: "countably_additive M f" ``` hoelzl@41981 ` 827` ``` shows "\\ :: 'a set \ extreal. (\s \ sets M. \ s = f s) \ ``` hoelzl@41689 ` 828` ``` measure_space \ space = space M, sets = sets (sigma M), measure = \ \" ``` hoelzl@41689 ` 829` ```proof - ``` hoelzl@41689 ` 830` ``` have inc: "increasing M f" ``` hoelzl@41689 ` 831` ``` by (metis additive_increasing ca countably_additive_additive posf) ``` hoelzl@41689 ` 832` ``` let ?infm = "(\x. Inf (measure_set M f x))" ``` hoelzl@41689 ` 833` ``` def ls \ "lambda_system (|space = space M, sets = Pow (space M)|) ?infm" ``` hoelzl@41689 ` 834` ``` have mls: "measure_space \space = space M, sets = ls, measure = ?infm\" ``` hoelzl@41689 ` 835` ``` using sigma_algebra.caratheodory_lemma ``` hoelzl@41689 ` 836` ``` [OF sigma_algebra_Pow inf_measure_outer [OF posf inc]] ``` hoelzl@41689 ` 837` ``` by (simp add: ls_def) ``` hoelzl@41689 ` 838` ``` hence sls: "sigma_algebra (|space = space M, sets = ls, measure = ?infm|)" ``` hoelzl@41689 ` 839` ``` by (simp add: measure_space_def) ``` hoelzl@41689 ` 840` ``` have "sets M \ ls" ``` hoelzl@41689 ` 841` ``` by (simp add: ls_def) ``` hoelzl@41689 ` 842` ``` (metis ca posf inc countably_additive_additive algebra_subset_lambda_system) ``` hoelzl@41689 ` 843` ``` hence sgs_sb: "sigma_sets (space M) (sets M) \ ls" ``` hoelzl@41689 ` 844` ``` using sigma_algebra.sigma_sets_subset [OF sls, of "sets M"] ``` hoelzl@41689 ` 845` ``` by simp ``` hoelzl@41689 ` 846` ``` have "measure_space \ space = space M, sets = sets (sigma M), measure = ?infm \" ``` hoelzl@41689 ` 847` ``` unfolding sigma_def ``` hoelzl@41689 ` 848` ``` by (rule measure_down [OF mls], rule sigma_algebra_sigma_sets) ``` hoelzl@41689 ` 849` ``` (simp_all add: sgs_sb space_closed) ``` hoelzl@41689 ` 850` ``` thus ?thesis using inf_measure_agrees [OF posf ca] ``` hoelzl@41689 ` 851` ``` by (intro exI[of _ ?infm]) auto ``` hoelzl@41689 ` 852` ```qed ``` paulson@33271 ` 853` hoelzl@42145 ` 854` ```subsubsection {*Alternative instances of caratheodory*} ``` hoelzl@42145 ` 855` hoelzl@42145 ` 856` ```lemma sums_def2: ``` hoelzl@42145 ` 857` ``` "f sums x \ (\n. (\i\n. f i)) ----> x" ``` hoelzl@42145 ` 858` ``` unfolding sums_def ``` hoelzl@42145 ` 859` ``` apply (subst LIMSEQ_Suc_iff[symmetric]) ``` hoelzl@42145 ` 860` ``` unfolding atLeastLessThanSuc_atLeastAtMost atLeast0AtMost .. ``` hoelzl@42145 ` 861` hoelzl@42145 ` 862` ```lemma (in ring_of_sets) countably_additive_iff_continuous_from_below: ``` hoelzl@42145 ` 863` ``` assumes f: "positive M f" "additive M f" ``` hoelzl@42145 ` 864` ``` shows "countably_additive M f \ ``` hoelzl@42145 ` 865` ``` (\A. range A \ sets M \ incseq A \ (\i. A i) \ sets M \ (\i. f (A i)) ----> f (\i. A i))" ``` hoelzl@42145 ` 866` ``` unfolding countably_additive_def ``` hoelzl@42145 ` 867` ```proof safe ``` hoelzl@42145 ` 868` ``` assume count_sum: "\A. range A \ sets M \ disjoint_family A \ UNION UNIV A \ sets M \ (\i. f (A i)) = f (UNION UNIV A)" ``` hoelzl@42145 ` 869` ``` fix A :: "nat \ 'a set" assume A: "range A \ sets M" "incseq A" "(\i. A i) \ sets M" ``` hoelzl@42145 ` 870` ``` then have dA: "range (disjointed A) \ sets M" by (auto simp: range_disjointed_sets) ``` hoelzl@42145 ` 871` ``` with count_sum[THEN spec, of "disjointed A"] A(3) ``` hoelzl@42145 ` 872` ``` have f_UN: "(\i. f (disjointed A i)) = f (\i. A i)" ``` hoelzl@42145 ` 873` ``` by (auto simp: UN_disjointed_eq disjoint_family_disjointed) ``` hoelzl@42145 ` 874` ``` moreover have "(\n. (\i=0.. (\i. f (disjointed A i))" ``` hoelzl@42145 ` 875` ``` using f(1)[unfolded positive_def] dA ``` hoelzl@42145 ` 876` ``` by (auto intro!: summable_sumr_LIMSEQ_suminf summable_extreal_pos) ``` hoelzl@42145 ` 877` ``` from LIMSEQ_Suc[OF this] ``` hoelzl@42145 ` 878` ``` have "(\n. (\i\n. f (disjointed A i))) ----> (\i. f (disjointed A i))" ``` hoelzl@42145 ` 879` ``` unfolding atLeastLessThanSuc_atLeastAtMost atLeast0AtMost . ``` hoelzl@42145 ` 880` ``` moreover have "\n. (\i\n. f (disjointed A i)) = f (A n)" ``` hoelzl@42145 ` 881` ``` using disjointed_additive[OF f A(1,2)] . ``` hoelzl@42145 ` 882` ``` ultimately show "(\i. f (A i)) ----> f (\i. A i)" by simp ``` hoelzl@42145 ` 883` ```next ``` hoelzl@42145 ` 884` ``` assume cont: "\A. range A \ sets M \ incseq A \ (\i. A i) \ sets M \ (\i. f (A i)) ----> f (\i. A i)" ``` hoelzl@42145 ` 885` ``` fix A :: "nat \ 'a set" assume A: "range A \ sets M" "disjoint_family A" "(\i. A i) \ sets M" ``` hoelzl@42145 ` 886` ``` have *: "(\n. (\i\n. A i)) = (\i. A i)" by auto ``` hoelzl@42145 ` 887` ``` have "(\n. f (\i\n. A i)) ----> f (\i. A i)" ``` hoelzl@42145 ` 888` ``` proof (unfold *[symmetric], intro cont[rule_format]) ``` hoelzl@42145 ` 889` ``` show "range (\i. \ i\i. A i) \ sets M" "(\i. \ i\i. A i) \ sets M" ``` hoelzl@42145 ` 890` ``` using A * by auto ``` hoelzl@42145 ` 891` ``` qed (force intro!: incseq_SucI) ``` hoelzl@42145 ` 892` ``` moreover have "\n. f (\i\n. A i) = (\i\n. f (A i))" ``` hoelzl@42145 ` 893` ``` using A ``` hoelzl@42145 ` 894` ``` by (intro additive_sum[OF f, of _ A, symmetric]) ``` hoelzl@42145 ` 895` ``` (auto intro: disjoint_family_on_mono[where B=UNIV]) ``` hoelzl@42145 ` 896` ``` ultimately ``` hoelzl@42145 ` 897` ``` have "(\i. f (A i)) sums f (\i. A i)" ``` hoelzl@42145 ` 898` ``` unfolding sums_def2 by simp ``` hoelzl@42145 ` 899` ``` from sums_unique[OF this] ``` hoelzl@42145 ` 900` ``` show "(\i. f (A i)) = f (\i. A i)" by simp ``` hoelzl@42145 ` 901` ```qed ``` hoelzl@42145 ` 902` hoelzl@42145 ` 903` ```lemma uminus_extreal_add_uminus_uminus: ``` hoelzl@42145 ` 904` ``` fixes a b :: extreal shows "a \ \ \ b \ \ \ - (- a + - b) = a + b" ``` hoelzl@42145 ` 905` ``` by (cases rule: extreal2_cases[of a b]) auto ``` hoelzl@42145 ` 906` hoelzl@42145 ` 907` ```lemma INFI_extreal_add: ``` hoelzl@42145 ` 908` ``` assumes "decseq f" "decseq g" and fin: "\i. f i \ \" "\i. g i \ \" ``` hoelzl@42145 ` 909` ``` shows "(INF i. f i + g i) = INFI UNIV f + INFI UNIV g" ``` hoelzl@42145 ` 910` ```proof - ``` hoelzl@42145 ` 911` ``` have INF_less: "(INF i. f i) < \" "(INF i. g i) < \" ``` hoelzl@42145 ` 912` ``` using assms unfolding INF_less_iff by auto ``` hoelzl@42145 ` 913` ``` { fix i from fin[of i] have "- ((- f i) + (- g i)) = f i + g i" ``` hoelzl@42145 ` 914` ``` by (rule uminus_extreal_add_uminus_uminus) } ``` hoelzl@42145 ` 915` ``` then have "(INF i. f i + g i) = (INF i. - ((- f i) + (- g i)))" ``` hoelzl@42145 ` 916` ``` by simp ``` hoelzl@42145 ` 917` ``` also have "\ = INFI UNIV f + INFI UNIV g" ``` hoelzl@42145 ` 918` ``` unfolding extreal_INFI_uminus ``` hoelzl@42145 ` 919` ``` using assms INF_less ``` hoelzl@42145 ` 920` ``` by (subst SUPR_extreal_add) ``` hoelzl@42145 ` 921` ``` (auto simp: extreal_SUPR_uminus intro!: uminus_extreal_add_uminus_uminus) ``` hoelzl@42145 ` 922` ``` finally show ?thesis . ``` hoelzl@42145 ` 923` ```qed ``` hoelzl@42145 ` 924` hoelzl@42145 ` 925` ```lemma (in ring_of_sets) continuous_from_above_iff_empty_continuous: ``` hoelzl@42145 ` 926` ``` assumes f: "positive M f" "additive M f" ``` hoelzl@42145 ` 927` ``` shows "(\A. range A \ sets M \ decseq A \ (\i. A i) \ sets M \ (\i. f (A i) \ \) \ (\i. f (A i)) ----> f (\i. A i)) ``` hoelzl@42145 ` 928` ``` \ (\A. range A \ sets M \ decseq A \ (\i. A i) = {} \ (\i. f (A i) \ \) \ (\i. f (A i)) ----> 0)" ``` hoelzl@42145 ` 929` ```proof safe ``` hoelzl@42145 ` 930` ``` assume cont: "(\A. range A \ sets M \ decseq A \ (\i. A i) \ sets M \ (\i. f (A i) \ \) \ (\i. f (A i)) ----> f (\i. A i))" ``` hoelzl@42145 ` 931` ``` fix A :: "nat \ 'a set" assume A: "range A \ sets M" "decseq A" "(\i. A i) = {}" "\i. f (A i) \ \" ``` hoelzl@42145 ` 932` ``` with cont[THEN spec, of A] show "(\i. f (A i)) ----> 0" ``` hoelzl@42145 ` 933` ``` using `positive M f`[unfolded positive_def] by auto ``` hoelzl@42145 ` 934` ```next ``` hoelzl@42145 ` 935` ``` assume cont: "\A. range A \ sets M \ decseq A \ (\i. A i) = {} \ (\i. f (A i) \ \) \ (\i. f (A i)) ----> 0" ``` hoelzl@42145 ` 936` ``` fix A :: "nat \ 'a set" assume A: "range A \ sets M" "decseq A" "(\i. A i) \ sets M" "\i. f (A i) \ \" ``` hoelzl@42145 ` 937` hoelzl@42145 ` 938` ``` have f_mono: "\a b. a \ sets M \ b \ sets M \ a \ b \ f a \ f b" ``` hoelzl@42145 ` 939` ``` using additive_increasing[OF f] unfolding increasing_def by simp ``` hoelzl@42145 ` 940` hoelzl@42145 ` 941` ``` have decseq_fA: "decseq (\i. f (A i))" ``` hoelzl@42145 ` 942` ``` using A by (auto simp: decseq_def intro!: f_mono) ``` hoelzl@42145 ` 943` ``` have decseq: "decseq (\i. A i - (\i. A i))" ``` hoelzl@42145 ` 944` ``` using A by (auto simp: decseq_def) ``` hoelzl@42145 ` 945` ``` then have decseq_f: "decseq (\i. f (A i - (\i. A i)))" ``` hoelzl@42145 ` 946` ``` using A unfolding decseq_def by (auto intro!: f_mono Diff) ``` hoelzl@42145 ` 947` ``` have "f (\x. A x) \ f (A 0)" ``` hoelzl@42145 ` 948` ``` using A by (auto intro!: f_mono) ``` hoelzl@42145 ` 949` ``` then have f_Int_fin: "f (\x. A x) \ \" ``` hoelzl@42145 ` 950` ``` using A by auto ``` hoelzl@42145 ` 951` ``` { fix i ``` hoelzl@42145 ` 952` ``` have "f (A i - (\i. A i)) \ f (A i)" using A by (auto intro!: f_mono) ``` hoelzl@42145 ` 953` ``` then have "f (A i - (\i. A i)) \ \" ``` hoelzl@42145 ` 954` ``` using A by auto } ``` hoelzl@42145 ` 955` ``` note f_fin = this ``` hoelzl@42145 ` 956` ``` have "(\i. f (A i - (\i. A i))) ----> 0" ``` hoelzl@42145 ` 957` ``` proof (intro cont[rule_format, OF _ decseq _ f_fin]) ``` hoelzl@42145 ` 958` ``` show "range (\i. A i - (\i. A i)) \ sets M" "(\i. A i - (\i. A i)) = {}" ``` hoelzl@42145 ` 959` ``` using A by auto ``` hoelzl@42145 ` 960` ``` qed ``` hoelzl@42145 ` 961` ``` from INF_Lim_extreal[OF decseq_f this] ``` hoelzl@42145 ` 962` ``` have "(INF n. f (A n - (\i. A i))) = 0" . ``` hoelzl@42145 ` 963` ``` moreover have "(INF n. f (\i. A i)) = f (\i. A i)" ``` hoelzl@42145 ` 964` ``` by auto ``` hoelzl@42145 ` 965` ``` ultimately have "(INF n. f (A n - (\i. A i)) + f (\i. A i)) = 0 + f (\i. A i)" ``` hoelzl@42145 ` 966` ``` using A(4) f_fin f_Int_fin ``` hoelzl@42145 ` 967` ``` by (subst INFI_extreal_add) (auto simp: decseq_f) ``` hoelzl@42145 ` 968` ``` moreover { ``` hoelzl@42145 ` 969` ``` fix n ``` hoelzl@42145 ` 970` ``` have "f (A n - (\i. A i)) + f (\i. A i) = f ((A n - (\i. A i)) \ (\i. A i))" ``` hoelzl@42145 ` 971` ``` using A by (subst f(2)[THEN additiveD]) auto ``` hoelzl@42145 ` 972` ``` also have "(A n - (\i. A i)) \ (\i. A i) = A n" ``` hoelzl@42145 ` 973` ``` by auto ``` hoelzl@42145 ` 974` ``` finally have "f (A n - (\i. A i)) + f (\i. A i) = f (A n)" . } ``` hoelzl@42145 ` 975` ``` ultimately have "(INF n. f (A n)) = f (\i. A i)" ``` hoelzl@42145 ` 976` ``` by simp ``` hoelzl@42145 ` 977` ``` with LIMSEQ_extreal_INFI[OF decseq_fA] ``` hoelzl@42145 ` 978` ``` show "(\i. f (A i)) ----> f (\i. A i)" by simp ``` hoelzl@42145 ` 979` ```qed ``` hoelzl@42145 ` 980` hoelzl@42145 ` 981` ```lemma positiveD1: "positive M f \ f {} = 0" by (auto simp: positive_def) ``` hoelzl@42145 ` 982` ```lemma positiveD2: "positive M f \ A \ sets M \ 0 \ f A" by (auto simp: positive_def) ``` hoelzl@42145 ` 983` hoelzl@42145 ` 984` ```lemma (in ring_of_sets) empty_continuous_imp_continuous_from_below: ``` hoelzl@42145 ` 985` ``` assumes f: "positive M f" "additive M f" "\A\sets M. f A \ \" ``` hoelzl@42145 ` 986` ``` assumes cont: "\A. range A \ sets M \ decseq A \ (\i. A i) = {} \ (\i. f (A i)) ----> 0" ``` hoelzl@42145 ` 987` ``` assumes A: "range A \ sets M" "incseq A" "(\i. A i) \ sets M" ``` hoelzl@42145 ` 988` ``` shows "(\i. f (A i)) ----> f (\i. A i)" ``` hoelzl@42145 ` 989` ```proof - ``` hoelzl@42145 ` 990` ``` have "\A\sets M. \x. f A = extreal x" ``` hoelzl@42145 ` 991` ``` proof ``` hoelzl@42145 ` 992` ``` fix A assume "A \ sets M" with f show "\x. f A = extreal x" ``` hoelzl@42145 ` 993` ``` unfolding positive_def by (cases "f A") auto ``` hoelzl@42145 ` 994` ``` qed ``` hoelzl@42145 ` 995` ``` from bchoice[OF this] guess f' .. note f' = this[rule_format] ``` hoelzl@42145 ` 996` ``` from A have "(\i. f ((\i. A i) - A i)) ----> 0" ``` hoelzl@42145 ` 997` ``` by (intro cont[rule_format]) (auto simp: decseq_def incseq_def) ``` hoelzl@42145 ` 998` ``` moreover ``` hoelzl@42145 ` 999` ``` { fix i ``` hoelzl@42145 ` 1000` ``` have "f ((\i. A i) - A i) + f (A i) = f ((\i. A i) - A i \ A i)" ``` hoelzl@42145 ` 1001` ``` using A by (intro f(2)[THEN additiveD, symmetric]) auto ``` hoelzl@42145 ` 1002` ``` also have "(\i. A i) - A i \ A i = (\i. A i)" ``` hoelzl@42145 ` 1003` ``` by auto ``` hoelzl@42145 ` 1004` ``` finally have "f' (\i. A i) - f' (A i) = f' ((\i. A i) - A i)" ``` hoelzl@42145 ` 1005` ``` using A by (subst (asm) (1 2 3) f') auto ``` hoelzl@42145 ` 1006` ``` then have "f ((\i. A i) - A i) = extreal (f' (\i. A i) - f' (A i))" ``` hoelzl@42145 ` 1007` ``` using A f' by auto } ``` hoelzl@42145 ` 1008` ``` ultimately have "(\i. f' (\i. A i) - f' (A i)) ----> 0" ``` hoelzl@42145 ` 1009` ``` by (simp add: zero_extreal_def) ``` hoelzl@42145 ` 1010` ``` then have "(\i. f' (A i)) ----> f' (\i. A i)" ``` hoelzl@42145 ` 1011` ``` by (rule LIMSEQ_diff_approach_zero2[OF LIMSEQ_const]) ``` hoelzl@42145 ` 1012` ``` then show "(\i. f (A i)) ----> f (\i. A i)" ``` hoelzl@42145 ` 1013` ``` using A by (subst (1 2) f') auto ``` hoelzl@42145 ` 1014` ```qed ``` hoelzl@42145 ` 1015` hoelzl@42145 ` 1016` ```lemma (in ring_of_sets) empty_continuous_imp_countably_additive: ``` hoelzl@42145 ` 1017` ``` assumes f: "positive M f" "additive M f" and fin: "\A\sets M. f A \ \" ``` hoelzl@42145 ` 1018` ``` assumes cont: "\A. range A \ sets M \ decseq A \ (\i. A i) = {} \ (\i. f (A i)) ----> 0" ``` hoelzl@42145 ` 1019` ``` shows "countably_additive M f" ``` hoelzl@42145 ` 1020` ``` using countably_additive_iff_continuous_from_below[OF f] ``` hoelzl@42145 ` 1021` ``` using empty_continuous_imp_continuous_from_below[OF f fin] cont ``` hoelzl@42145 ` 1022` ``` by blast ``` hoelzl@42145 ` 1023` hoelzl@42145 ` 1024` ```lemma (in ring_of_sets) caratheodory_empty_continuous: ``` hoelzl@42145 ` 1025` ``` assumes f: "positive M f" "additive M f" and fin: "\A. A \ sets M \ f A \ \" ``` hoelzl@42145 ` 1026` ``` assumes cont: "\A. range A \ sets M \ decseq A \ (\i. A i) = {} \ (\i. f (A i)) ----> 0" ``` hoelzl@42145 ` 1027` ``` shows "\\ :: 'a set \ extreal. (\s \ sets M. \ s = f s) \ ``` hoelzl@42145 ` 1028` ``` measure_space \ space = space M, sets = sets (sigma M), measure = \ \" ``` hoelzl@42145 ` 1029` ```proof (intro caratheodory empty_continuous_imp_countably_additive f) ``` hoelzl@42145 ` 1030` ``` show "\A\sets M. f A \ \" using fin by auto ``` hoelzl@42145 ` 1031` ```qed (rule cont) ``` hoelzl@42145 ` 1032` paulson@33271 ` 1033` ```end ```