src/HOL/Probability/Caratheodory.thy
 author huffman Wed Mar 10 15:57:01 2010 -0800 (2010-03-10) changeset 35704 5007843dae33 parent 35582 b16d99a72dc9 child 36649 bfd8c550faa6 permissions -rw-r--r--
convert HOL-Probability to use Nat_Bijection library
 paulson@33271 ` 1` ```header {*Caratheodory Extension Theorem*} ``` paulson@33271 ` 2` paulson@33271 ` 3` ```theory Caratheodory ``` paulson@33271 ` 4` ``` imports Sigma_Algebra SupInf SeriesPlus ``` paulson@33271 ` 5` ```begin ``` paulson@33271 ` 6` paulson@33271 ` 7` ```text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*} ``` paulson@33271 ` 8` paulson@33271 ` 9` ```subsection {* Measure Spaces *} ``` paulson@33271 ` 10` paulson@33271 ` 11` ```text {*A measure assigns a nonnegative real to every measurable set. ``` paulson@33271 ` 12` ``` It is countably additive for disjoint sets.*} ``` paulson@33271 ` 13` paulson@33271 ` 14` ```record 'a measure_space = "'a algebra" + ``` paulson@33271 ` 15` ``` measure:: "'a set \ real" ``` paulson@33271 ` 16` paulson@33271 ` 17` ```definition ``` hoelzl@35582 ` 18` ``` disjoint_family_on where ``` hoelzl@35582 ` 19` ``` "disjoint_family_on A S \ (\m\S. \n\S. m \ n \ A m \ A n = {})" ``` hoelzl@35582 ` 20` hoelzl@35582 ` 21` ```abbreviation ``` hoelzl@35582 ` 22` ``` "disjoint_family A \ disjoint_family_on A UNIV" ``` paulson@33271 ` 23` paulson@33271 ` 24` ```definition ``` paulson@33271 ` 25` ``` positive where ``` paulson@33271 ` 26` ``` "positive M f \ f {} = (0::real) & (\x \ sets M. 0 \ f x)" ``` paulson@33271 ` 27` paulson@33271 ` 28` ```definition ``` paulson@33271 ` 29` ``` additive where ``` paulson@33271 ` 30` ``` "additive M f \ ``` paulson@33271 ` 31` ``` (\x \ sets M. \y \ sets M. x \ y = {} ``` paulson@33271 ` 32` ``` \ f (x \ y) = f x + f y)" ``` paulson@33271 ` 33` paulson@33271 ` 34` ```definition ``` paulson@33271 ` 35` ``` countably_additive where ``` paulson@33271 ` 36` ``` "countably_additive M f \ ``` paulson@33271 ` 37` ``` (\A. range A \ sets M \ ``` paulson@33271 ` 38` ``` disjoint_family A \ ``` paulson@33271 ` 39` ``` (\i. A i) \ sets M \ ``` paulson@33271 ` 40` ``` (\n. f (A n)) sums f (\i. A i))" ``` paulson@33271 ` 41` paulson@33271 ` 42` ```definition ``` paulson@33271 ` 43` ``` increasing where ``` paulson@33271 ` 44` ``` "increasing M f \ (\x \ sets M. \y \ sets M. x \ y \ f x \ f y)" ``` paulson@33271 ` 45` paulson@33271 ` 46` ```definition ``` paulson@33271 ` 47` ``` subadditive where ``` paulson@33271 ` 48` ``` "subadditive M f \ ``` paulson@33271 ` 49` ``` (\x \ sets M. \y \ sets M. x \ y = {} ``` paulson@33271 ` 50` ``` \ f (x \ y) \ f x + f y)" ``` paulson@33271 ` 51` paulson@33271 ` 52` ```definition ``` paulson@33271 ` 53` ``` countably_subadditive where ``` paulson@33271 ` 54` ``` "countably_subadditive M f \ ``` paulson@33271 ` 55` ``` (\A. range A \ sets M \ ``` paulson@33271 ` 56` ``` disjoint_family A \ ``` paulson@33271 ` 57` ``` (\i. A i) \ sets M \ ``` paulson@33271 ` 58` ``` summable (f o A) \ ``` paulson@33271 ` 59` ``` f (\i. A i) \ suminf (\n. f (A n)))" ``` paulson@33271 ` 60` paulson@33271 ` 61` ```definition ``` paulson@33271 ` 62` ``` lambda_system where ``` paulson@33271 ` 63` ``` "lambda_system M f = ``` paulson@33271 ` 64` ``` {l. l \ sets M & (\x \ sets M. f (l \ x) + f ((space M - l) \ x) = f x)}" ``` paulson@33271 ` 65` paulson@33271 ` 66` ```definition ``` paulson@33271 ` 67` ``` outer_measure_space where ``` paulson@33271 ` 68` ``` "outer_measure_space M f \ ``` paulson@33271 ` 69` ``` positive M f & increasing M f & countably_subadditive M f" ``` paulson@33271 ` 70` paulson@33271 ` 71` ```definition ``` paulson@33271 ` 72` ``` measure_set where ``` paulson@33271 ` 73` ``` "measure_set M f X = ``` paulson@33271 ` 74` ``` {r . \A. range A \ sets M & disjoint_family A & X \ (\i. A i) & (f \ A) sums r}" ``` paulson@33271 ` 75` paulson@33271 ` 76` paulson@33271 ` 77` ```locale measure_space = sigma_algebra + ``` paulson@33271 ` 78` ``` assumes positive: "!!a. a \ sets M \ 0 \ measure M a" ``` paulson@33271 ` 79` ``` and empty_measure [simp]: "measure M {} = (0::real)" ``` paulson@33271 ` 80` ``` and ca: "countably_additive M (measure M)" ``` paulson@33271 ` 81` paulson@33271 ` 82` ```subsection {* Basic Lemmas *} ``` paulson@33271 ` 83` paulson@33271 ` 84` ```lemma positive_imp_0: "positive M f \ f {} = 0" ``` paulson@33271 ` 85` ``` by (simp add: positive_def) ``` paulson@33271 ` 86` paulson@33271 ` 87` ```lemma positive_imp_pos: "positive M f \ x \ sets M \ 0 \ f x" ``` paulson@33271 ` 88` ``` by (simp add: positive_def) ``` paulson@33271 ` 89` paulson@33271 ` 90` ```lemma increasingD: ``` paulson@33271 ` 91` ``` "increasing M f \ x \ y \ x\sets M \ y\sets M \ f x \ f y" ``` paulson@33271 ` 92` ``` by (auto simp add: increasing_def) ``` paulson@33271 ` 93` paulson@33271 ` 94` ```lemma subadditiveD: ``` paulson@33271 ` 95` ``` "subadditive M f \ x \ y = {} \ x\sets M \ y\sets M ``` paulson@33271 ` 96` ``` \ f (x \ y) \ f x + f y" ``` paulson@33271 ` 97` ``` by (auto simp add: subadditive_def) ``` paulson@33271 ` 98` paulson@33271 ` 99` ```lemma additiveD: ``` paulson@33271 ` 100` ``` "additive M f \ x \ y = {} \ x\sets M \ y\sets M ``` paulson@33271 ` 101` ``` \ f (x \ y) = f x + f y" ``` paulson@33271 ` 102` ``` by (auto simp add: additive_def) ``` paulson@33271 ` 103` paulson@33271 ` 104` ```lemma countably_additiveD: ``` hoelzl@35582 ` 105` ``` "countably_additive M f \ range A \ sets M \ disjoint_family A ``` paulson@33271 ` 106` ``` \ (\i. A i) \ sets M \ (\n. f (A n)) sums f (\i. A i)" ``` hoelzl@35582 ` 107` ``` by (simp add: countably_additive_def) ``` paulson@33271 ` 108` paulson@33271 ` 109` ```lemma Int_Diff_disjoint: "A \ B \ (A - B) = {}" ``` paulson@33271 ` 110` ``` by blast ``` paulson@33271 ` 111` paulson@33271 ` 112` ```lemma Int_Diff_Un: "A \ B \ (A - B) = A" ``` paulson@33271 ` 113` ``` by blast ``` paulson@33271 ` 114` paulson@33271 ` 115` ```lemma disjoint_family_subset: ``` paulson@33271 ` 116` ``` "disjoint_family A \ (!!x. B x \ A x) \ disjoint_family B" ``` hoelzl@35582 ` 117` ``` by (force simp add: disjoint_family_on_def) ``` paulson@33271 ` 118` paulson@33271 ` 119` ```subsection {* A Two-Element Series *} ``` paulson@33271 ` 120` paulson@33271 ` 121` ```definition binaryset :: "'a set \ 'a set \ nat \ 'a set " ``` paulson@33271 ` 122` ``` where "binaryset A B = (\\<^isup>x. {})(0 := A, Suc 0 := B)" ``` paulson@33271 ` 123` paulson@33271 ` 124` ```lemma range_binaryset_eq: "range(binaryset A B) = {A,B,{}}" ``` hoelzl@35582 ` 125` ``` apply (simp add: binaryset_def) ``` hoelzl@35582 ` 126` ``` apply (rule set_ext) ``` hoelzl@35582 ` 127` ``` apply (auto simp add: image_iff) ``` paulson@33271 ` 128` ``` done ``` paulson@33271 ` 129` paulson@33271 ` 130` ```lemma UN_binaryset_eq: "(\i. binaryset A B i) = A \ B" ``` hoelzl@35582 ` 131` ``` by (simp add: UNION_eq_Union_image range_binaryset_eq) ``` paulson@33271 ` 132` hoelzl@35582 ` 133` ```lemma LIMSEQ_binaryset: ``` paulson@33271 ` 134` ``` assumes f: "f {} = 0" ``` paulson@33271 ` 135` ``` shows "(\n. \i = 0.. f A + f B" ``` paulson@33271 ` 136` ```proof - ``` paulson@33271 ` 137` ``` have "(\n. \i = 0..< Suc (Suc n). f (binaryset A B i)) = (\n. f A + f B)" ``` hoelzl@35582 ` 138` ``` proof ``` paulson@33271 ` 139` ``` fix n ``` paulson@33271 ` 140` ``` show "(\i\nat = 0\nat.. f A + f B" by (rule LIMSEQ_const) ``` paulson@33271 ` 145` ``` ultimately ``` hoelzl@35582 ` 146` ``` have "(\n. \i = 0..< Suc (Suc n). f (binaryset A B i)) ----> f A + f B" ``` paulson@33271 ` 147` ``` by metis ``` paulson@33271 ` 148` ``` hence "(\n. \i = 0..< n+2. f (binaryset A B i)) ----> f A + f B" ``` paulson@33271 ` 149` ``` by simp ``` paulson@33271 ` 150` ``` thus ?thesis by (rule LIMSEQ_offset [where k=2]) ``` paulson@33271 ` 151` ```qed ``` paulson@33271 ` 152` paulson@33271 ` 153` ```lemma binaryset_sums: ``` paulson@33271 ` 154` ``` assumes f: "f {} = 0" ``` paulson@33271 ` 155` ``` shows "(\n. f (binaryset A B n)) sums (f A + f B)" ``` paulson@33271 ` 156` ``` by (simp add: sums_def LIMSEQ_binaryset [where f=f, OF f]) ``` paulson@33271 ` 157` paulson@33271 ` 158` ```lemma suminf_binaryset_eq: ``` paulson@33271 ` 159` ``` "f {} = 0 \ suminf (\n. f (binaryset A B n)) = f A + f B" ``` paulson@33271 ` 160` ``` by (metis binaryset_sums sums_unique) ``` paulson@33271 ` 161` paulson@33271 ` 162` paulson@33271 ` 163` ```subsection {* Lambda Systems *} ``` paulson@33271 ` 164` paulson@33271 ` 165` ```lemma (in algebra) lambda_system_eq: ``` paulson@33271 ` 166` ``` "lambda_system M f = ``` paulson@33271 ` 167` ``` {l. l \ sets M & (\x \ sets M. f (x \ l) + f (x - l) = f x)}" ``` paulson@33271 ` 168` ```proof - ``` paulson@33271 ` 169` ``` have [simp]: "!!l x. l \ sets M \ x \ sets M \ (space M - l) \ x = x - l" ``` paulson@33271 ` 170` ``` by (metis Diff_eq Int_Diff Int_absorb1 Int_commute sets_into_space) ``` paulson@33271 ` 171` ``` show ?thesis ``` paulson@33271 ` 172` ``` by (auto simp add: lambda_system_def) (metis Diff_Compl Int_commute)+ ``` paulson@33271 ` 173` ```qed ``` paulson@33271 ` 174` paulson@33271 ` 175` ```lemma (in algebra) lambda_system_empty: ``` paulson@33271 ` 176` ``` "positive M f \ {} \ lambda_system M f" ``` paulson@33271 ` 177` ``` by (auto simp add: positive_def lambda_system_eq) ``` paulson@33271 ` 178` paulson@33271 ` 179` ```lemma lambda_system_sets: ``` paulson@33271 ` 180` ``` "x \ lambda_system M f \ x \ sets M" ``` paulson@33271 ` 181` ``` by (simp add: lambda_system_def) ``` paulson@33271 ` 182` paulson@33271 ` 183` ```lemma (in algebra) lambda_system_Compl: ``` paulson@33271 ` 184` ``` fixes f:: "'a set \ real" ``` paulson@33271 ` 185` ``` assumes x: "x \ lambda_system M f" ``` paulson@33271 ` 186` ``` shows "space M - x \ lambda_system M f" ``` paulson@33271 ` 187` ``` proof - ``` paulson@33271 ` 188` ``` have "x \ space M" ``` paulson@33271 ` 189` ``` by (metis sets_into_space lambda_system_sets x) ``` paulson@33271 ` 190` ``` hence "space M - (space M - x) = x" ``` paulson@33271 ` 191` ``` by (metis double_diff equalityE) ``` paulson@33271 ` 192` ``` with x show ?thesis ``` paulson@33271 ` 193` ``` by (force simp add: lambda_system_def) ``` paulson@33271 ` 194` ``` qed ``` paulson@33271 ` 195` paulson@33271 ` 196` ```lemma (in algebra) lambda_system_Int: ``` paulson@33271 ` 197` ``` fixes f:: "'a set \ real" ``` paulson@33271 ` 198` ``` assumes xl: "x \ lambda_system M f" and yl: "y \ lambda_system M f" ``` paulson@33271 ` 199` ``` shows "x \ y \ lambda_system M f" ``` paulson@33271 ` 200` ``` proof - ``` paulson@33271 ` 201` ``` from xl yl show ?thesis ``` paulson@33271 ` 202` ``` proof (auto simp add: positive_def lambda_system_eq Int) ``` wenzelm@33536 ` 203` ``` fix u ``` wenzelm@33536 ` 204` ``` assume x: "x \ sets M" and y: "y \ sets M" and u: "u \ sets M" ``` paulson@33271 ` 205` ``` and fx: "\z\sets M. f (z \ x) + f (z - x) = f z" ``` paulson@33271 ` 206` ``` and fy: "\z\sets M. f (z \ y) + f (z - y) = f z" ``` wenzelm@33536 ` 207` ``` have "u - x \ y \ sets M" ``` wenzelm@33536 ` 208` ``` by (metis Diff Diff_Int Un u x y) ``` wenzelm@33536 ` 209` ``` moreover ``` wenzelm@33536 ` 210` ``` have "(u - (x \ y)) \ y = u \ y - x" by blast ``` wenzelm@33536 ` 211` ``` moreover ``` wenzelm@33536 ` 212` ``` have "u - x \ y - y = u - y" by blast ``` wenzelm@33536 ` 213` ``` ultimately ``` wenzelm@33536 ` 214` ``` have ey: "f (u - x \ y) = f (u \ y - x) + f (u - y)" using fy ``` wenzelm@33536 ` 215` ``` by force ``` wenzelm@33536 ` 216` ``` have "f (u \ (x \ y)) + f (u - x \ y) ``` paulson@33271 ` 217` ``` = (f (u \ (x \ y)) + f (u \ y - x)) + f (u - y)" ``` wenzelm@33536 ` 218` ``` by (simp add: ey) ``` wenzelm@33536 ` 219` ``` also have "... = (f ((u \ y) \ x) + f (u \ y - x)) + f (u - y)" ``` wenzelm@33536 ` 220` ``` by (simp add: Int_ac) ``` wenzelm@33536 ` 221` ``` also have "... = f (u \ y) + f (u - y)" ``` wenzelm@33536 ` 222` ``` using fx [THEN bspec, of "u \ y"] Int y u ``` wenzelm@33536 ` 223` ``` by force ``` wenzelm@33536 ` 224` ``` also have "... = f u" ``` wenzelm@33536 ` 225` ``` by (metis fy u) ``` wenzelm@33536 ` 226` ``` finally show "f (u \ (x \ y)) + f (u - x \ y) = f u" . ``` paulson@33271 ` 227` ``` qed ``` paulson@33271 ` 228` ``` qed ``` paulson@33271 ` 229` paulson@33271 ` 230` paulson@33271 ` 231` ```lemma (in algebra) lambda_system_Un: ``` paulson@33271 ` 232` ``` fixes f:: "'a set \ real" ``` paulson@33271 ` 233` ``` assumes xl: "x \ lambda_system M f" and yl: "y \ lambda_system M f" ``` paulson@33271 ` 234` ``` shows "x \ y \ lambda_system M f" ``` paulson@33271 ` 235` ```proof - ``` paulson@33271 ` 236` ``` have "(space M - x) \ (space M - y) \ sets M" ``` paulson@33271 ` 237` ``` by (metis Diff_Un Un compl_sets lambda_system_sets xl yl) ``` paulson@33271 ` 238` ``` moreover ``` paulson@33271 ` 239` ``` have "x \ y = space M - ((space M - x) \ (space M - y))" ``` paulson@33271 ` 240` ``` by auto (metis subsetD lambda_system_sets sets_into_space xl yl)+ ``` paulson@33271 ` 241` ``` ultimately show ?thesis ``` paulson@33271 ` 242` ``` by (metis lambda_system_Compl lambda_system_Int xl yl) ``` paulson@33271 ` 243` ```qed ``` paulson@33271 ` 244` paulson@33271 ` 245` ```lemma (in algebra) lambda_system_algebra: ``` paulson@33271 ` 246` ``` "positive M f \ algebra (M (|sets := lambda_system M f|))" ``` paulson@33271 ` 247` ``` apply (auto simp add: algebra_def) ``` paulson@33271 ` 248` ``` apply (metis lambda_system_sets set_mp sets_into_space) ``` paulson@33271 ` 249` ``` apply (metis lambda_system_empty) ``` paulson@33271 ` 250` ``` apply (metis lambda_system_Compl) ``` paulson@33271 ` 251` ``` apply (metis lambda_system_Un) ``` paulson@33271 ` 252` ``` done ``` paulson@33271 ` 253` paulson@33271 ` 254` ```lemma (in algebra) lambda_system_strong_additive: ``` paulson@33271 ` 255` ``` assumes z: "z \ sets M" and disj: "x \ y = {}" ``` paulson@33271 ` 256` ``` and xl: "x \ lambda_system M f" and yl: "y \ lambda_system M f" ``` paulson@33271 ` 257` ``` shows "f (z \ (x \ y)) = f (z \ x) + f (z \ y)" ``` paulson@33271 ` 258` ``` proof - ``` paulson@33271 ` 259` ``` have "z \ x = (z \ (x \ y)) \ x" using disj by blast ``` paulson@33271 ` 260` ``` moreover ``` paulson@33271 ` 261` ``` have "z \ y = (z \ (x \ y)) - x" using disj by blast ``` paulson@33271 ` 262` ``` moreover ``` paulson@33271 ` 263` ``` have "(z \ (x \ y)) \ sets M" ``` paulson@33271 ` 264` ``` by (metis Int Un lambda_system_sets xl yl z) ``` paulson@33271 ` 265` ``` ultimately show ?thesis using xl yl ``` paulson@33271 ` 266` ``` by (simp add: lambda_system_eq) ``` paulson@33271 ` 267` ``` qed ``` paulson@33271 ` 268` paulson@33271 ` 269` ```lemma (in algebra) Int_space_eq1 [simp]: "x \ sets M \ space M \ x = x" ``` paulson@33271 ` 270` ``` by (metis Int_absorb1 sets_into_space) ``` paulson@33271 ` 271` paulson@33271 ` 272` ```lemma (in algebra) Int_space_eq2 [simp]: "x \ sets M \ x \ space M = x" ``` paulson@33271 ` 273` ``` by (metis Int_absorb2 sets_into_space) ``` paulson@33271 ` 274` paulson@33271 ` 275` ```lemma (in algebra) lambda_system_additive: ``` paulson@33271 ` 276` ``` "additive (M (|sets := lambda_system M f|)) f" ``` paulson@33271 ` 277` ``` proof (auto simp add: additive_def) ``` paulson@33271 ` 278` ``` fix x and y ``` paulson@33271 ` 279` ``` assume disj: "x \ y = {}" ``` paulson@33271 ` 280` ``` and xl: "x \ lambda_system M f" and yl: "y \ lambda_system M f" ``` paulson@33271 ` 281` ``` hence "x \ sets M" "y \ sets M" by (blast intro: lambda_system_sets)+ ``` paulson@33271 ` 282` ``` thus "f (x \ y) = f x + f y" ``` paulson@33271 ` 283` ``` using lambda_system_strong_additive [OF top disj xl yl] ``` paulson@33271 ` 284` ``` by (simp add: Un) ``` paulson@33271 ` 285` ``` qed ``` paulson@33271 ` 286` paulson@33271 ` 287` paulson@33271 ` 288` ```lemma (in algebra) countably_subadditive_subadditive: ``` paulson@33271 ` 289` ``` assumes f: "positive M f" and cs: "countably_subadditive M f" ``` paulson@33271 ` 290` ``` shows "subadditive M f" ``` hoelzl@35582 ` 291` ```proof (auto simp add: subadditive_def) ``` paulson@33271 ` 292` ``` fix x y ``` paulson@33271 ` 293` ``` assume x: "x \ sets M" and y: "y \ sets M" and "x \ y = {}" ``` paulson@33271 ` 294` ``` hence "disjoint_family (binaryset x y)" ``` hoelzl@35582 ` 295` ``` by (auto simp add: disjoint_family_on_def binaryset_def) ``` hoelzl@35582 ` 296` ``` hence "range (binaryset x y) \ sets M \ ``` hoelzl@35582 ` 297` ``` (\i. binaryset x y i) \ sets M \ ``` paulson@33271 ` 298` ``` summable (f o (binaryset x y)) \ ``` paulson@33271 ` 299` ``` f (\i. binaryset x y i) \ suminf (\n. f (binaryset x y n))" ``` hoelzl@35582 ` 300` ``` using cs by (simp add: countably_subadditive_def) ``` hoelzl@35582 ` 301` ``` hence "{x,y,{}} \ sets M \ x \ y \ sets M \ ``` paulson@33271 ` 302` ``` summable (f o (binaryset x y)) \ ``` paulson@33271 ` 303` ``` f (x \ y) \ suminf (\n. f (binaryset x y n))" ``` paulson@33271 ` 304` ``` by (simp add: range_binaryset_eq UN_binaryset_eq) ``` paulson@33271 ` 305` ``` thus "f (x \ y) \ f x + f y" using f x y binaryset_sums ``` hoelzl@35582 ` 306` ``` by (auto simp add: Un sums_iff positive_def o_def) ``` hoelzl@35582 ` 307` ```qed ``` paulson@33271 ` 308` paulson@33271 ` 309` paulson@33271 ` 310` ```definition disjointed :: "(nat \ 'a set) \ nat \ 'a set " ``` paulson@33271 ` 311` ``` where "disjointed A n = A n - (\i\{0..i\{0..i\{0..i. disjointed A i) = (\i. A i)" ``` hoelzl@35582 ` 322` ``` apply (rule UN_finite2_eq [where k=0]) ``` hoelzl@35582 ` 323` ``` apply (simp add: finite_UN_disjointed_eq) ``` paulson@33271 ` 324` ``` done ``` paulson@33271 ` 325` paulson@33271 ` 326` ```lemma less_disjoint_disjointed: "m disjointed A m \ disjointed A n = {}" ``` paulson@33271 ` 327` ``` by (auto simp add: disjointed_def) ``` paulson@33271 ` 328` paulson@33271 ` 329` ```lemma disjoint_family_disjointed: "disjoint_family (disjointed A)" ``` hoelzl@35582 ` 330` ``` by (simp add: disjoint_family_on_def) ``` paulson@33271 ` 331` ``` (metis neq_iff Int_commute less_disjoint_disjointed) ``` paulson@33271 ` 332` paulson@33271 ` 333` ```lemma disjointed_subset: "disjointed A n \ A n" ``` paulson@33271 ` 334` ``` by (auto simp add: disjointed_def) ``` paulson@33271 ` 335` paulson@33271 ` 336` paulson@33271 ` 337` ```lemma (in algebra) UNION_in_sets: ``` paulson@33271 ` 338` ``` fixes A:: "nat \ 'a set" ``` paulson@33271 ` 339` ``` assumes A: "range A \ sets M " ``` paulson@33271 ` 340` ``` shows "(\i\{0.. sets M" ``` paulson@33271 ` 341` ```proof (induct n) ``` paulson@33271 ` 342` ``` case 0 show ?case by simp ``` paulson@33271 ` 343` ```next ``` paulson@33271 ` 344` ``` case (Suc n) ``` paulson@33271 ` 345` ``` thus ?case ``` paulson@33271 ` 346` ``` by (simp add: atLeastLessThanSuc) (metis A Un UNIV_I image_subset_iff) ``` paulson@33271 ` 347` ```qed ``` paulson@33271 ` 348` paulson@33271 ` 349` ```lemma (in algebra) range_disjointed_sets: ``` paulson@33271 ` 350` ``` assumes A: "range A \ sets M " ``` paulson@33271 ` 351` ``` shows "range (disjointed A) \ sets M" ``` paulson@33271 ` 352` ```proof (auto simp add: disjointed_def) ``` paulson@33271 ` 353` ``` fix n ``` paulson@33271 ` 354` ``` show "A n - (\i\{0.. sets M" using UNION_in_sets ``` paulson@33271 ` 355` ``` by (metis A Diff UNIV_I disjointed_def image_subset_iff) ``` paulson@33271 ` 356` ```qed ``` paulson@33271 ` 357` paulson@33271 ` 358` ```lemma sigma_algebra_disjoint_iff: ``` paulson@33271 ` 359` ``` "sigma_algebra M \ ``` paulson@33271 ` 360` ``` algebra M & ``` paulson@33271 ` 361` ``` (\A. range A \ sets M \ disjoint_family A \ ``` paulson@33271 ` 362` ``` (\i::nat. A i) \ sets M)" ``` paulson@33271 ` 363` ```proof (auto simp add: sigma_algebra_iff) ``` paulson@33271 ` 364` ``` fix A :: "nat \ 'a set" ``` paulson@33271 ` 365` ``` assume M: "algebra M" ``` paulson@33271 ` 366` ``` and A: "range A \ sets M" ``` paulson@33271 ` 367` ``` and UnA: "\A. range A \ sets M \ ``` paulson@33271 ` 368` ``` disjoint_family A \ (\i::nat. A i) \ sets M" ``` paulson@33271 ` 369` ``` hence "range (disjointed A) \ sets M \ ``` paulson@33271 ` 370` ``` disjoint_family (disjointed A) \ ``` paulson@33271 ` 371` ``` (\i. disjointed A i) \ sets M" by blast ``` paulson@33271 ` 372` ``` hence "(\i. disjointed A i) \ sets M" ``` paulson@33271 ` 373` ``` by (simp add: algebra.range_disjointed_sets M A disjoint_family_disjointed) ``` paulson@33271 ` 374` ``` thus "(\i::nat. A i) \ sets M" by (simp add: UN_disjointed_eq) ``` paulson@33271 ` 375` ```qed ``` paulson@33271 ` 376` paulson@33271 ` 377` paulson@33271 ` 378` ```lemma (in algebra) additive_sum: ``` paulson@33271 ` 379` ``` fixes A:: "nat \ 'a set" ``` paulson@33271 ` 380` ``` assumes f: "positive M f" and ad: "additive M f" ``` paulson@33271 ` 381` ``` and A: "range A \ sets M" ``` paulson@33271 ` 382` ``` and disj: "disjoint_family A" ``` paulson@33271 ` 383` ``` shows "setsum (f o A) {0..i\{0.. (\i\{0.. sets M" using A by blast ``` paulson@33271 ` 392` ``` moreover have "(\i\{0.. sets M" ``` paulson@33271 ` 393` ``` by (metis A UNION_in_sets atLeast0LessThan) ``` paulson@33271 ` 394` ``` moreover ``` paulson@33271 ` 395` ``` ultimately have "f (A n \ (\i\{0..i\{0.. range A \ sets M \ disjoint_family A \ ``` paulson@33271 ` 404` ``` (\i. A i) \ sets M \ summable (f o A) \ f (\i. A i) \ suminf (f o A)" ``` paulson@33271 ` 405` ``` by (auto simp add: countably_subadditive_def o_def) ``` paulson@33271 ` 406` paulson@33271 ` 407` ```lemma (in algebra) increasing_additive_summable: ``` paulson@33271 ` 408` ``` fixes A:: "nat \ 'a set" ``` paulson@33271 ` 409` ``` assumes f: "positive M f" and ad: "additive M f" ``` paulson@33271 ` 410` ``` and inc: "increasing M f" ``` paulson@33271 ` 411` ``` and A: "range A \ sets M" ``` paulson@33271 ` 412` ``` and disj: "disjoint_family A" ``` paulson@33271 ` 413` ``` shows "summable (f o A)" ``` paulson@33271 ` 414` ```proof (rule pos_summable) ``` paulson@33271 ` 415` ``` fix n ``` paulson@33271 ` 416` ``` show "0 \ (f \ A) n" using f A ``` paulson@33271 ` 417` ``` by (force simp add: positive_def) ``` paulson@33271 ` 418` ``` next ``` paulson@33271 ` 419` ``` fix n ``` paulson@33271 ` 420` ``` have "setsum (f \ A) {0..i\{0.. f (space M)" using space_closed A ``` paulson@33271 ` 423` ``` by (blast intro: increasingD [OF inc] UNION_in_sets top) ``` paulson@33271 ` 424` ``` finally show "setsum (f \ A) {0.. f (space M)" . ``` paulson@33271 ` 425` ```qed ``` paulson@33271 ` 426` paulson@33271 ` 427` ```lemma lambda_system_positive: ``` paulson@33271 ` 428` ``` "positive M f \ positive (M (|sets := lambda_system M f|)) f" ``` paulson@33271 ` 429` ``` by (simp add: positive_def lambda_system_def) ``` paulson@33271 ` 430` paulson@33271 ` 431` ```lemma lambda_system_increasing: ``` paulson@33271 ` 432` ``` "increasing M f \ increasing (M (|sets := lambda_system M f|)) f" ``` paulson@33271 ` 433` ``` by (simp add: increasing_def lambda_system_def) ``` paulson@33271 ` 434` paulson@33271 ` 435` ```lemma (in algebra) lambda_system_strong_sum: ``` paulson@33271 ` 436` ``` fixes A:: "nat \ 'a set" ``` paulson@33271 ` 437` ``` assumes f: "positive M f" and a: "a \ sets M" ``` paulson@33271 ` 438` ``` and A: "range A \ lambda_system M f" ``` paulson@33271 ` 439` ``` and disj: "disjoint_family A" ``` paulson@33271 ` 440` ``` shows "(\i = 0..A i)) = f (a \ (\i\{0.. UNION {0.. lambda_system M f" using A ``` paulson@33271 ` 448` ``` by blast ``` paulson@33271 ` 449` ``` have 4: "UNION {0.. lambda_system M f" ``` paulson@33271 ` 450` ``` using A algebra.UNION_in_sets [OF local.lambda_system_algebra [OF f]] ``` paulson@33271 ` 451` ``` by simp ``` paulson@33271 ` 452` ``` from Suc.hyps show ?case ``` paulson@33271 ` 453` ``` by (simp add: atLeastLessThanSuc lambda_system_strong_additive [OF a 2 3 4]) ``` paulson@33271 ` 454` ```qed ``` paulson@33271 ` 455` paulson@33271 ` 456` paulson@33271 ` 457` ```lemma (in sigma_algebra) lambda_system_caratheodory: ``` paulson@33271 ` 458` ``` assumes oms: "outer_measure_space M f" ``` paulson@33271 ` 459` ``` and A: "range A \ lambda_system M f" ``` paulson@33271 ` 460` ``` and disj: "disjoint_family A" ``` paulson@33271 ` 461` ``` shows "(\i. A i) \ lambda_system M f & (f \ A) sums f (\i. A i)" ``` paulson@33271 ` 462` ```proof - ``` paulson@33271 ` 463` ``` have pos: "positive M f" and inc: "increasing M f" ``` paulson@33271 ` 464` ``` and csa: "countably_subadditive M f" ``` paulson@33271 ` 465` ``` by (metis oms outer_measure_space_def)+ ``` paulson@33271 ` 466` ``` have sa: "subadditive M f" ``` paulson@33271 ` 467` ``` by (metis countably_subadditive_subadditive csa pos) ``` paulson@33271 ` 468` ``` have A': "range A \ sets (M(|sets := lambda_system M f|))" using A ``` paulson@33271 ` 469` ``` by simp ``` paulson@33271 ` 470` ``` have alg_ls: "algebra (M(|sets := lambda_system M f|))" ``` paulson@33271 ` 471` ``` by (rule lambda_system_algebra [OF pos]) ``` paulson@33271 ` 472` ``` have A'': "range A \ sets M" ``` paulson@33271 ` 473` ``` by (metis A image_subset_iff lambda_system_sets) ``` paulson@33271 ` 474` ``` have sumfA: "summable (f \ A)" ``` paulson@33271 ` 475` ``` by (metis algebra.increasing_additive_summable [OF alg_ls] ``` paulson@33271 ` 476` ``` lambda_system_positive lambda_system_additive lambda_system_increasing ``` paulson@33271 ` 477` ``` A' oms outer_measure_space_def disj) ``` paulson@33271 ` 478` ``` have U_in: "(\i. A i) \ sets M" ``` paulson@33271 ` 479` ``` by (metis A countable_UN image_subset_iff lambda_system_sets) ``` paulson@33271 ` 480` ``` have U_eq: "f (\i. A i) = suminf (f o A)" ``` paulson@33271 ` 481` ``` proof (rule antisym) ``` paulson@33271 ` 482` ``` show "f (\i. A i) \ suminf (f \ A)" ``` wenzelm@33536 ` 483` ``` by (rule countably_subadditiveD [OF csa A'' disj U_in sumfA]) ``` paulson@33271 ` 484` ``` show "suminf (f \ A) \ f (\i. A i)" ``` wenzelm@33536 ` 485` ``` by (rule suminf_le [OF sumfA]) ``` paulson@33271 ` 486` ``` (metis algebra.additive_sum [OF alg_ls] pos disj UN_Un Un_UNIV_right ``` wenzelm@33536 ` 487` ``` lambda_system_positive lambda_system_additive ``` paulson@33271 ` 488` ``` subset_Un_eq increasingD [OF inc] A' A'' UNION_in_sets U_in) ``` paulson@33271 ` 489` ``` qed ``` paulson@33271 ` 490` ``` { ``` paulson@33271 ` 491` ``` fix a ``` paulson@33271 ` 492` ``` assume a [iff]: "a \ sets M" ``` paulson@33271 ` 493` ``` have "f (a \ (\i. A i)) + f (a - (\i. A i)) = f a" ``` paulson@33271 ` 494` ``` proof - ``` paulson@33271 ` 495` ``` have summ: "summable (f \ (\i. a \ i) \ A)" using pos A'' ``` wenzelm@33536 ` 496` ``` apply - ``` wenzelm@33536 ` 497` ``` apply (rule summable_comparison_test [OF _ sumfA]) ``` wenzelm@33536 ` 498` ``` apply (rule_tac x="0" in exI) ``` wenzelm@33536 ` 499` ``` apply (simp add: positive_def) ``` wenzelm@33536 ` 500` ``` apply (auto simp add: ) ``` wenzelm@33536 ` 501` ``` apply (subst abs_of_nonneg) ``` wenzelm@33536 ` 502` ``` apply (metis A'' Int UNIV_I a image_subset_iff) ``` wenzelm@33536 ` 503` ``` apply (blast intro: increasingD [OF inc] a) ``` wenzelm@33536 ` 504` ``` done ``` paulson@33271 ` 505` ``` show ?thesis ``` paulson@33271 ` 506` ``` proof (rule antisym) ``` wenzelm@33536 ` 507` ``` have "range (\i. a \ A i) \ sets M" using A'' ``` wenzelm@33536 ` 508` ``` by blast ``` wenzelm@33536 ` 509` ``` moreover ``` wenzelm@33536 ` 510` ``` have "disjoint_family (\i. a \ A i)" using disj ``` hoelzl@35582 ` 511` ``` by (auto simp add: disjoint_family_on_def) ``` wenzelm@33536 ` 512` ``` moreover ``` wenzelm@33536 ` 513` ``` have "a \ (\i. A i) \ sets M" ``` wenzelm@33536 ` 514` ``` by (metis Int U_in a) ``` wenzelm@33536 ` 515` ``` ultimately ``` wenzelm@33536 ` 516` ``` have "f (a \ (\i. A i)) \ suminf (f \ (\i. a \ i) \ A)" ``` wenzelm@33536 ` 517` ``` using countably_subadditiveD [OF csa, of "(\i. a \ A i)"] summ ``` wenzelm@33536 ` 518` ``` by (simp add: o_def) ``` wenzelm@33536 ` 519` ``` moreover ``` wenzelm@33536 ` 520` ``` have "suminf (f \ (\i. a \ i) \ A) \ f a - f (a - (\i. A i))" ``` wenzelm@33536 ` 521` ``` proof (rule suminf_le [OF summ]) ``` wenzelm@33536 ` 522` ``` fix n ``` wenzelm@33536 ` 523` ``` have UNION_in: "(\i\{0.. sets M" ``` wenzelm@33536 ` 524` ``` by (metis A'' UNION_in_sets) ``` wenzelm@33536 ` 525` ``` have le_fa: "f (UNION {0.. a) \ f a" using A'' ``` wenzelm@33536 ` 526` ``` by (blast intro: increasingD [OF inc] A'' Int UNION_in_sets a) ``` wenzelm@33536 ` 527` ``` have ls: "(\i\{0.. lambda_system M f" ``` wenzelm@33536 ` 528` ``` using algebra.UNION_in_sets [OF lambda_system_algebra [OF pos]] ``` wenzelm@33536 ` 529` ``` by (simp add: A) ``` wenzelm@33536 ` 530` ``` hence eq_fa: "f (a \ (\i\{0..i\{0..i. A i)) \ f (a - (\i\{0.. (\i. a \ i) \ A) {0.. f a - f (a - (\i. A i))" ``` wenzelm@33536 ` 536` ``` using eq_fa ``` wenzelm@33536 ` 537` ``` by (simp add: suminf_le [OF summ] lambda_system_strong_sum pos ``` paulson@33271 ` 538` ``` a A disj) ``` wenzelm@33536 ` 539` ``` qed ``` wenzelm@33536 ` 540` ``` ultimately show "f (a \ (\i. A i)) + f (a - (\i. A i)) \ f a" ``` wenzelm@33536 ` 541` ``` by arith ``` paulson@33271 ` 542` ``` next ``` wenzelm@33536 ` 543` ``` have "f a \ f (a \ (\i. A i) \ (a - (\i. A i)))" ``` wenzelm@33536 ` 544` ``` by (blast intro: increasingD [OF inc] a U_in) ``` wenzelm@33536 ` 545` ``` also have "... \ f (a \ (\i. A i)) + f (a - (\i. A i))" ``` wenzelm@33536 ` 546` ``` by (blast intro: subadditiveD [OF sa] Int Diff U_in) ``` wenzelm@33536 ` 547` ``` finally show "f a \ f (a \ (\i. A i)) + f (a - (\i. A i))" . ``` paulson@33271 ` 548` ``` qed ``` paulson@33271 ` 549` ``` qed ``` paulson@33271 ` 550` ``` } ``` paulson@33271 ` 551` ``` thus ?thesis ``` paulson@33271 ` 552` ``` by (simp add: lambda_system_eq sums_iff U_eq U_in sumfA) ``` paulson@33271 ` 553` ```qed ``` paulson@33271 ` 554` paulson@33271 ` 555` ```lemma (in sigma_algebra) caratheodory_lemma: ``` paulson@33271 ` 556` ``` assumes oms: "outer_measure_space M f" ``` paulson@33271 ` 557` ``` shows "measure_space (|space = space M, sets = lambda_system M f, measure = f|)" ``` paulson@33271 ` 558` ```proof - ``` paulson@33271 ` 559` ``` have pos: "positive M f" ``` paulson@33271 ` 560` ``` by (metis oms outer_measure_space_def) ``` paulson@33271 ` 561` ``` have alg: "algebra (|space = space M, sets = lambda_system M f, measure = f|)" ``` paulson@33271 ` 562` ``` using lambda_system_algebra [OF pos] ``` paulson@33271 ` 563` ``` by (simp add: algebra_def) ``` paulson@33271 ` 564` ``` then moreover ``` paulson@33271 ` 565` ``` have "sigma_algebra (|space = space M, sets = lambda_system M f, measure = f|)" ``` paulson@33271 ` 566` ``` using lambda_system_caratheodory [OF oms] ``` paulson@33271 ` 567` ``` by (simp add: sigma_algebra_disjoint_iff) ``` paulson@33271 ` 568` ``` moreover ``` paulson@33271 ` 569` ``` have "measure_space_axioms (|space = space M, sets = lambda_system M f, measure = f|)" ``` paulson@33271 ` 570` ``` using pos lambda_system_caratheodory [OF oms] ``` paulson@33271 ` 571` ``` by (simp add: measure_space_axioms_def positive_def lambda_system_sets ``` paulson@33271 ` 572` ``` countably_additive_def o_def) ``` paulson@33271 ` 573` ``` ultimately ``` paulson@33271 ` 574` ``` show ?thesis ``` paulson@33271 ` 575` ``` by intro_locales (auto simp add: sigma_algebra_def) ``` paulson@33271 ` 576` ```qed ``` paulson@33271 ` 577` paulson@33271 ` 578` paulson@33271 ` 579` ```lemma (in algebra) inf_measure_nonempty: ``` paulson@33271 ` 580` ``` assumes f: "positive M f" and b: "b \ sets M" and a: "a \ b" ``` paulson@33271 ` 581` ``` shows "f b \ measure_set M f a" ``` paulson@33271 ` 582` ```proof - ``` paulson@33271 ` 583` ``` have "(f \ (\i. {})(0 := b)) sums setsum (f \ (\i. {})(0 := b)) {0..<1::nat}" ``` paulson@33271 ` 584` ``` by (rule series_zero) (simp add: positive_imp_0 [OF f]) ``` paulson@33271 ` 585` ``` also have "... = f b" ``` paulson@33271 ` 586` ``` by simp ``` paulson@33271 ` 587` ``` finally have "(f \ (\i. {})(0 := b)) sums f b" . ``` paulson@33271 ` 588` ``` thus ?thesis using a ``` paulson@33271 ` 589` ``` by (auto intro!: exI [of _ "(\i. {})(0 := b)"] ``` hoelzl@35582 ` 590` ``` simp add: measure_set_def disjoint_family_on_def b split_if_mem2) ``` paulson@33271 ` 591` ```qed ``` paulson@33271 ` 592` paulson@33271 ` 593` ```lemma (in algebra) inf_measure_pos0: ``` paulson@33271 ` 594` ``` "positive M f \ x \ measure_set M f a \ 0 \ x" ``` paulson@33271 ` 595` ```apply (auto simp add: positive_def measure_set_def sums_iff intro!: suminf_ge_zero) ``` paulson@33271 ` 596` ```apply blast ``` paulson@33271 ` 597` ```done ``` paulson@33271 ` 598` paulson@33271 ` 599` ```lemma (in algebra) inf_measure_pos: ``` paulson@33271 ` 600` ``` shows "positive M f \ x \ space M \ 0 \ Inf (measure_set M f x)" ``` paulson@33271 ` 601` ```apply (rule Inf_greatest) ``` paulson@33271 ` 602` ```apply (metis emptyE inf_measure_nonempty top) ``` paulson@33271 ` 603` ```apply (metis inf_measure_pos0) ``` paulson@33271 ` 604` ```done ``` paulson@33271 ` 605` paulson@33271 ` 606` ```lemma (in algebra) additive_increasing: ``` paulson@33271 ` 607` ``` assumes posf: "positive M f" and addf: "additive M f" ``` paulson@33271 ` 608` ``` shows "increasing M f" ``` paulson@33271 ` 609` ```proof (auto simp add: increasing_def) ``` paulson@33271 ` 610` ``` fix x y ``` paulson@33271 ` 611` ``` assume xy: "x \ sets M" "y \ sets M" "x \ y" ``` paulson@33271 ` 612` ``` have "f x \ f x + f (y-x)" using posf ``` paulson@33271 ` 613` ``` by (simp add: positive_def) (metis Diff xy) ``` paulson@33271 ` 614` ``` also have "... = f (x \ (y-x))" using addf ``` paulson@33271 ` 615` ``` by (auto simp add: additive_def) (metis Diff_disjoint Un_Diff_cancel Diff xy) ``` paulson@33271 ` 616` ``` also have "... = f y" ``` paulson@33271 ` 617` ``` by (metis Un_Diff_cancel Un_absorb1 xy) ``` paulson@33271 ` 618` ``` finally show "f x \ f y" . ``` paulson@33271 ` 619` ```qed ``` paulson@33271 ` 620` paulson@33271 ` 621` ```lemma (in algebra) countably_additive_additive: ``` paulson@33271 ` 622` ``` assumes posf: "positive M f" and ca: "countably_additive M f" ``` paulson@33271 ` 623` ``` shows "additive M f" ``` paulson@33271 ` 624` ```proof (auto simp add: additive_def) ``` paulson@33271 ` 625` ``` fix x y ``` paulson@33271 ` 626` ``` assume x: "x \ sets M" and y: "y \ sets M" and "x \ y = {}" ``` paulson@33271 ` 627` ``` hence "disjoint_family (binaryset x y)" ``` hoelzl@35582 ` 628` ``` by (auto simp add: disjoint_family_on_def binaryset_def) ``` paulson@33271 ` 629` ``` hence "range (binaryset x y) \ sets M \ ``` paulson@33271 ` 630` ``` (\i. binaryset x y i) \ sets M \ ``` paulson@33271 ` 631` ``` f (\i. binaryset x y i) = suminf (\n. f (binaryset x y n))" ``` paulson@33271 ` 632` ``` using ca ``` paulson@33271 ` 633` ``` by (simp add: countably_additive_def) (metis UN_binaryset_eq sums_unique) ``` paulson@33271 ` 634` ``` hence "{x,y,{}} \ sets M \ x \ y \ sets M \ ``` paulson@33271 ` 635` ``` f (x \ y) = suminf (\n. f (binaryset x y n))" ``` paulson@33271 ` 636` ``` by (simp add: range_binaryset_eq UN_binaryset_eq) ``` paulson@33271 ` 637` ``` thus "f (x \ y) = f x + f y" using posf x y ``` paulson@33271 ` 638` ``` by (simp add: Un suminf_binaryset_eq positive_def) ``` paulson@33271 ` 639` ```qed ``` paulson@33271 ` 640` ``` ``` paulson@33271 ` 641` ```lemma (in algebra) inf_measure_agrees: ``` paulson@33271 ` 642` ``` assumes posf: "positive M f" and ca: "countably_additive M f" ``` paulson@33271 ` 643` ``` and s: "s \ sets M" ``` paulson@33271 ` 644` ``` shows "Inf (measure_set M f s) = f s" ``` paulson@33271 ` 645` ```proof (rule Inf_eq) ``` paulson@33271 ` 646` ``` fix z ``` paulson@33271 ` 647` ``` assume z: "z \ measure_set M f s" ``` paulson@33271 ` 648` ``` from this obtain A where ``` paulson@33271 ` 649` ``` A: "range A \ sets M" and disj: "disjoint_family A" ``` paulson@33271 ` 650` ``` and "s \ (\x. A x)" and sm: "summable (f \ A)" ``` paulson@33271 ` 651` ``` and si: "suminf (f \ A) = z" ``` paulson@33271 ` 652` ``` by (auto simp add: measure_set_def sums_iff) ``` paulson@33271 ` 653` ``` hence seq: "s = (\i. A i \ s)" by blast ``` paulson@33271 ` 654` ``` have inc: "increasing M f" ``` paulson@33271 ` 655` ``` by (metis additive_increasing ca countably_additive_additive posf) ``` paulson@33271 ` 656` ``` have sums: "(\i. f (A i \ s)) sums f (\i. A i \ s)" ``` paulson@33271 ` 657` ``` proof (rule countably_additiveD [OF ca]) ``` paulson@33271 ` 658` ``` show "range (\n. A n \ s) \ sets M" using A s ``` wenzelm@33536 ` 659` ``` by blast ``` paulson@33271 ` 660` ``` show "disjoint_family (\n. A n \ s)" using disj ``` hoelzl@35582 ` 661` ``` by (auto simp add: disjoint_family_on_def) ``` paulson@33271 ` 662` ``` show "(\i. A i \ s) \ sets M" using A s ``` wenzelm@33536 ` 663` ``` by (metis UN_extend_simps(4) s seq) ``` paulson@33271 ` 664` ``` qed ``` paulson@33271 ` 665` ``` hence "f s = suminf (\i. f (A i \ s))" ``` paulson@33271 ` 666` ``` by (metis Int_commute UN_simps(4) seq sums_iff) ``` paulson@33271 ` 667` ``` also have "... \ suminf (f \ A)" ``` paulson@33271 ` 668` ``` proof (rule summable_le [OF _ _ sm]) ``` paulson@33271 ` 669` ``` show "\n. f (A n \ s) \ (f \ A) n" using A s ``` wenzelm@33536 ` 670` ``` by (force intro: increasingD [OF inc]) ``` paulson@33271 ` 671` ``` show "summable (\i. f (A i \ s))" using sums ``` wenzelm@33536 ` 672` ``` by (simp add: sums_iff) ``` paulson@33271 ` 673` ``` qed ``` paulson@33271 ` 674` ``` also have "... = z" by (rule si) ``` paulson@33271 ` 675` ``` finally show "f s \ z" . ``` paulson@33271 ` 676` ```next ``` paulson@33271 ` 677` ``` fix y ``` paulson@33271 ` 678` ``` assume y: "!!u. u \ measure_set M f s \ y \ u" ``` paulson@33271 ` 679` ``` thus "y \ f s" ``` paulson@33271 ` 680` ``` by (blast intro: inf_measure_nonempty [OF posf s subset_refl]) ``` paulson@33271 ` 681` ```qed ``` paulson@33271 ` 682` paulson@33271 ` 683` ```lemma (in algebra) inf_measure_empty: ``` paulson@33271 ` 684` ``` assumes posf: "positive M f" ``` paulson@33271 ` 685` ``` shows "Inf (measure_set M f {}) = 0" ``` paulson@33271 ` 686` ```proof (rule antisym) ``` paulson@33271 ` 687` ``` show "0 \ Inf (measure_set M f {})" ``` paulson@33271 ` 688` ``` by (metis empty_subsetI inf_measure_pos posf) ``` paulson@33271 ` 689` ``` show "Inf (measure_set M f {}) \ 0" ``` paulson@33271 ` 690` ``` by (metis Inf_lower empty_sets inf_measure_pos0 inf_measure_nonempty posf ``` paulson@33271 ` 691` ``` positive_imp_0 subset_refl) ``` paulson@33271 ` 692` ```qed ``` paulson@33271 ` 693` paulson@33271 ` 694` ```lemma (in algebra) inf_measure_positive: ``` paulson@33271 ` 695` ``` "positive M f \ ``` paulson@33271 ` 696` ``` positive (| space = space M, sets = Pow (space M) |) ``` paulson@33271 ` 697` ``` (\x. Inf (measure_set M f x))" ``` paulson@33271 ` 698` ``` by (simp add: positive_def inf_measure_empty inf_measure_pos) ``` paulson@33271 ` 699` paulson@33271 ` 700` ```lemma (in algebra) inf_measure_increasing: ``` paulson@33271 ` 701` ``` assumes posf: "positive M f" ``` paulson@33271 ` 702` ``` shows "increasing (| space = space M, sets = Pow (space M) |) ``` paulson@33271 ` 703` ``` (\x. Inf (measure_set M f x))" ``` paulson@33271 ` 704` ```apply (auto simp add: increasing_def) ``` paulson@33271 ` 705` ```apply (rule Inf_greatest, metis emptyE inf_measure_nonempty top posf) ``` paulson@33271 ` 706` ```apply (rule Inf_lower) ``` paulson@33271 ` 707` ```apply (clarsimp simp add: measure_set_def, blast) ``` paulson@33271 ` 708` ```apply (blast intro: inf_measure_pos0 posf) ``` paulson@33271 ` 709` ```done ``` paulson@33271 ` 710` paulson@33271 ` 711` paulson@33271 ` 712` ```lemma (in algebra) inf_measure_le: ``` paulson@33271 ` 713` ``` assumes posf: "positive M f" and inc: "increasing M f" ``` paulson@33271 ` 714` ``` and x: "x \ {r . \A. range A \ sets M & s \ (\i. A i) & (f \ A) sums r}" ``` paulson@33271 ` 715` ``` shows "Inf (measure_set M f s) \ x" ``` paulson@33271 ` 716` ```proof - ``` paulson@33271 ` 717` ``` from x ``` paulson@33271 ` 718` ``` obtain A where A: "range A \ sets M" and ss: "s \ (\i. A i)" ``` paulson@33271 ` 719` ``` and sm: "summable (f \ A)" and xeq: "suminf (f \ A) = x" ``` paulson@33271 ` 720` ``` by (auto simp add: sums_iff) ``` paulson@33271 ` 721` ``` have dA: "range (disjointed A) \ sets M" ``` paulson@33271 ` 722` ``` by (metis A range_disjointed_sets) ``` paulson@33271 ` 723` ``` have "\n. \(f o disjointed A) n\ \ (f \ A) n" ``` paulson@33271 ` 724` ``` proof (auto) ``` paulson@33271 ` 725` ``` fix n ``` paulson@33271 ` 726` ``` have "\f (disjointed A n)\ = f (disjointed A n)" using posf dA ``` wenzelm@33536 ` 727` ``` by (auto simp add: positive_def image_subset_iff) ``` paulson@33271 ` 728` ``` also have "... \ f (A n)" ``` wenzelm@33536 ` 729` ``` by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A) ``` paulson@33271 ` 730` ``` finally show "\f (disjointed A n)\ \ f (A n)" . ``` paulson@33271 ` 731` ``` qed ``` paulson@33271 ` 732` ``` from Series.summable_le2 [OF this sm] ``` paulson@33271 ` 733` ``` have sda: "summable (f o disjointed A)" ``` paulson@33271 ` 734` ``` "suminf (f o disjointed A) \ suminf (f \ A)" ``` paulson@33271 ` 735` ``` by blast+ ``` paulson@33271 ` 736` ``` hence ley: "suminf (f o disjointed A) \ x" ``` paulson@33271 ` 737` ``` by (metis xeq) ``` paulson@33271 ` 738` ``` from sda have "(f \ disjointed A) sums suminf (f \ disjointed A)" ``` paulson@33271 ` 739` ``` by (simp add: sums_iff) ``` paulson@33271 ` 740` ``` hence y: "suminf (f o disjointed A) \ measure_set M f s" ``` paulson@33271 ` 741` ``` apply (auto simp add: measure_set_def) ``` paulson@33271 ` 742` ``` apply (rule_tac x="disjointed A" in exI) ``` paulson@33271 ` 743` ``` apply (simp add: disjoint_family_disjointed UN_disjointed_eq ss dA) ``` paulson@33271 ` 744` ``` done ``` paulson@33271 ` 745` ``` show ?thesis ``` paulson@33271 ` 746` ``` by (blast intro: Inf_lower y order_trans [OF _ ley] inf_measure_pos0 posf) ``` paulson@33271 ` 747` ```qed ``` paulson@33271 ` 748` paulson@33271 ` 749` ```lemma (in algebra) inf_measure_close: ``` paulson@33271 ` 750` ``` assumes posf: "positive M f" and e: "0 < e" and ss: "s \ (space M)" ``` paulson@33271 ` 751` ``` shows "\A l. range A \ sets M & disjoint_family A & s \ (\i. A i) & ``` paulson@33271 ` 752` ``` (f \ A) sums l & l \ Inf (measure_set M f s) + e" ``` paulson@33271 ` 753` ```proof - ``` paulson@33271 ` 754` ``` have " measure_set M f s \ {}" ``` paulson@33271 ` 755` ``` by (metis emptyE ss inf_measure_nonempty [OF posf top]) ``` paulson@33271 ` 756` ``` hence "\l \ measure_set M f s. l < Inf (measure_set M f s) + e" ``` paulson@33271 ` 757` ``` by (rule Inf_close [OF _ e]) ``` paulson@33271 ` 758` ``` thus ?thesis ``` paulson@33271 ` 759` ``` by (auto simp add: measure_set_def, rule_tac x=" A" in exI, auto) ``` paulson@33271 ` 760` ```qed ``` paulson@33271 ` 761` paulson@33271 ` 762` ```lemma (in algebra) inf_measure_countably_subadditive: ``` paulson@33271 ` 763` ``` assumes posf: "positive M f" and inc: "increasing M f" ``` paulson@33271 ` 764` ``` shows "countably_subadditive (| space = space M, sets = Pow (space M) |) ``` paulson@33271 ` 765` ``` (\x. Inf (measure_set M f x))" ``` paulson@33271 ` 766` ```proof (auto simp add: countably_subadditive_def o_def, rule field_le_epsilon) ``` paulson@33271 ` 767` ``` fix A :: "nat \ 'a set" and e :: real ``` paulson@33271 ` 768` ``` assume A: "range A \ Pow (space M)" ``` paulson@33271 ` 769` ``` and disj: "disjoint_family A" ``` paulson@33271 ` 770` ``` and sb: "(\i. A i) \ space M" ``` paulson@33271 ` 771` ``` and sum1: "summable (\n. Inf (measure_set M f (A n)))" ``` paulson@33271 ` 772` ``` and e: "0 < e" ``` paulson@33271 ` 773` ``` have "!!n. \B l. range B \ sets M \ disjoint_family B \ A n \ (\i. B i) \ ``` paulson@33271 ` 774` ``` (f o B) sums l \ ``` paulson@33271 ` 775` ``` l \ Inf (measure_set M f (A n)) + e * (1/2)^(Suc n)" ``` paulson@33271 ` 776` ``` apply (rule inf_measure_close [OF posf]) ``` paulson@33271 ` 777` ``` apply (metis e half mult_pos_pos zero_less_power) ``` paulson@33271 ` 778` ``` apply (metis UNIV_I UN_subset_iff sb) ``` paulson@33271 ` 779` ``` done ``` paulson@33271 ` 780` ``` hence "\BB ll. \n. range (BB n) \ sets M \ disjoint_family (BB n) \ ``` paulson@33271 ` 781` ``` A n \ (\i. BB n i) \ (f o BB n) sums ll n \ ``` paulson@33271 ` 782` ``` ll n \ Inf (measure_set M f (A n)) + e * (1/2)^(Suc n)" ``` paulson@33271 ` 783` ``` by (rule choice2) ``` paulson@33271 ` 784` ``` then obtain BB ll ``` paulson@33271 ` 785` ``` where BB: "!!n. (range (BB n) \ sets M)" ``` paulson@33271 ` 786` ``` and disjBB: "!!n. disjoint_family (BB n)" ``` paulson@33271 ` 787` ``` and sbBB: "!!n. A n \ (\i. BB n i)" ``` paulson@33271 ` 788` ``` and BBsums: "!!n. (f o BB n) sums ll n" ``` paulson@33271 ` 789` ``` and ll: "!!n. ll n \ Inf (measure_set M f (A n)) + e * (1/2)^(Suc n)" ``` paulson@33271 ` 790` ``` by auto blast ``` paulson@33271 ` 791` ``` have llpos: "!!n. 0 \ ll n" ``` wenzelm@33536 ` 792` ``` by (metis BBsums sums_iff o_apply posf positive_imp_pos suminf_ge_zero ``` paulson@33271 ` 793` ``` range_subsetD BB) ``` paulson@33271 ` 794` ``` have sll: "summable ll & ``` paulson@33271 ` 795` ``` suminf ll \ suminf (\n. Inf (measure_set M f (A n))) + e" ``` paulson@33271 ` 796` ``` proof - ``` wenzelm@33536 ` 797` ``` have "(\n. e * (1/2)^(Suc n)) sums (e*1)" ``` wenzelm@33536 ` 798` ``` by (rule sums_mult [OF power_half_series]) ``` wenzelm@33536 ` 799` ``` hence sum0: "summable (\n. e * (1 / 2) ^ Suc n)" ``` wenzelm@33536 ` 800` ``` and eqe: "(\n. e * (1 / 2) ^ n / 2) = e" ``` wenzelm@33536 ` 801` ``` by (auto simp add: sums_iff) ``` wenzelm@33536 ` 802` ``` have 0: "suminf (\n. Inf (measure_set M f (A n))) + ``` paulson@33271 ` 803` ``` suminf (\n. e * (1/2)^(Suc n)) = ``` paulson@33271 ` 804` ``` suminf (\n. Inf (measure_set M f (A n)) + e * (1/2)^(Suc n))" ``` wenzelm@33536 ` 805` ``` by (rule suminf_add [OF sum1 sum0]) ``` wenzelm@33536 ` 806` ``` have 1: "\n. \ll n\ \ Inf (measure_set M f (A n)) + e * (1/2) ^ Suc n" ``` wenzelm@33536 ` 807` ``` by (metis ll llpos abs_of_nonneg) ``` wenzelm@33536 ` 808` ``` have 2: "summable (\n. Inf (measure_set M f (A n)) + e*(1/2)^(Suc n))" ``` wenzelm@33536 ` 809` ``` by (rule summable_add [OF sum1 sum0]) ``` wenzelm@33536 ` 810` ``` have "suminf ll \ (\n. Inf (measure_set M f (A n)) + e*(1/2) ^ Suc n)" ``` wenzelm@33536 ` 811` ``` using Series.summable_le2 [OF 1 2] by auto ``` wenzelm@33536 ` 812` ``` also have "... = (\n. Inf (measure_set M f (A n))) + ``` paulson@33271 ` 813` ``` (\n. e * (1 / 2) ^ Suc n)" ``` wenzelm@33536 ` 814` ``` by (metis 0) ``` wenzelm@33536 ` 815` ``` also have "... = (\n. Inf (measure_set M f (A n))) + e" ``` wenzelm@33536 ` 816` ``` by (simp add: eqe) ``` wenzelm@33536 ` 817` ``` finally show ?thesis using Series.summable_le2 [OF 1 2] by auto ``` paulson@33271 ` 818` ``` qed ``` huffman@35704 ` 819` ``` def C \ "(split BB) o prod_decode" ``` paulson@33271 ` 820` ``` have C: "!!n. C n \ sets M" ``` huffman@35704 ` 821` ``` apply (rule_tac p="prod_decode n" in PairE) ``` paulson@33271 ` 822` ``` apply (simp add: C_def) ``` paulson@33271 ` 823` ``` apply (metis BB subsetD rangeI) ``` paulson@33271 ` 824` ``` done ``` paulson@33271 ` 825` ``` have sbC: "(\i. A i) \ (\i. C i)" ``` paulson@33271 ` 826` ``` proof (auto simp add: C_def) ``` wenzelm@33536 ` 827` ``` fix x i ``` wenzelm@33536 ` 828` ``` assume x: "x \ A i" ``` wenzelm@33536 ` 829` ``` with sbBB [of i] obtain j where "x \ BB i j" ``` wenzelm@33536 ` 830` ``` by blast ``` huffman@35704 ` 831` ``` thus "\i. x \ split BB (prod_decode i)" ``` huffman@35704 ` 832` ``` by (metis prod_encode_inverse prod.cases prod_case_split) ``` paulson@33271 ` 833` ``` qed ``` huffman@35704 ` 834` ``` have "(f \ C) = (f \ (\(x, y). BB x y)) \ prod_decode" ``` paulson@33271 ` 835` ``` by (rule ext) (auto simp add: C_def) ``` paulson@33271 ` 836` ``` also have "... sums suminf ll" ``` paulson@33271 ` 837` ``` proof (rule suminf_2dimen) ``` wenzelm@33536 ` 838` ``` show "\m n. 0 \ (f \ (\(x, y). BB x y)) (m, n)" using posf BB ``` wenzelm@33536 ` 839` ``` by (force simp add: positive_def) ``` wenzelm@33536 ` 840` ``` show "\m. (\n. (f \ (\(x, y). BB x y)) (m, n)) sums ll m"using BBsums BB ``` wenzelm@33536 ` 841` ``` by (force simp add: o_def) ``` wenzelm@33536 ` 842` ``` show "summable ll" using sll ``` wenzelm@33536 ` 843` ``` by auto ``` paulson@33271 ` 844` ``` qed ``` paulson@33271 ` 845` ``` finally have Csums: "(f \ C) sums suminf ll" . ``` paulson@33271 ` 846` ``` have "Inf (measure_set M f (\i. A i)) \ suminf ll" ``` paulson@33271 ` 847` ``` apply (rule inf_measure_le [OF posf inc], auto) ``` paulson@33271 ` 848` ``` apply (rule_tac x="C" in exI) ``` paulson@33271 ` 849` ``` apply (auto simp add: C sbC Csums) ``` paulson@33271 ` 850` ``` done ``` paulson@33271 ` 851` ``` also have "... \ (\n. Inf (measure_set M f (A n))) + e" using sll ``` paulson@33271 ` 852` ``` by blast ``` paulson@33271 ` 853` ``` finally show "Inf (measure_set M f (\i. A i)) \ ``` paulson@33271 ` 854` ``` (\n. Inf (measure_set M f (A n))) + e" . ``` paulson@33271 ` 855` ```qed ``` paulson@33271 ` 856` paulson@33271 ` 857` ```lemma (in algebra) inf_measure_outer: ``` paulson@33271 ` 858` ``` "positive M f \ increasing M f ``` paulson@33271 ` 859` ``` \ outer_measure_space (| space = space M, sets = Pow (space M) |) ``` paulson@33271 ` 860` ``` (\x. Inf (measure_set M f x))" ``` paulson@33271 ` 861` ``` by (simp add: outer_measure_space_def inf_measure_positive ``` paulson@33271 ` 862` ``` inf_measure_increasing inf_measure_countably_subadditive) ``` paulson@33271 ` 863` paulson@33271 ` 864` ```(*MOVE UP*) ``` paulson@33271 ` 865` paulson@33271 ` 866` ```lemma (in algebra) algebra_subset_lambda_system: ``` paulson@33271 ` 867` ``` assumes posf: "positive M f" and inc: "increasing M f" ``` paulson@33271 ` 868` ``` and add: "additive M f" ``` paulson@33271 ` 869` ``` shows "sets M \ lambda_system (| space = space M, sets = Pow (space M) |) ``` paulson@33271 ` 870` ``` (\x. Inf (measure_set M f x))" ``` paulson@33271 ` 871` ```proof (auto dest: sets_into_space ``` paulson@33271 ` 872` ``` simp add: algebra.lambda_system_eq [OF algebra_Pow]) ``` paulson@33271 ` 873` ``` fix x s ``` paulson@33271 ` 874` ``` assume x: "x \ sets M" ``` paulson@33271 ` 875` ``` and s: "s \ space M" ``` paulson@33271 ` 876` ``` have [simp]: "!!x. x \ sets M \ s \ (space M - x) = s-x" using s ``` paulson@33271 ` 877` ``` by blast ``` paulson@33271 ` 878` ``` have "Inf (measure_set M f (s\x)) + Inf (measure_set M f (s-x)) ``` paulson@33271 ` 879` ``` \ Inf (measure_set M f s)" ``` paulson@33271 ` 880` ``` proof (rule field_le_epsilon) ``` paulson@33271 ` 881` ``` fix e :: real ``` paulson@33271 ` 882` ``` assume e: "0 < e" ``` paulson@33271 ` 883` ``` from inf_measure_close [OF posf e s] ``` paulson@33271 ` 884` ``` obtain A l where A: "range A \ sets M" and disj: "disjoint_family A" ``` paulson@33271 ` 885` ``` and sUN: "s \ (\i. A i)" and fsums: "(f \ A) sums l" ``` wenzelm@33536 ` 886` ``` and l: "l \ Inf (measure_set M f s) + e" ``` wenzelm@33536 ` 887` ``` by auto ``` paulson@33271 ` 888` ``` have [simp]: "!!x. x \ sets M \ ``` paulson@33271 ` 889` ``` (f o (\z. z \ (space M - x)) o A) = (f o (\z. z - x) o A)" ``` wenzelm@33536 ` 890` ``` by (rule ext, simp, metis A Int_Diff Int_space_eq2 range_subsetD) ``` paulson@33271 ` 891` ``` have [simp]: "!!n. f (A n \ x) + f (A n - x) = f (A n)" ``` wenzelm@33536 ` 892` ``` by (subst additiveD [OF add, symmetric]) ``` wenzelm@33536 ` 893` ``` (auto simp add: x range_subsetD [OF A] Int_Diff_Un Int_Diff_disjoint) ``` paulson@33271 ` 894` ``` have fsumb: "summable (f \ A)" ``` wenzelm@33536 ` 895` ``` by (metis fsums sums_iff) ``` paulson@33271 ` 896` ``` { fix u ``` wenzelm@33536 ` 897` ``` assume u: "u \ sets M" ``` wenzelm@33536 ` 898` ``` have [simp]: "\n. \f (A n \ u)\ \ f (A n)" ``` wenzelm@33536 ` 899` ``` by (simp add: positive_imp_pos [OF posf] increasingD [OF inc] ``` paulson@33271 ` 900` ``` u Int range_subsetD [OF A]) ``` wenzelm@33536 ` 901` ``` have 1: "summable (f o (\z. z\u) o A)" ``` paulson@33271 ` 902` ``` by (rule summable_comparison_test [OF _ fsumb]) simp ``` wenzelm@33536 ` 903` ``` have 2: "Inf (measure_set M f (s\u)) \ suminf (f o (\z. z\u) o A)" ``` paulson@33271 ` 904` ``` proof (rule Inf_lower) ``` paulson@33271 ` 905` ``` show "suminf (f \ (\z. z \ u) \ A) \ measure_set M f (s \ u)" ``` paulson@33271 ` 906` ``` apply (simp add: measure_set_def) ``` paulson@33271 ` 907` ``` apply (rule_tac x="(\z. z \ u) o A" in exI) ``` paulson@33271 ` 908` ``` apply (auto simp add: disjoint_family_subset [OF disj]) ``` paulson@33271 ` 909` ``` apply (blast intro: u range_subsetD [OF A]) ``` paulson@33271 ` 910` ``` apply (blast dest: subsetD [OF sUN]) ``` paulson@33271 ` 911` ``` apply (metis 1 o_assoc sums_iff) ``` paulson@33271 ` 912` ``` done ``` paulson@33271 ` 913` ``` next ``` paulson@33271 ` 914` ``` show "\x. x \ measure_set M f (s \ u) \ 0 \ x" ``` paulson@33271 ` 915` ``` by (blast intro: inf_measure_pos0 [OF posf]) ``` paulson@33271 ` 916` ``` qed ``` paulson@33271 ` 917` ``` note 1 2 ``` paulson@33271 ` 918` ``` } note lesum = this ``` paulson@33271 ` 919` ``` have sum1: "summable (f o (\z. z\x) o A)" ``` paulson@33271 ` 920` ``` and inf1: "Inf (measure_set M f (s\x)) \ suminf (f o (\z. z\x) o A)" ``` paulson@33271 ` 921` ``` and sum2: "summable (f o (\z. z \ (space M - x)) o A)" ``` paulson@33271 ` 922` ``` and inf2: "Inf (measure_set M f (s \ (space M - x))) ``` paulson@33271 ` 923` ``` \ suminf (f o (\z. z \ (space M - x)) o A)" ``` wenzelm@33536 ` 924` ``` by (metis Diff lesum top x)+ ``` paulson@33271 ` 925` ``` hence "Inf (measure_set M f (s\x)) + Inf (measure_set M f (s-x)) ``` paulson@33271 ` 926` ``` \ suminf (f o (\s. s\x) o A) + suminf (f o (\s. s-x) o A)" ``` wenzelm@33536 ` 927` ``` by (simp add: x) ``` paulson@33271 ` 928` ``` also have "... \ suminf (f o A)" using suminf_add [OF sum1 sum2] ``` wenzelm@33536 ` 929` ``` by (simp add: x) (simp add: o_def) ``` paulson@33271 ` 930` ``` also have "... \ Inf (measure_set M f s) + e" ``` wenzelm@33536 ` 931` ``` by (metis fsums l sums_unique) ``` paulson@33271 ` 932` ``` finally show "Inf (measure_set M f (s\x)) + Inf (measure_set M f (s-x)) ``` paulson@33271 ` 933` ``` \ Inf (measure_set M f s) + e" . ``` paulson@33271 ` 934` ``` qed ``` paulson@33271 ` 935` ``` moreover ``` paulson@33271 ` 936` ``` have "Inf (measure_set M f s) ``` paulson@33271 ` 937` ``` \ Inf (measure_set M f (s\x)) + Inf (measure_set M f (s-x))" ``` paulson@33271 ` 938` ``` proof - ``` paulson@33271 ` 939` ``` have "Inf (measure_set M f s) = Inf (measure_set M f ((s\x) \ (s-x)))" ``` paulson@33271 ` 940` ``` by (metis Un_Diff_Int Un_commute) ``` paulson@33271 ` 941` ``` also have "... \ Inf (measure_set M f (s\x)) + Inf (measure_set M f (s-x))" ``` paulson@33271 ` 942` ``` apply (rule subadditiveD) ``` paulson@33271 ` 943` ``` apply (iprover intro: algebra.countably_subadditive_subadditive algebra_Pow ``` wenzelm@33536 ` 944` ``` inf_measure_positive inf_measure_countably_subadditive posf inc) ``` paulson@33271 ` 945` ``` apply (auto simp add: subsetD [OF s]) ``` paulson@33271 ` 946` ``` done ``` paulson@33271 ` 947` ``` finally show ?thesis . ``` paulson@33271 ` 948` ``` qed ``` paulson@33271 ` 949` ``` ultimately ``` paulson@33271 ` 950` ``` show "Inf (measure_set M f (s\x)) + Inf (measure_set M f (s-x)) ``` paulson@33271 ` 951` ``` = Inf (measure_set M f s)" ``` paulson@33271 ` 952` ``` by (rule order_antisym) ``` paulson@33271 ` 953` ```qed ``` paulson@33271 ` 954` paulson@33271 ` 955` ```lemma measure_down: ``` paulson@33271 ` 956` ``` "measure_space N \ sigma_algebra M \ sets M \ sets N \ ``` paulson@33271 ` 957` ``` (measure M = measure N) \ measure_space M" ``` paulson@33271 ` 958` ``` by (simp add: measure_space_def measure_space_axioms_def positive_def ``` paulson@33271 ` 959` ``` countably_additive_def) ``` paulson@33271 ` 960` ``` blast ``` paulson@33271 ` 961` paulson@33271 ` 962` ```theorem (in algebra) caratheodory: ``` paulson@33271 ` 963` ``` assumes posf: "positive M f" and ca: "countably_additive M f" ``` paulson@33271 ` 964` ``` shows "\MS :: 'a measure_space. ``` paulson@33271 ` 965` ``` (\s \ sets M. measure MS s = f s) \ ``` paulson@33271 ` 966` ``` ((|space = space MS, sets = sets MS|) = sigma (space M) (sets M)) \ ``` paulson@33271 ` 967` ``` measure_space MS" ``` paulson@33271 ` 968` ``` proof - ``` paulson@33271 ` 969` ``` have inc: "increasing M f" ``` paulson@33271 ` 970` ``` by (metis additive_increasing ca countably_additive_additive posf) ``` paulson@33271 ` 971` ``` let ?infm = "(\x. Inf (measure_set M f x))" ``` paulson@33271 ` 972` ``` def ls \ "lambda_system (|space = space M, sets = Pow (space M)|) ?infm" ``` paulson@33271 ` 973` ``` have mls: "measure_space (|space = space M, sets = ls, measure = ?infm|)" ``` paulson@33271 ` 974` ``` using sigma_algebra.caratheodory_lemma ``` paulson@33271 ` 975` ``` [OF sigma_algebra_Pow inf_measure_outer [OF posf inc]] ``` paulson@33271 ` 976` ``` by (simp add: ls_def) ``` paulson@33271 ` 977` ``` hence sls: "sigma_algebra (|space = space M, sets = ls, measure = ?infm|)" ``` paulson@33271 ` 978` ``` by (simp add: measure_space_def) ``` paulson@33271 ` 979` ``` have "sets M \ ls" ``` paulson@33271 ` 980` ``` by (simp add: ls_def) ``` paulson@33271 ` 981` ``` (metis ca posf inc countably_additive_additive algebra_subset_lambda_system) ``` paulson@33271 ` 982` ``` hence sgs_sb: "sigma_sets (space M) (sets M) \ ls" ``` paulson@33271 ` 983` ``` using sigma_algebra.sigma_sets_subset [OF sls, of "sets M"] ``` paulson@33271 ` 984` ``` by simp ``` paulson@33271 ` 985` ``` have "measure_space (|space = space M, ``` paulson@33271 ` 986` ``` sets = sigma_sets (space M) (sets M), ``` paulson@33271 ` 987` ``` measure = ?infm|)" ``` paulson@33271 ` 988` ``` by (rule measure_down [OF mls], rule sigma_algebra_sigma_sets) ``` paulson@33271 ` 989` ``` (simp_all add: sgs_sb space_closed) ``` paulson@33271 ` 990` ``` thus ?thesis ``` paulson@33271 ` 991` ``` by (force simp add: sigma_def inf_measure_agrees [OF posf ca]) ``` paulson@33271 ` 992` ```qed ``` paulson@33271 ` 993` paulson@33271 ` 994` ```end ```