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