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