src/HOL/Probability/Measure.thy
 author hoelzl Tue Mar 22 18:53:05 2011 +0100 (2011-03-22) changeset 42066 6db76c88907a parent 42065 2b98b4c2e2f1 child 42067 66c8281349ec permissions -rw-r--r--
generalized Caratheodory from algebra to ring_of_sets
 hoelzl@40859 ` 1` ```(* Author: Lawrence C Paulson; Armin Heller, Johannes Hoelzl, TU Muenchen *) ``` paulson@33271 ` 2` paulson@33271 ` 3` ```theory Measure ``` hoelzl@38656 ` 4` ``` imports Caratheodory ``` paulson@33271 ` 5` ```begin ``` paulson@33271 ` 6` hoelzl@41689 ` 7` ```lemma measure_algebra_more[simp]: ``` hoelzl@41689 ` 8` ``` "\ space = A, sets = B, \ = algebra.more M \ \ measure := m \ = ``` hoelzl@41689 ` 9` ``` \ space = A, sets = B, \ = algebra.more (M \ measure := m \) \" ``` hoelzl@41689 ` 10` ``` by (cases M) simp ``` hoelzl@41689 ` 11` hoelzl@41689 ` 12` ```lemma measure_algebra_more_eq[simp]: ``` hoelzl@41689 ` 13` ``` "\X. measure \ space = T, sets = A, \ = algebra.more X \ = measure X" ``` hoelzl@41689 ` 14` ``` unfolding measure_space.splits by simp ``` hoelzl@41689 ` 15` hoelzl@41689 ` 16` ```lemma measure_sigma[simp]: "measure (sigma A) = measure A" ``` hoelzl@41689 ` 17` ``` unfolding sigma_def by simp ``` hoelzl@41689 ` 18` hoelzl@41831 ` 19` ```lemma algebra_measure_update[simp]: ``` hoelzl@41831 ` 20` ``` "algebra (M'\measure := m\) \ algebra M'" ``` hoelzl@42065 ` 21` ``` unfolding algebra_iff_Un by simp ``` hoelzl@41831 ` 22` hoelzl@41831 ` 23` ```lemma sigma_algebra_measure_update[simp]: ``` hoelzl@41831 ` 24` ``` "sigma_algebra (M'\measure := m\) \ sigma_algebra M'" ``` hoelzl@41831 ` 25` ``` unfolding sigma_algebra_def sigma_algebra_axioms_def by simp ``` hoelzl@41831 ` 26` hoelzl@41831 ` 27` ```lemma finite_sigma_algebra_measure_update[simp]: ``` hoelzl@41831 ` 28` ``` "finite_sigma_algebra (M'\measure := m\) \ finite_sigma_algebra M'" ``` hoelzl@41831 ` 29` ``` unfolding finite_sigma_algebra_def finite_sigma_algebra_axioms_def by simp ``` hoelzl@41831 ` 30` hoelzl@41831 ` 31` ```lemma measurable_cancel_measure[simp]: ``` hoelzl@41831 ` 32` ``` "measurable M1 (M2\measure := m2\) = measurable M1 M2" ``` hoelzl@41831 ` 33` ``` "measurable (M2\measure := m1\) M1 = measurable M2 M1" ``` hoelzl@41831 ` 34` ``` unfolding measurable_def by auto ``` hoelzl@41831 ` 35` hoelzl@40859 ` 36` ```lemma inj_on_image_eq_iff: ``` hoelzl@40859 ` 37` ``` assumes "inj_on f S" ``` hoelzl@40859 ` 38` ``` assumes "A \ S" "B \ S" ``` hoelzl@40859 ` 39` ``` shows "(f ` A = f ` B) \ (A = B)" ``` hoelzl@40859 ` 40` ```proof - ``` hoelzl@40859 ` 41` ``` have "inj_on f (A \ B)" ``` hoelzl@40859 ` 42` ``` using assms by (auto intro: subset_inj_on) ``` hoelzl@40859 ` 43` ``` from inj_on_Un_image_eq_iff[OF this] ``` hoelzl@40859 ` 44` ``` show ?thesis . ``` hoelzl@40859 ` 45` ```qed ``` hoelzl@40859 ` 46` hoelzl@40859 ` 47` ```lemma image_vimage_inter_eq: ``` hoelzl@40859 ` 48` ``` assumes "f ` S = T" "X \ T" ``` hoelzl@40859 ` 49` ``` shows "f ` (f -` X \ S) = X" ``` hoelzl@40859 ` 50` ```proof (intro antisym) ``` hoelzl@40859 ` 51` ``` have "f ` (f -` X \ S) \ f ` (f -` X)" by auto ``` hoelzl@40859 ` 52` ``` also have "\ = X \ range f" by simp ``` hoelzl@40859 ` 53` ``` also have "\ = X" using assms by auto ``` hoelzl@40859 ` 54` ``` finally show "f ` (f -` X \ S) \ X" by auto ``` hoelzl@40859 ` 55` ```next ``` hoelzl@40859 ` 56` ``` show "X \ f ` (f -` X \ S)" ``` hoelzl@40859 ` 57` ``` proof ``` hoelzl@40859 ` 58` ``` fix x assume "x \ X" ``` hoelzl@40859 ` 59` ``` then have "x \ T" using `X \ T` by auto ``` hoelzl@40859 ` 60` ``` then obtain y where "x = f y" "y \ S" ``` hoelzl@40859 ` 61` ``` using assms by auto ``` hoelzl@40859 ` 62` ``` then have "{y} \ f -` X \ S" using `x \ X` by auto ``` hoelzl@40859 ` 63` ``` moreover have "x \ f ` {y}" using `x = f y` by auto ``` hoelzl@40859 ` 64` ``` ultimately show "x \ f ` (f -` X \ S)" by auto ``` hoelzl@40859 ` 65` ``` qed ``` hoelzl@40859 ` 66` ```qed ``` hoelzl@40859 ` 67` hoelzl@40859 ` 68` ```text {* ``` hoelzl@40859 ` 69` ``` This formalisation of measure theory is based on the work of Hurd/Coble wand ``` hoelzl@40859 ` 70` ``` was later translated by Lawrence Paulson to Isabelle/HOL. Later it was ``` hoelzl@40859 ` 71` ``` modified to use the positive infinite reals and to prove the uniqueness of ``` hoelzl@40859 ` 72` ``` cut stable measures. ``` hoelzl@40859 ` 73` ```*} ``` paulson@33271 ` 74` hoelzl@38656 ` 75` ```section {* Equations for the measure function @{text \} *} ``` paulson@33271 ` 76` hoelzl@38656 ` 77` ```lemma (in measure_space) measure_countably_additive: ``` hoelzl@38656 ` 78` ``` assumes "range A \ sets M" "disjoint_family A" ``` hoelzl@41981 ` 79` ``` shows "(\i. \ (A i)) = \ (\i. A i)" ``` paulson@33271 ` 80` ```proof - ``` hoelzl@38656 ` 81` ``` have "(\ i. A i) \ sets M" using assms(1) by (rule countable_UN) ``` hoelzl@38656 ` 82` ``` with ca assms show ?thesis by (simp add: countably_additive_def) ``` paulson@33271 ` 83` ```qed ``` paulson@33271 ` 84` hoelzl@41689 ` 85` ```lemma (in sigma_algebra) sigma_algebra_cong: ``` hoelzl@41689 ` 86` ``` assumes "space N = space M" "sets N = sets M" ``` hoelzl@41689 ` 87` ``` shows "sigma_algebra N" ``` hoelzl@41689 ` 88` ``` by default (insert sets_into_space, auto simp: assms) ``` hoelzl@41689 ` 89` hoelzl@38656 ` 90` ```lemma (in measure_space) measure_space_cong: ``` hoelzl@41689 ` 91` ``` assumes "\A. A \ sets M \ measure N A = \ A" "space N = space M" "sets N = sets M" ``` hoelzl@41689 ` 92` ``` shows "measure_space N" ``` hoelzl@41689 ` 93` ```proof - ``` hoelzl@41689 ` 94` ``` interpret N: sigma_algebra N by (intro sigma_algebra_cong assms) ``` hoelzl@41689 ` 95` ``` show ?thesis ``` hoelzl@41689 ` 96` ``` proof ``` hoelzl@41981 ` 97` ``` show "positive N (measure N)" using assms by (auto simp: positive_def) ``` hoelzl@41689 ` 98` ``` show "countably_additive N (measure N)" unfolding countably_additive_def ``` hoelzl@41689 ` 99` ``` proof safe ``` hoelzl@41689 ` 100` ``` fix A :: "nat \ 'a set" assume A: "range A \ sets N" "disjoint_family A" ``` hoelzl@41689 ` 101` ``` then have "\i. A i \ sets M" "(UNION UNIV A) \ sets M" unfolding assms by auto ``` hoelzl@41689 ` 102` ``` from measure_countably_additive[of A] A this[THEN assms(1)] ``` hoelzl@41981 ` 103` ``` show "(\n. measure N (A n)) = measure N (UNION UNIV A)" ``` hoelzl@41689 ` 104` ``` unfolding assms by simp ``` hoelzl@41689 ` 105` ``` qed ``` hoelzl@38656 ` 106` ``` qed ``` paulson@33271 ` 107` ```qed ``` paulson@33271 ` 108` hoelzl@38656 ` 109` ```lemma (in measure_space) additive: "additive M \" ``` hoelzl@42066 ` 110` ``` using ca by (auto intro!: countably_additive_additive simp: positive_def) ``` paulson@33271 ` 111` paulson@33271 ` 112` ```lemma (in measure_space) measure_additive: ``` hoelzl@38656 ` 113` ``` "a \ sets M \ b \ sets M \ a \ b = {} ``` hoelzl@38656 ` 114` ``` \ \ a + \ b = \ (a \ b)" ``` paulson@33271 ` 115` ``` by (metis additiveD additive) ``` paulson@33271 ` 116` hoelzl@36624 ` 117` ```lemma (in measure_space) measure_mono: ``` hoelzl@36624 ` 118` ``` assumes "a \ b" "a \ sets M" "b \ sets M" ``` hoelzl@38656 ` 119` ``` shows "\ a \ \ b" ``` hoelzl@36624 ` 120` ```proof - ``` hoelzl@36624 ` 121` ``` have "b = a \ (b - a)" using assms by auto ``` hoelzl@36624 ` 122` ``` moreover have "{} = a \ (b - a)" by auto ``` hoelzl@38656 ` 123` ``` ultimately have "\ b = \ a + \ (b - a)" ``` hoelzl@41981 ` 124` ``` using measure_additive[of a "b - a"] Diff[of b a] assms by auto ``` hoelzl@41981 ` 125` ``` moreover have "\ a + 0 \ \ a + \ (b - a)" using assms by (intro add_mono) auto ``` hoelzl@38656 ` 126` ``` ultimately show "\ a \ \ b" by auto ``` hoelzl@36624 ` 127` ```qed ``` hoelzl@36624 ` 128` hoelzl@38656 ` 129` ```lemma (in measure_space) measure_compl: ``` hoelzl@41981 ` 130` ``` assumes s: "s \ sets M" and fin: "\ s \ \" ``` hoelzl@38656 ` 131` ``` shows "\ (space M - s) = \ (space M) - \ s" ``` paulson@33271 ` 132` ```proof - ``` hoelzl@38656 ` 133` ``` have s_less_space: "\ s \ \ (space M)" ``` hoelzl@38656 ` 134` ``` using s by (auto intro!: measure_mono sets_into_space) ``` hoelzl@41981 ` 135` ``` from s have "0 \ \ s" by auto ``` hoelzl@38656 ` 136` ``` have "\ (space M) = \ (s \ (space M - s))" using s ``` hoelzl@38656 ` 137` ``` by (metis Un_Diff_cancel Un_absorb1 s sets_into_space) ``` hoelzl@38656 ` 138` ``` also have "... = \ s + \ (space M - s)" ``` hoelzl@38656 ` 139` ``` by (rule additiveD [OF additive]) (auto simp add: s) ``` hoelzl@38656 ` 140` ``` finally have "\ (space M) = \ s + \ (space M - s)" . ``` hoelzl@41981 ` 141` ``` then show ?thesis ``` hoelzl@41981 ` 142` ``` using fin `0 \ \ s` ``` hoelzl@41981 ` 143` ``` unfolding extreal_eq_minus_iff by (auto simp: ac_simps) ``` paulson@33271 ` 144` ```qed ``` paulson@33271 ` 145` hoelzl@38656 ` 146` ```lemma (in measure_space) measure_Diff: ``` hoelzl@41981 ` 147` ``` assumes finite: "\ B \ \" ``` hoelzl@38656 ` 148` ``` and measurable: "A \ sets M" "B \ sets M" "B \ A" ``` hoelzl@38656 ` 149` ``` shows "\ (A - B) = \ A - \ B" ``` hoelzl@38656 ` 150` ```proof - ``` hoelzl@41981 ` 151` ``` have "0 \ \ B" using assms by auto ``` hoelzl@41981 ` 152` ``` have "(A - B) \ B = A" using `B \ A` by auto ``` hoelzl@41981 ` 153` ``` then have "\ A = \ ((A - B) \ B)" by simp ``` hoelzl@41981 ` 154` ``` also have "\ = \ (A - B) + \ B" ``` hoelzl@41981 ` 155` ``` using measurable by (subst measure_additive[symmetric]) auto ``` hoelzl@41981 ` 156` ``` finally show "\ (A - B) = \ A - \ B" ``` hoelzl@41981 ` 157` ``` unfolding extreal_eq_minus_iff ``` hoelzl@41981 ` 158` ``` using finite `0 \ \ B` by auto ``` hoelzl@38656 ` 159` ```qed ``` paulson@33271 ` 160` paulson@33271 ` 161` ```lemma (in measure_space) measure_countable_increasing: ``` paulson@33271 ` 162` ``` assumes A: "range A \ sets M" ``` paulson@33271 ` 163` ``` and A0: "A 0 = {}" ``` hoelzl@41981 ` 164` ``` and ASuc: "\n. A n \ A (Suc n)" ``` hoelzl@38656 ` 165` ``` shows "(SUP n. \ (A n)) = \ (\i. A i)" ``` paulson@33271 ` 166` ```proof - ``` hoelzl@41981 ` 167` ``` { fix n ``` hoelzl@41981 ` 168` ``` have "\ (A n) = (\i (A (Suc i) - A i))" ``` paulson@33271 ` 169` ``` proof (induct n) ``` huffman@37032 ` 170` ``` case 0 thus ?case by (auto simp add: A0) ``` paulson@33271 ` 171` ``` next ``` hoelzl@38656 ` 172` ``` case (Suc m) ``` wenzelm@33536 ` 173` ``` have "A (Suc m) = A m \ (A (Suc m) - A m)" ``` wenzelm@33536 ` 174` ``` by (metis ASuc Un_Diff_cancel Un_absorb1) ``` hoelzl@38656 ` 175` ``` hence "\ (A (Suc m)) = ``` hoelzl@38656 ` 176` ``` \ (A m) + \ (A (Suc m) - A m)" ``` hoelzl@38656 ` 177` ``` by (subst measure_additive) ``` hoelzl@38656 ` 178` ``` (auto simp add: measure_additive range_subsetD [OF A]) ``` wenzelm@33536 ` 179` ``` with Suc show ?case ``` wenzelm@33536 ` 180` ``` by simp ``` hoelzl@38656 ` 181` ``` qed } ``` hoelzl@38656 ` 182` ``` note Meq = this ``` paulson@33271 ` 183` ``` have Aeq: "(\i. A (Suc i) - A i) = (\i. A i)" ``` hoelzl@38656 ` 184` ``` proof (rule UN_finite2_eq [where k=1], simp) ``` paulson@33271 ` 185` ``` fix i ``` paulson@33271 ` 186` ``` show "(\i\{0..i\{0..i. A (Suc i) - A i \ sets M" ``` paulson@33271 ` 196` ``` by (metis A Diff range_subsetD) ``` paulson@33271 ` 197` ``` have A2: "(\i. A (Suc i) - A i) \ sets M" ``` huffman@37032 ` 198` ``` by (blast intro: range_subsetD [OF A]) ``` hoelzl@41981 ` 199` ``` have "(SUP n. \i (A (Suc i) - A i)) = (\i. \ (A (Suc i) - A i))" ``` hoelzl@41981 ` 200` ``` using A by (auto intro!: suminf_extreal_eq_SUPR[symmetric]) ``` hoelzl@41981 ` 201` ``` also have "\ = \ (\i. A (Suc i) - A i)" ``` hoelzl@38656 ` 202` ``` by (rule measure_countably_additive) ``` paulson@33271 ` 203` ``` (auto simp add: disjoint_family_Suc ASuc A1 A2) ``` hoelzl@38656 ` 204` ``` also have "... = \ (\i. A i)" ``` hoelzl@38656 ` 205` ``` by (simp add: Aeq) ``` hoelzl@41981 ` 206` ``` finally have "(SUP n. \i (A (Suc i) - A i)) = \ (\i. A i)" . ``` hoelzl@41981 ` 207` ``` then show ?thesis by (auto simp add: Meq) ``` paulson@33271 ` 208` ```qed ``` paulson@33271 ` 209` hoelzl@38656 ` 210` ```lemma (in measure_space) continuity_from_below: ``` hoelzl@41981 ` 211` ``` assumes A: "range A \ sets M" and "incseq A" ``` hoelzl@38656 ` 212` ``` shows "(SUP n. \ (A n)) = \ (\i. A i)" ``` hoelzl@38656 ` 213` ```proof - ``` hoelzl@38656 ` 214` ``` have *: "(SUP n. \ (nat_case {} A (Suc n))) = (SUP n. \ (nat_case {} A n))" ``` hoelzl@41981 ` 215` ``` using A by (auto intro!: SUPR_eq exI split: nat.split) ``` hoelzl@38656 ` 216` ``` have ueq: "(\i. nat_case {} A i) = (\i. A i)" ``` hoelzl@38656 ` 217` ``` by (auto simp add: split: nat.splits) ``` hoelzl@38656 ` 218` ``` have meq: "\n. \ (A n) = (\ \ nat_case {} A) (Suc n)" ``` hoelzl@38656 ` 219` ``` by simp ``` hoelzl@38656 ` 220` ``` have "(SUP n. \ (nat_case {} A n)) = \ (\i. nat_case {} A i)" ``` hoelzl@41981 ` 221` ``` using range_subsetD[OF A] incseq_SucD[OF `incseq A`] ``` hoelzl@41981 ` 222` ``` by (force split: nat.splits intro!: measure_countable_increasing) ``` hoelzl@38656 ` 223` ``` also have "\ (\i. nat_case {} A i) = \ (\i. A i)" ``` hoelzl@38656 ` 224` ``` by (simp add: ueq) ``` hoelzl@38656 ` 225` ``` finally have "(SUP n. \ (nat_case {} A n)) = \ (\i. A i)" . ``` hoelzl@38656 ` 226` ``` thus ?thesis unfolding meq * comp_def . ``` paulson@33271 ` 227` ```qed ``` paulson@33271 ` 228` hoelzl@41981 ` 229` ```lemma (in measure_space) measure_incseq: ``` hoelzl@41981 ` 230` ``` assumes "range B \ sets M" "incseq B" ``` hoelzl@41981 ` 231` ``` shows "incseq (\i. \ (B i))" ``` hoelzl@41981 ` 232` ``` using assms by (auto simp: incseq_def intro!: measure_mono) ``` paulson@33271 ` 233` hoelzl@41981 ` 234` ```lemma (in measure_space) continuity_from_below_Lim: ``` hoelzl@41981 ` 235` ``` assumes A: "range A \ sets M" "incseq A" ``` hoelzl@41981 ` 236` ``` shows "(\i. (\ (A i))) ----> \ (\i. A i)" ``` hoelzl@41981 ` 237` ``` using LIMSEQ_extreal_SUPR[OF measure_incseq, OF A] ``` hoelzl@41981 ` 238` ``` continuity_from_below[OF A] by simp ``` hoelzl@41981 ` 239` hoelzl@41981 ` 240` ```lemma (in measure_space) measure_decseq: ``` hoelzl@41981 ` 241` ``` assumes "range B \ sets M" "decseq B" ``` hoelzl@41981 ` 242` ``` shows "decseq (\i. \ (B i))" ``` hoelzl@41981 ` 243` ``` using assms by (auto simp: decseq_def intro!: measure_mono) ``` paulson@33271 ` 244` hoelzl@38656 ` 245` ```lemma (in measure_space) continuity_from_above: ``` hoelzl@41981 ` 246` ``` assumes A: "range A \ sets M" and "decseq A" ``` hoelzl@41981 ` 247` ``` and finite: "\i. \ (A i) \ \" ``` hoelzl@38656 ` 248` ``` shows "(INF n. \ (A n)) = \ (\i. A i)" ``` paulson@33271 ` 249` ```proof - ``` hoelzl@38656 ` 250` ``` have le_MI: "\ (\i. A i) \ \ (A 0)" ``` hoelzl@38656 ` 251` ``` using A by (auto intro!: measure_mono) ``` hoelzl@41981 ` 252` ``` hence *: "\ (\i. A i) \ \" using finite[of 0] by auto ``` hoelzl@41981 ` 253` hoelzl@41981 ` 254` ``` have A0: "0 \ \ (A 0)" using A by auto ``` hoelzl@38656 ` 255` hoelzl@41981 ` 256` ``` have "\ (A 0) - (INF n. \ (A n)) = \ (A 0) + (SUP n. - \ (A n))" ``` hoelzl@41981 ` 257` ``` by (simp add: extreal_SUPR_uminus minus_extreal_def) ``` hoelzl@41981 ` 258` ``` also have "\ = (SUP n. \ (A 0) - \ (A n))" ``` hoelzl@41981 ` 259` ``` unfolding minus_extreal_def using A0 assms ``` hoelzl@41981 ` 260` ``` by (subst SUPR_extreal_add) (auto simp add: measure_decseq) ``` hoelzl@41981 ` 261` ``` also have "\ = (SUP n. \ (A 0 - A n))" ``` hoelzl@41981 ` 262` ``` using A finite `decseq A`[unfolded decseq_def] by (subst measure_Diff) auto ``` hoelzl@38656 ` 263` ``` also have "\ = \ (\i. A 0 - A i)" ``` hoelzl@38656 ` 264` ``` proof (rule continuity_from_below) ``` hoelzl@38656 ` 265` ``` show "range (\n. A 0 - A n) \ sets M" ``` hoelzl@38656 ` 266` ``` using A by auto ``` hoelzl@41981 ` 267` ``` show "incseq (\n. A 0 - A n)" ``` hoelzl@41981 ` 268` ``` using `decseq A` by (auto simp add: incseq_def decseq_def) ``` hoelzl@38656 ` 269` ``` qed ``` hoelzl@38656 ` 270` ``` also have "\ = \ (A 0) - \ (\i. A i)" ``` hoelzl@41981 ` 271` ``` using A finite * by (simp, subst measure_Diff) auto ``` hoelzl@38656 ` 272` ``` finally show ?thesis ``` hoelzl@41981 ` 273` ``` unfolding extreal_minus_eq_minus_iff using finite A0 by auto ``` paulson@33271 ` 274` ```qed ``` paulson@33271 ` 275` hoelzl@38656 ` 276` ```lemma (in measure_space) measure_insert: ``` hoelzl@38656 ` 277` ``` assumes sets: "{x} \ sets M" "A \ sets M" and "x \ A" ``` hoelzl@38656 ` 278` ``` shows "\ (insert x A) = \ {x} + \ A" ``` paulson@33271 ` 279` ```proof - ``` hoelzl@38656 ` 280` ``` have "{x} \ A = {}" using `x \ A` by auto ``` hoelzl@38656 ` 281` ``` from measure_additive[OF sets this] show ?thesis by simp ``` paulson@33271 ` 282` ```qed ``` paulson@33271 ` 283` hoelzl@41981 ` 284` ```lemma (in measure_space) measure_setsum: ``` hoelzl@41981 ` 285` ``` assumes "finite S" and "\i. i \ S \ A i \ sets M" ``` hoelzl@41981 ` 286` ``` assumes disj: "disjoint_family_on A S" ``` hoelzl@41981 ` 287` ``` shows "(\i\S. \ (A i)) = \ (\i\S. A i)" ``` hoelzl@38656 ` 288` ```using assms proof induct ``` hoelzl@41981 ` 289` ``` case (insert i S) ``` hoelzl@41981 ` 290` ``` then have "(\i\S. \ (A i)) = \ (\a\S. A a)" ``` hoelzl@41981 ` 291` ``` by (auto intro: disjoint_family_on_mono) ``` hoelzl@41981 ` 292` ``` moreover have "A i \ (\a\S. A a) = {}" ``` hoelzl@41981 ` 293` ``` using `disjoint_family_on A (insert i S)` `i \ S` ``` hoelzl@41981 ` 294` ``` by (auto simp: disjoint_family_on_def) ``` hoelzl@41981 ` 295` ``` ultimately show ?case using insert ``` hoelzl@41981 ` 296` ``` by (auto simp: measure_additive finite_UN) ``` hoelzl@38656 ` 297` ```qed simp ``` hoelzl@35582 ` 298` hoelzl@41981 ` 299` ```lemma (in measure_space) measure_finite_singleton: ``` hoelzl@41981 ` 300` ``` assumes "finite S" "\x. x \ S \ {x} \ sets M" ``` hoelzl@41981 ` 301` ``` shows "\ S = (\x\S. \ {x})" ``` hoelzl@41981 ` 302` ``` using measure_setsum[of S "\x. {x}", OF assms] ``` hoelzl@41981 ` 303` ``` by (auto simp: disjoint_family_on_def) ``` hoelzl@35582 ` 304` hoelzl@41689 ` 305` ```lemma finite_additivity_sufficient: ``` hoelzl@41689 ` 306` ``` assumes "sigma_algebra M" ``` hoelzl@41689 ` 307` ``` assumes fin: "finite (space M)" and pos: "positive M (measure M)" and add: "additive M (measure M)" ``` hoelzl@41689 ` 308` ``` shows "measure_space M" ``` hoelzl@41689 ` 309` ```proof - ``` hoelzl@41689 ` 310` ``` interpret sigma_algebra M by fact ``` hoelzl@41689 ` 311` ``` show ?thesis ``` hoelzl@41689 ` 312` ``` proof ``` hoelzl@41981 ` 313` ``` show [simp]: "positive M (measure M)" using pos by (simp add: positive_def) ``` hoelzl@41689 ` 314` ``` show "countably_additive M (measure M)" ``` hoelzl@38656 ` 315` ``` proof (auto simp add: countably_additive_def) ``` paulson@33271 ` 316` ``` fix A :: "nat \ 'a set" ``` hoelzl@38656 ` 317` ``` assume A: "range A \ sets M" ``` paulson@33271 ` 318` ``` and disj: "disjoint_family A" ``` hoelzl@38656 ` 319` ``` and UnA: "(\i. A i) \ sets M" ``` paulson@33271 ` 320` ``` def I \ "{i. A i \ {}}" ``` paulson@33271 ` 321` ``` have "Union (A ` I) \ space M" using A ``` hoelzl@38656 ` 322` ``` by auto (metis range_subsetD subsetD sets_into_space) ``` paulson@33271 ` 323` ``` hence "finite (A ` I)" ``` hoelzl@38656 ` 324` ``` by (metis finite_UnionD finite_subset fin) ``` paulson@33271 ` 325` ``` moreover have "inj_on A I" using disj ``` hoelzl@38656 ` 326` ``` by (auto simp add: I_def disjoint_family_on_def inj_on_def) ``` paulson@33271 ` 327` ``` ultimately have finI: "finite I" ``` paulson@33271 ` 328` ``` by (metis finite_imageD) ``` paulson@33271 ` 329` ``` hence "\N. \m\N. A m = {}" ``` paulson@33271 ` 330` ``` proof (cases "I = {}") ``` hoelzl@38656 ` 331` ``` case True thus ?thesis by (simp add: I_def) ``` paulson@33271 ` 332` ``` next ``` paulson@33271 ` 333` ``` case False ``` paulson@33271 ` 334` ``` hence "\i\I. i < Suc(Max I)" ``` hoelzl@38656 ` 335` ``` by (simp add: Max_less_iff [symmetric] finI) ``` paulson@33271 ` 336` ``` hence "\m \ Suc(Max I). A m = {}" ``` hoelzl@38656 ` 337` ``` by (simp add: I_def) (metis less_le_not_le) ``` paulson@33271 ` 338` ``` thus ?thesis ``` paulson@33271 ` 339` ``` by blast ``` paulson@33271 ` 340` ``` qed ``` paulson@33271 ` 341` ``` then obtain N where N: "\m\N. A m = {}" by blast ``` hoelzl@41981 ` 342` ``` then have "\m\N. measure M (A m) = 0" using pos[unfolded positive_def] by simp ``` hoelzl@41981 ` 343` ``` then have "(\n. measure M (A n)) = (\mi (\ x i (\ x sets M" using A ``` hoelzl@38656 ` 355` ``` by force ``` paulson@33271 ` 356` ``` show "(\i sets M" ``` paulson@33271 ` 357` ``` proof (induct n) ``` paulson@33271 ` 358` ``` case 0 thus ?case by simp ``` paulson@33271 ` 359` ``` next ``` paulson@33271 ` 360` ``` case (Suc n) thus ?case using A ``` hoelzl@38656 ` 361` ``` by (simp add: lessThan_Suc Un range_subsetD) ``` paulson@33271 ` 362` ``` qed ``` paulson@33271 ` 363` ``` qed ``` paulson@33271 ` 364` ``` thus ?case using Suc ``` hoelzl@38656 ` 365` ``` by (simp add: lessThan_Suc) ``` paulson@33271 ` 366` ``` qed ``` hoelzl@41689 ` 367` ``` also have "... = measure M (\i. A i)" ``` paulson@33271 ` 368` ``` proof - ``` paulson@33271 ` 369` ``` have "(\ ii. A i)" using N ``` paulson@33271 ` 370` ``` by auto (metis Int_absorb N disjoint_iff_not_equal lessThan_iff not_leE) ``` paulson@33271 ` 371` ``` thus ?thesis by simp ``` paulson@33271 ` 372` ``` qed ``` hoelzl@41981 ` 373` ``` finally show "(\n. measure M (A n)) = measure M (\i. A i)" . ``` paulson@33271 ` 374` ``` qed ``` hoelzl@41689 ` 375` ``` qed ``` paulson@33271 ` 376` ```qed ``` paulson@33271 ` 377` hoelzl@35692 ` 378` ```lemma (in measure_space) measure_setsum_split: ``` hoelzl@41981 ` 379` ``` assumes "finite S" and "A \ sets M" and br_in_M: "B ` S \ sets M" ``` hoelzl@41981 ` 380` ``` assumes "(\i\S. B i) = space M" ``` hoelzl@41981 ` 381` ``` assumes "disjoint_family_on B S" ``` hoelzl@41981 ` 382` ``` shows "\ A = (\i\S. \ (A \ (B i)))" ``` hoelzl@35692 ` 383` ```proof - ``` hoelzl@41981 ` 384` ``` have *: "\ A = \ (\i\S. A \ B i)" ``` hoelzl@35692 ` 385` ``` using assms by auto ``` hoelzl@35692 ` 386` ``` show ?thesis unfolding * ``` hoelzl@41981 ` 387` ``` proof (rule measure_setsum[symmetric]) ``` hoelzl@41981 ` 388` ``` show "disjoint_family_on (\i. A \ B i) S" ``` hoelzl@41981 ` 389` ``` using `disjoint_family_on B S` ``` hoelzl@35692 ` 390` ``` unfolding disjoint_family_on_def by auto ``` hoelzl@41981 ` 391` ``` qed (insert assms, auto) ``` hoelzl@35692 ` 392` ```qed ``` hoelzl@35692 ` 393` hoelzl@38656 ` 394` ```lemma (in measure_space) measure_subadditive: ``` hoelzl@38656 ` 395` ``` assumes measurable: "A \ sets M" "B \ sets M" ``` hoelzl@38656 ` 396` ``` shows "\ (A \ B) \ \ A + \ B" ``` hoelzl@38656 ` 397` ```proof - ``` hoelzl@38656 ` 398` ``` from measure_additive[of A "B - A"] ``` hoelzl@38656 ` 399` ``` have "\ (A \ B) = \ A + \ (B - A)" ``` hoelzl@38656 ` 400` ``` using assms by (simp add: Diff) ``` hoelzl@38656 ` 401` ``` also have "\ \ \ A + \ B" ``` hoelzl@38656 ` 402` ``` using assms by (auto intro!: add_left_mono measure_mono) ``` hoelzl@38656 ` 403` ``` finally show ?thesis . ``` hoelzl@38656 ` 404` ```qed ``` hoelzl@38656 ` 405` hoelzl@40859 ` 406` ```lemma (in measure_space) measure_eq_0: ``` hoelzl@40859 ` 407` ``` assumes "N \ sets M" and "\ N = 0" and "K \ N" and "K \ sets M" ``` hoelzl@40859 ` 408` ``` shows "\ K = 0" ``` hoelzl@41981 ` 409` ``` using measure_mono[OF assms(3,4,1)] assms(2) positive_measure[OF assms(4)] by auto ``` hoelzl@40859 ` 410` hoelzl@39092 ` 411` ```lemma (in measure_space) measure_finitely_subadditive: ``` hoelzl@39092 ` 412` ``` assumes "finite I" "A ` I \ sets M" ``` hoelzl@39092 ` 413` ``` shows "\ (\i\I. A i) \ (\i\I. \ (A i))" ``` hoelzl@39092 ` 414` ```using assms proof induct ``` hoelzl@39092 ` 415` ``` case (insert i I) ``` hoelzl@39092 ` 416` ``` then have "(\i\I. A i) \ sets M" by (auto intro: finite_UN) ``` hoelzl@39092 ` 417` ``` then have "\ (\i\insert i I. A i) \ \ (A i) + \ (\i\I. A i)" ``` hoelzl@39092 ` 418` ``` using insert by (simp add: measure_subadditive) ``` hoelzl@39092 ` 419` ``` also have "\ \ (\i\insert i I. \ (A i))" ``` hoelzl@39092 ` 420` ``` using insert by (auto intro!: add_left_mono) ``` hoelzl@39092 ` 421` ``` finally show ?case . ``` hoelzl@39092 ` 422` ```qed simp ``` hoelzl@39092 ` 423` hoelzl@40859 ` 424` ```lemma (in measure_space) measure_countably_subadditive: ``` hoelzl@38656 ` 425` ``` assumes "range f \ sets M" ``` hoelzl@41981 ` 426` ``` shows "\ (\i. f i) \ (\i. \ (f i))" ``` hoelzl@38656 ` 427` ```proof - ``` hoelzl@38656 ` 428` ``` have "\ (\i. f i) = \ (\i. disjointed f i)" ``` hoelzl@38656 ` 429` ``` unfolding UN_disjointed_eq .. ``` hoelzl@41981 ` 430` ``` also have "\ = (\i. \ (disjointed f i))" ``` hoelzl@38656 ` 431` ``` using range_disjointed_sets[OF assms] measure_countably_additive ``` hoelzl@38656 ` 432` ``` by (simp add: disjoint_family_disjointed comp_def) ``` hoelzl@41981 ` 433` ``` also have "\ \ (\i. \ (f i))" ``` hoelzl@41981 ` 434` ``` using range_disjointed_sets[OF assms] assms ``` hoelzl@41981 ` 435` ``` by (auto intro!: suminf_le_pos measure_mono positive_measure disjointed_subset) ``` hoelzl@38656 ` 436` ``` finally show ?thesis . ``` hoelzl@38656 ` 437` ```qed ``` hoelzl@38656 ` 438` hoelzl@40859 ` 439` ```lemma (in measure_space) measure_UN_eq_0: ``` hoelzl@41981 ` 440` ``` assumes "\i::nat. \ (N i) = 0" and "range N \ sets M" ``` hoelzl@40859 ` 441` ``` shows "\ (\ i. N i) = 0" ``` hoelzl@41981 ` 442` ```proof - ``` hoelzl@41981 ` 443` ``` have "0 \ \ (\ i. N i)" using assms by auto ``` hoelzl@41981 ` 444` ``` moreover have "\ (\ i. N i) \ 0" ``` hoelzl@41981 ` 445` ``` using measure_countably_subadditive[OF assms(2)] assms(1) by simp ``` hoelzl@41981 ` 446` ``` ultimately show ?thesis by simp ``` hoelzl@41981 ` 447` ```qed ``` hoelzl@40859 ` 448` hoelzl@39092 ` 449` ```lemma (in measure_space) measure_inter_full_set: ``` hoelzl@41981 ` 450` ``` assumes "S \ sets M" "T \ sets M" and fin: "\ (T - S) \ \" ``` hoelzl@39092 ` 451` ``` assumes T: "\ T = \ (space M)" ``` hoelzl@39092 ` 452` ``` shows "\ (S \ T) = \ S" ``` hoelzl@39092 ` 453` ```proof (rule antisym) ``` hoelzl@39092 ` 454` ``` show " \ (S \ T) \ \ S" ``` hoelzl@39092 ` 455` ``` using assms by (auto intro!: measure_mono) ``` hoelzl@39092 ` 456` hoelzl@41981 ` 457` ``` have pos: "0 \ \ (T - S)" using assms by auto ``` hoelzl@39092 ` 458` ``` show "\ S \ \ (S \ T)" ``` hoelzl@39092 ` 459` ``` proof (rule ccontr) ``` hoelzl@39092 ` 460` ``` assume contr: "\ ?thesis" ``` hoelzl@39092 ` 461` ``` have "\ (space M) = \ ((T - S) \ (S \ T))" ``` hoelzl@39092 ` 462` ``` unfolding T[symmetric] by (auto intro!: arg_cong[where f="\"]) ``` hoelzl@39092 ` 463` ``` also have "\ \ \ (T - S) + \ (S \ T)" ``` hoelzl@39092 ` 464` ``` using assms by (auto intro!: measure_subadditive) ``` hoelzl@39092 ` 465` ``` also have "\ < \ (T - S) + \ S" ``` hoelzl@41981 ` 466` ``` using fin contr pos by (intro extreal_less_add) auto ``` hoelzl@39092 ` 467` ``` also have "\ = \ (T \ S)" ``` hoelzl@39092 ` 468` ``` using assms by (subst measure_additive) auto ``` hoelzl@39092 ` 469` ``` also have "\ \ \ (space M)" ``` hoelzl@39092 ` 470` ``` using assms sets_into_space by (auto intro!: measure_mono) ``` hoelzl@39092 ` 471` ``` finally show False .. ``` hoelzl@39092 ` 472` ``` qed ``` hoelzl@39092 ` 473` ```qed ``` hoelzl@39092 ` 474` hoelzl@40859 ` 475` ```lemma measure_unique_Int_stable: ``` hoelzl@41689 ` 476` ``` fixes E :: "('a, 'b) algebra_scheme" and A :: "nat \ 'a set" ``` hoelzl@41689 ` 477` ``` assumes "Int_stable E" ``` hoelzl@41981 ` 478` ``` and A: "range A \ sets E" "incseq A" "(\i. A i) = space E" ``` hoelzl@41689 ` 479` ``` and M: "measure_space \space = space E, sets = sets (sigma E), measure = \\" (is "measure_space ?M") ``` hoelzl@41689 ` 480` ``` and N: "measure_space \space = space E, sets = sets (sigma E), measure = \\" (is "measure_space ?N") ``` hoelzl@40859 ` 481` ``` and eq: "\X. X \ sets E \ \ X = \ X" ``` hoelzl@41981 ` 482` ``` and finite: "\i. \ (A i) \ \" ``` hoelzl@41689 ` 483` ``` assumes "X \ sets (sigma E)" ``` hoelzl@40859 ` 484` ``` shows "\ X = \ X" ``` hoelzl@40859 ` 485` ```proof - ``` hoelzl@41689 ` 486` ``` let "?D F" = "{D. D \ sets (sigma E) \ \ (F \ D) = \ (F \ D)}" ``` hoelzl@41689 ` 487` ``` interpret M: measure_space ?M ``` hoelzl@41689 ` 488` ``` where "space ?M = space E" and "sets ?M = sets (sigma E)" and "measure ?M = \" by (simp_all add: M) ``` hoelzl@41689 ` 489` ``` interpret N: measure_space ?N ``` hoelzl@41689 ` 490` ``` where "space ?N = space E" and "sets ?N = sets (sigma E)" and "measure ?N = \" by (simp_all add: N) ``` hoelzl@41981 ` 491` ``` { fix F assume "F \ sets E" and "\ F \ \" ``` hoelzl@41689 ` 492` ``` then have [intro]: "F \ sets (sigma E)" by auto ``` hoelzl@41981 ` 493` ``` have "\ F \ \" using `\ F \ \` `F \ sets E` eq by simp ``` hoelzl@40859 ` 494` ``` interpret D: dynkin_system "\space=space E, sets=?D F\" ``` hoelzl@40859 ` 495` ``` proof (rule dynkin_systemI, simp_all) ``` hoelzl@41689 ` 496` ``` fix A assume "A \ sets (sigma E) \ \ (F \ A) = \ (F \ A)" ``` hoelzl@41689 ` 497` ``` then show "A \ space E" using M.sets_into_space by auto ``` hoelzl@40859 ` 498` ``` next ``` hoelzl@41689 ` 499` ``` have "F \ space E = F" using `F \ sets E` by auto ``` hoelzl@41689 ` 500` ``` then show "\ (F \ space E) = \ (F \ space E)" ``` hoelzl@41689 ` 501` ``` using `F \ sets E` eq by auto ``` hoelzl@40859 ` 502` ``` next ``` hoelzl@41689 ` 503` ``` fix A assume *: "A \ sets (sigma E) \ \ (F \ A) = \ (F \ A)" ``` hoelzl@41689 ` 504` ``` then have **: "F \ (space (sigma E) - A) = F - (F \ A)" ``` hoelzl@41689 ` 505` ``` and [intro]: "F \ A \ sets (sigma E)" ``` hoelzl@41689 ` 506` ``` using `F \ sets E` M.sets_into_space by auto ``` hoelzl@41689 ` 507` ``` have "\ (F \ A) \ \ F" by (auto intro!: N.measure_mono) ``` hoelzl@41981 ` 508` ``` then have "\ (F \ A) \ \" using `\ F \ \` by auto ``` hoelzl@40859 ` 509` ``` have "\ (F \ A) \ \ F" by (auto intro!: M.measure_mono) ``` hoelzl@41981 ` 510` ``` then have "\ (F \ A) \ \" using `\ F \ \` by auto ``` hoelzl@41689 ` 511` ``` then have "\ (F \ (space (sigma E) - A)) = \ F - \ (F \ A)" unfolding ** ``` hoelzl@41689 ` 512` ``` using `F \ A \ sets (sigma E)` by (auto intro!: M.measure_Diff) ``` hoelzl@40859 ` 513` ``` also have "\ = \ F - \ (F \ A)" using eq `F \ sets E` * by simp ``` hoelzl@41689 ` 514` ``` also have "\ = \ (F \ (space (sigma E) - A))" unfolding ** ``` hoelzl@41981 ` 515` ``` using `F \ A \ sets (sigma E)` `\ (F \ A) \ \` by (auto intro!: N.measure_Diff[symmetric]) ``` hoelzl@41689 ` 516` ``` finally show "space E - A \ sets (sigma E) \ \ (F \ (space E - A)) = \ (F \ (space E - A))" ``` hoelzl@41689 ` 517` ``` using * by auto ``` hoelzl@40859 ` 518` ``` next ``` hoelzl@40859 ` 519` ``` fix A :: "nat \ 'a set" ``` hoelzl@41689 ` 520` ``` assume "disjoint_family A" "range A \ {X \ sets (sigma E). \ (F \ X) = \ (F \ X)}" ``` hoelzl@41689 ` 521` ``` then have A: "range (\i. F \ A i) \ sets (sigma E)" "F \ (\x. A x) = (\x. F \ A x)" ``` hoelzl@41689 ` 522` ``` "disjoint_family (\i. F \ A i)" "\i. \ (F \ A i) = \ (F \ A i)" "range A \ sets (sigma E)" ``` hoelzl@41689 ` 523` ``` by (auto simp: disjoint_family_on_def subset_eq) ``` hoelzl@41689 ` 524` ``` then show "(\x. A x) \ sets (sigma E) \ \ (F \ (\x. A x)) = \ (F \ (\x. A x))" ``` hoelzl@40859 ` 525` ``` by (auto simp: M.measure_countably_additive[symmetric] ``` hoelzl@41689 ` 526` ``` N.measure_countably_additive[symmetric] ``` hoelzl@40859 ` 527` ``` simp del: UN_simps) ``` hoelzl@40859 ` 528` ``` qed ``` hoelzl@41689 ` 529` ``` have *: "sets (sigma E) = sets \space = space E, sets = ?D F\" ``` hoelzl@41689 ` 530` ``` using `F \ sets E` `Int_stable E` ``` hoelzl@40859 ` 531` ``` by (intro D.dynkin_lemma) ``` hoelzl@40859 ` 532` ``` (auto simp add: sets_sigma Int_stable_def eq intro: sigma_sets.Basic) ``` hoelzl@41689 ` 533` ``` have "\D. D \ sets (sigma E) \ \ (F \ D) = \ (F \ D)" ``` hoelzl@41689 ` 534` ``` by (subst (asm) *) auto } ``` hoelzl@40859 ` 535` ``` note * = this ``` hoelzl@41981 ` 536` ``` let "?A i" = "A i \ X" ``` hoelzl@41981 ` 537` ``` have A': "range ?A \ sets (sigma E)" "incseq ?A" ``` hoelzl@41981 ` 538` ``` using A(1,2) `X \ sets (sigma E)` by (auto simp: incseq_def) ``` hoelzl@41981 ` 539` ``` { fix i have "\ (?A i) = \ (?A i)" ``` hoelzl@41689 ` 540` ``` using *[of "A i" X] `X \ sets (sigma E)` A finite by auto } ``` hoelzl@41981 ` 541` ``` with M.continuity_from_below[OF A'] N.continuity_from_below[OF A'] ``` hoelzl@41981 ` 542` ``` show ?thesis using A(3) `X \ sets (sigma E)` by auto ``` hoelzl@40859 ` 543` ```qed ``` hoelzl@40859 ` 544` hoelzl@40859 ` 545` ```section "@{text \}-null sets" ``` hoelzl@40859 ` 546` hoelzl@40859 ` 547` ```abbreviation (in measure_space) "null_sets \ {N\sets M. \ N = 0}" ``` hoelzl@40859 ` 548` hoelzl@40859 ` 549` ```lemma (in measure_space) null_sets_Un[intro]: ``` hoelzl@40859 ` 550` ``` assumes "N \ null_sets" "N' \ null_sets" ``` hoelzl@40859 ` 551` ``` shows "N \ N' \ null_sets" ``` hoelzl@40859 ` 552` ```proof (intro conjI CollectI) ``` hoelzl@40859 ` 553` ``` show "N \ N' \ sets M" using assms by auto ``` hoelzl@41981 ` 554` ``` then have "0 \ \ (N \ N')" by simp ``` hoelzl@41981 ` 555` ``` moreover have "\ (N \ N') \ \ N + \ N'" ``` hoelzl@40859 ` 556` ``` using assms by (intro measure_subadditive) auto ``` hoelzl@41981 ` 557` ``` ultimately show "\ (N \ N') = 0" using assms by auto ``` hoelzl@40859 ` 558` ```qed ``` hoelzl@40859 ` 559` hoelzl@40859 ` 560` ```lemma UN_from_nat: "(\i. N i) = (\i. N (Countable.from_nat i))" ``` hoelzl@40859 ` 561` ```proof - ``` hoelzl@40859 ` 562` ``` have "(\i. N i) = (\i. (N \ Countable.from_nat) i)" ``` hoelzl@40859 ` 563` ``` unfolding SUPR_def image_compose ``` hoelzl@40859 ` 564` ``` unfolding surj_from_nat .. ``` hoelzl@40859 ` 565` ``` then show ?thesis by simp ``` hoelzl@40859 ` 566` ```qed ``` hoelzl@40859 ` 567` hoelzl@40859 ` 568` ```lemma (in measure_space) null_sets_UN[intro]: ``` hoelzl@40859 ` 569` ``` assumes "\i::'i::countable. N i \ null_sets" ``` hoelzl@40859 ` 570` ``` shows "(\i. N i) \ null_sets" ``` hoelzl@40859 ` 571` ```proof (intro conjI CollectI) ``` hoelzl@40859 ` 572` ``` show "(\i. N i) \ sets M" using assms by auto ``` hoelzl@41981 ` 573` ``` then have "0 \ \ (\i. N i)" by simp ``` hoelzl@41981 ` 574` ``` moreover have "\ (\i. N i) \ (\n. \ (N (Countable.from_nat n)))" ``` hoelzl@40859 ` 575` ``` unfolding UN_from_nat[of N] ``` hoelzl@40859 ` 576` ``` using assms by (intro measure_countably_subadditive) auto ``` hoelzl@41981 ` 577` ``` ultimately show "\ (\i. N i) = 0" using assms by auto ``` hoelzl@40859 ` 578` ```qed ``` hoelzl@40859 ` 579` hoelzl@40871 ` 580` ```lemma (in measure_space) null_sets_finite_UN: ``` hoelzl@40871 ` 581` ``` assumes "finite S" "\i. i \ S \ A i \ null_sets" ``` hoelzl@40871 ` 582` ``` shows "(\i\S. A i) \ null_sets" ``` hoelzl@40871 ` 583` ```proof (intro CollectI conjI) ``` hoelzl@40871 ` 584` ``` show "(\i\S. A i) \ sets M" using assms by (intro finite_UN) auto ``` hoelzl@41981 ` 585` ``` then have "0 \ \ (\i\S. A i)" by simp ``` hoelzl@41981 ` 586` ``` moreover have "\ (\i\S. A i) \ (\i\S. \ (A i))" ``` hoelzl@40871 ` 587` ``` using assms by (intro measure_finitely_subadditive) auto ``` hoelzl@41981 ` 588` ``` ultimately show "\ (\i\S. A i) = 0" using assms by auto ``` hoelzl@40871 ` 589` ```qed ``` hoelzl@40871 ` 590` hoelzl@40859 ` 591` ```lemma (in measure_space) null_set_Int1: ``` hoelzl@40859 ` 592` ``` assumes "B \ null_sets" "A \ sets M" shows "A \ B \ null_sets" ``` hoelzl@40859 ` 593` ```using assms proof (intro CollectI conjI) ``` hoelzl@40859 ` 594` ``` show "\ (A \ B) = 0" using assms by (intro measure_eq_0[of B "A \ B"]) auto ``` hoelzl@40859 ` 595` ```qed auto ``` hoelzl@40859 ` 596` hoelzl@40859 ` 597` ```lemma (in measure_space) null_set_Int2: ``` hoelzl@40859 ` 598` ``` assumes "B \ null_sets" "A \ sets M" shows "B \ A \ null_sets" ``` hoelzl@40859 ` 599` ``` using assms by (subst Int_commute) (rule null_set_Int1) ``` hoelzl@40859 ` 600` hoelzl@40859 ` 601` ```lemma (in measure_space) measure_Diff_null_set: ``` hoelzl@40859 ` 602` ``` assumes "B \ null_sets" "A \ sets M" ``` hoelzl@40859 ` 603` ``` shows "\ (A - B) = \ A" ``` hoelzl@40859 ` 604` ```proof - ``` hoelzl@40859 ` 605` ``` have *: "A - B = (A - (A \ B))" by auto ``` hoelzl@40859 ` 606` ``` have "A \ B \ null_sets" using assms by (rule null_set_Int1) ``` hoelzl@40859 ` 607` ``` then show ?thesis ``` hoelzl@40859 ` 608` ``` unfolding * using assms ``` hoelzl@40859 ` 609` ``` by (subst measure_Diff) auto ``` hoelzl@40859 ` 610` ```qed ``` hoelzl@40859 ` 611` hoelzl@40859 ` 612` ```lemma (in measure_space) null_set_Diff: ``` hoelzl@40859 ` 613` ``` assumes "B \ null_sets" "A \ sets M" shows "B - A \ null_sets" ``` hoelzl@40859 ` 614` ```using assms proof (intro CollectI conjI) ``` hoelzl@40859 ` 615` ``` show "\ (B - A) = 0" using assms by (intro measure_eq_0[of B "B - A"]) auto ``` hoelzl@40859 ` 616` ```qed auto ``` hoelzl@40859 ` 617` hoelzl@40859 ` 618` ```lemma (in measure_space) measure_Un_null_set: ``` hoelzl@40859 ` 619` ``` assumes "A \ sets M" "B \ null_sets" ``` hoelzl@40859 ` 620` ``` shows "\ (A \ B) = \ A" ``` hoelzl@40859 ` 621` ```proof - ``` hoelzl@40859 ` 622` ``` have *: "A \ B = A \ (B - A)" by auto ``` hoelzl@40859 ` 623` ``` have "B - A \ null_sets" using assms(2,1) by (rule null_set_Diff) ``` hoelzl@40859 ` 624` ``` then show ?thesis ``` hoelzl@40859 ` 625` ``` unfolding * using assms ``` hoelzl@40859 ` 626` ``` by (subst measure_additive[symmetric]) auto ``` hoelzl@40859 ` 627` ```qed ``` hoelzl@40859 ` 628` hoelzl@40871 ` 629` ```section "Formalise almost everywhere" ``` hoelzl@40871 ` 630` hoelzl@40871 ` 631` ```definition (in measure_space) ``` hoelzl@40871 ` 632` ``` almost_everywhere :: "('a \ bool) \ bool" (binder "AE " 10) where ``` hoelzl@40871 ` 633` ``` "almost_everywhere P \ (\N\null_sets. { x \ space M. \ P x } \ N)" ``` hoelzl@40871 ` 634` hoelzl@41981 ` 635` ```syntax ``` hoelzl@41981 ` 636` ``` "_almost_everywhere" :: "'a \ ('a, 'b) measure_space_scheme \ ('a \ bool) \ bool" ("AE _ in _. _" [0,0,10] 10) ``` hoelzl@41981 ` 637` hoelzl@41981 ` 638` ```translations ``` hoelzl@41981 ` 639` ``` "AE x in M. P" == "CONST measure_space.almost_everywhere M (%x. P)" ``` hoelzl@41981 ` 640` hoelzl@41981 ` 641` ```lemma (in measure_space) AE_cong_measure: ``` hoelzl@41981 ` 642` ``` assumes "\A. A \ sets M \ measure N A = \ A" "sets N = sets M" "space N = space M" ``` hoelzl@41981 ` 643` ``` shows "(AE x in N. P x) \ (AE x. P x)" ``` hoelzl@41981 ` 644` ```proof - ``` hoelzl@41981 ` 645` ``` interpret N: measure_space N ``` hoelzl@41981 ` 646` ``` by (rule measure_space_cong) fact+ ``` hoelzl@41981 ` 647` ``` show ?thesis ``` hoelzl@41981 ` 648` ``` unfolding N.almost_everywhere_def almost_everywhere_def ``` hoelzl@41981 ` 649` ``` by (auto simp: assms) ``` hoelzl@41981 ` 650` ```qed ``` hoelzl@41981 ` 651` hoelzl@40871 ` 652` ```lemma (in measure_space) AE_I': ``` hoelzl@40871 ` 653` ``` "N \ null_sets \ {x\space M. \ P x} \ N \ (AE x. P x)" ``` hoelzl@40871 ` 654` ``` unfolding almost_everywhere_def by auto ``` hoelzl@40871 ` 655` hoelzl@40871 ` 656` ```lemma (in measure_space) AE_iff_null_set: ``` hoelzl@40871 ` 657` ``` assumes "{x\space M. \ P x} \ sets M" (is "?P \ sets M") ``` hoelzl@40871 ` 658` ``` shows "(AE x. P x) \ {x\space M. \ P x} \ null_sets" ``` hoelzl@40871 ` 659` ```proof ``` hoelzl@40871 ` 660` ``` assume "AE x. P x" then obtain N where N: "N \ sets M" "?P \ N" "\ N = 0" ``` hoelzl@40871 ` 661` ``` unfolding almost_everywhere_def by auto ``` hoelzl@41981 ` 662` ``` have "0 \ \ ?P" using assms by simp ``` hoelzl@40871 ` 663` ``` moreover have "\ ?P \ \ N" ``` hoelzl@40871 ` 664` ``` using assms N(1,2) by (auto intro: measure_mono) ``` hoelzl@41981 ` 665` ``` ultimately have "\ ?P = 0" unfolding `\ N = 0` by auto ``` hoelzl@41981 ` 666` ``` then show "?P \ null_sets" using assms by simp ``` hoelzl@40871 ` 667` ```next ``` hoelzl@40871 ` 668` ``` assume "?P \ null_sets" with assms show "AE x. P x" by (auto intro: AE_I') ``` hoelzl@40871 ` 669` ```qed ``` hoelzl@40871 ` 670` hoelzl@41981 ` 671` ```lemma (in measure_space) AE_iff_measurable: ``` hoelzl@41981 ` 672` ``` "N \ sets M \ {x\space M. \ P x} = N \ (AE x. P x) \ \ N = 0" ``` hoelzl@41981 ` 673` ``` using AE_iff_null_set[of P] by simp ``` hoelzl@41981 ` 674` hoelzl@40859 ` 675` ```lemma (in measure_space) AE_True[intro, simp]: "AE x. True" ``` hoelzl@40859 ` 676` ``` unfolding almost_everywhere_def by auto ``` hoelzl@40859 ` 677` hoelzl@40859 ` 678` ```lemma (in measure_space) AE_E[consumes 1]: ``` hoelzl@40859 ` 679` ``` assumes "AE x. P x" ``` hoelzl@40859 ` 680` ``` obtains N where "{x \ space M. \ P x} \ N" "\ N = 0" "N \ sets M" ``` hoelzl@40859 ` 681` ``` using assms unfolding almost_everywhere_def by auto ``` hoelzl@40859 ` 682` hoelzl@41705 ` 683` ```lemma (in measure_space) AE_E2: ``` hoelzl@41705 ` 684` ``` assumes "AE x. P x" "{x\space M. P x} \ sets M" ``` hoelzl@41705 ` 685` ``` shows "\ {x\space M. \ P x} = 0" (is "\ ?P = 0") ``` hoelzl@41705 ` 686` ```proof - ``` hoelzl@41981 ` 687` ``` have "{x\space M. \ P x} = space M - {x\space M. P x}" ``` hoelzl@41981 ` 688` ``` by auto ``` hoelzl@41981 ` 689` ``` with AE_iff_null_set[of P] assms show ?thesis by auto ``` hoelzl@41705 ` 690` ```qed ``` hoelzl@41705 ` 691` hoelzl@40859 ` 692` ```lemma (in measure_space) AE_I: ``` hoelzl@40859 ` 693` ``` assumes "{x \ space M. \ P x} \ N" "\ N = 0" "N \ sets M" ``` hoelzl@40859 ` 694` ``` shows "AE x. P x" ``` hoelzl@40859 ` 695` ``` using assms unfolding almost_everywhere_def by auto ``` hoelzl@40859 ` 696` hoelzl@41705 ` 697` ```lemma (in measure_space) AE_mp[elim!]: ``` hoelzl@40859 ` 698` ``` assumes AE_P: "AE x. P x" and AE_imp: "AE x. P x \ Q x" ``` hoelzl@40859 ` 699` ``` shows "AE x. Q x" ``` hoelzl@40859 ` 700` ```proof - ``` hoelzl@40859 ` 701` ``` from AE_P obtain A where P: "{x\space M. \ P x} \ A" ``` hoelzl@40859 ` 702` ``` and A: "A \ sets M" "\ A = 0" ``` hoelzl@40859 ` 703` ``` by (auto elim!: AE_E) ``` hoelzl@40859 ` 704` hoelzl@40859 ` 705` ``` from AE_imp obtain B where imp: "{x\space M. P x \ \ Q x} \ B" ``` hoelzl@40859 ` 706` ``` and B: "B \ sets M" "\ B = 0" ``` hoelzl@40859 ` 707` ``` by (auto elim!: AE_E) ``` hoelzl@40859 ` 708` hoelzl@40859 ` 709` ``` show ?thesis ``` hoelzl@40859 ` 710` ``` proof (intro AE_I) ``` hoelzl@41981 ` 711` ``` have "0 \ \ (A \ B)" using A B by auto ``` hoelzl@41981 ` 712` ``` moreover have "\ (A \ B) \ 0" ``` hoelzl@41981 ` 713` ``` using measure_subadditive[of A B] A B by auto ``` hoelzl@41981 ` 714` ``` ultimately show "A \ B \ sets M" "\ (A \ B) = 0" using A B by auto ``` hoelzl@40859 ` 715` ``` show "{x\space M. \ Q x} \ A \ B" ``` hoelzl@40859 ` 716` ``` using P imp by auto ``` hoelzl@40859 ` 717` ``` qed ``` hoelzl@40859 ` 718` ```qed ``` hoelzl@40859 ` 719` hoelzl@41705 ` 720` ```lemma (in measure_space) ``` hoelzl@41705 ` 721` ``` shows AE_iffI: "AE x. P x \ AE x. P x \ Q x \ AE x. Q x" ``` hoelzl@41705 ` 722` ``` and AE_disjI1: "AE x. P x \ AE x. P x \ Q x" ``` hoelzl@41705 ` 723` ``` and AE_disjI2: "AE x. Q x \ AE x. P x \ Q x" ``` hoelzl@41705 ` 724` ``` and AE_conjI: "AE x. P x \ AE x. Q x \ AE x. P x \ Q x" ``` hoelzl@41705 ` 725` ``` and AE_conj_iff[simp]: "(AE x. P x \ Q x) \ (AE x. P x) \ (AE x. Q x)" ``` hoelzl@41705 ` 726` ``` by auto ``` hoelzl@40859 ` 727` hoelzl@41705 ` 728` ```lemma (in measure_space) AE_space: "AE x. x \ space M" ``` hoelzl@40859 ` 729` ``` by (rule AE_I[where N="{}"]) auto ``` hoelzl@40859 ` 730` hoelzl@41705 ` 731` ```lemma (in measure_space) AE_I2[simp, intro]: ``` hoelzl@41705 ` 732` ``` "(\x. x \ space M \ P x) \ AE x. P x" ``` hoelzl@41705 ` 733` ``` using AE_space by auto ``` hoelzl@41705 ` 734` hoelzl@41705 ` 735` ```lemma (in measure_space) AE_Ball_mp: ``` hoelzl@41705 ` 736` ``` "\x\space M. P x \ AE x. P x \ Q x \ AE x. Q x" ``` hoelzl@41705 ` 737` ``` by auto ``` hoelzl@41705 ` 738` hoelzl@41705 ` 739` ```lemma (in measure_space) AE_cong[cong]: ``` hoelzl@41705 ` 740` ``` "(\x. x \ space M \ P x \ Q x) \ (AE x. P x) \ (AE x. Q x)" ``` hoelzl@41705 ` 741` ``` by auto ``` hoelzl@40859 ` 742` hoelzl@41981 ` 743` ```lemma (in measure_space) AE_all_countable: ``` hoelzl@41981 ` 744` ``` "(AE x. \i. P i x) \ (\i::'i::countable. AE x. P i x)" ``` hoelzl@40859 ` 745` ```proof ``` hoelzl@40859 ` 746` ``` assume "\i. AE x. P i x" ``` hoelzl@40859 ` 747` ``` from this[unfolded almost_everywhere_def Bex_def, THEN choice] ``` hoelzl@40859 ` 748` ``` obtain N where N: "\i. N i \ null_sets" "\i. {x\space M. \ P i x} \ N i" by auto ``` hoelzl@40859 ` 749` ``` have "{x\space M. \ (\i. P i x)} \ (\i. {x\space M. \ P i x})" by auto ``` hoelzl@40859 ` 750` ``` also have "\ \ (\i. N i)" using N by auto ``` hoelzl@40859 ` 751` ``` finally have "{x\space M. \ (\i. P i x)} \ (\i. N i)" . ``` hoelzl@40859 ` 752` ``` moreover from N have "(\i. N i) \ null_sets" ``` hoelzl@40859 ` 753` ``` by (intro null_sets_UN) auto ``` hoelzl@40859 ` 754` ``` ultimately show "AE x. \i. P i x" ``` hoelzl@40859 ` 755` ``` unfolding almost_everywhere_def by auto ``` hoelzl@41705 ` 756` ```qed auto ``` hoelzl@40859 ` 757` hoelzl@41981 ` 758` ```lemma (in measure_space) AE_finite_all: ``` hoelzl@41981 ` 759` ``` assumes f: "finite S" shows "(AE x. \i\S. P i x) \ (\i\S. AE x. P i x)" ``` hoelzl@41981 ` 760` ``` using f by induct auto ``` hoelzl@41981 ` 761` hoelzl@38656 ` 762` ```lemma (in measure_space) restricted_measure_space: ``` hoelzl@38656 ` 763` ``` assumes "S \ sets M" ``` hoelzl@41689 ` 764` ``` shows "measure_space (restricted_space S)" ``` hoelzl@41689 ` 765` ``` (is "measure_space ?r") ``` hoelzl@38656 ` 766` ``` unfolding measure_space_def measure_space_axioms_def ``` hoelzl@38656 ` 767` ```proof safe ``` hoelzl@38656 ` 768` ``` show "sigma_algebra ?r" using restricted_sigma_algebra[OF assms] . ``` hoelzl@41981 ` 769` ``` show "positive ?r (measure ?r)" using `S \ sets M` by (auto simp: positive_def) ``` hoelzl@41689 ` 770` hoelzl@41689 ` 771` ``` show "countably_additive ?r (measure ?r)" ``` hoelzl@38656 ` 772` ``` unfolding countably_additive_def ``` hoelzl@38656 ` 773` ``` proof safe ``` hoelzl@38656 ` 774` ``` fix A :: "nat \ 'a set" ``` hoelzl@38656 ` 775` ``` assume *: "range A \ sets ?r" and **: "disjoint_family A" ``` hoelzl@38656 ` 776` ``` from restriction_in_sets[OF assms *[simplified]] ** ``` hoelzl@41981 ` 777` ``` show "(\n. measure ?r (A n)) = measure ?r (\i. A i)" ``` hoelzl@38656 ` 778` ``` using measure_countably_additive by simp ``` hoelzl@38656 ` 779` ``` qed ``` hoelzl@38656 ` 780` ```qed ``` hoelzl@38656 ` 781` hoelzl@41981 ` 782` ```lemma (in measure_space) AE_restricted: ``` hoelzl@41981 ` 783` ``` assumes "A \ sets M" ``` hoelzl@41981 ` 784` ``` shows "(AE x in restricted_space A. P x) \ (AE x. x \ A \ P x)" ``` hoelzl@41981 ` 785` ```proof - ``` hoelzl@41981 ` 786` ``` interpret R: measure_space "restricted_space A" ``` hoelzl@41981 ` 787` ``` by (rule restricted_measure_space[OF `A \ sets M`]) ``` hoelzl@41981 ` 788` ``` show ?thesis ``` hoelzl@41981 ` 789` ``` proof ``` hoelzl@41981 ` 790` ``` assume "AE x in restricted_space A. P x" ``` hoelzl@41981 ` 791` ``` from this[THEN R.AE_E] guess N' . ``` hoelzl@41981 ` 792` ``` then obtain N where "{x \ A. \ P x} \ A \ N" "\ (A \ N) = 0" "N \ sets M" ``` hoelzl@41981 ` 793` ``` by auto ``` hoelzl@41981 ` 794` ``` moreover then have "{x \ space M. \ (x \ A \ P x)} \ A \ N" ``` hoelzl@41981 ` 795` ``` using `A \ sets M` sets_into_space by auto ``` hoelzl@41981 ` 796` ``` ultimately show "AE x. x \ A \ P x" ``` hoelzl@41981 ` 797` ``` using `A \ sets M` by (auto intro!: AE_I[where N="A \ N"]) ``` hoelzl@41981 ` 798` ``` next ``` hoelzl@41981 ` 799` ``` assume "AE x. x \ A \ P x" ``` hoelzl@41981 ` 800` ``` from this[THEN AE_E] guess N . ``` hoelzl@41981 ` 801` ``` then show "AE x in restricted_space A. P x" ``` hoelzl@41981 ` 802` ``` using null_set_Int1[OF _ `A \ sets M`] `A \ sets M`[THEN sets_into_space] ``` hoelzl@41981 ` 803` ``` by (auto intro!: R.AE_I[where N="A \ N"] simp: subset_eq) ``` hoelzl@41981 ` 804` ``` qed ``` hoelzl@41981 ` 805` ```qed ``` hoelzl@41981 ` 806` hoelzl@39092 ` 807` ```lemma (in measure_space) measure_space_subalgebra: ``` hoelzl@41981 ` 808` ``` assumes "sigma_algebra N" and "sets N \ sets M" "space N = space M" ``` hoelzl@41689 ` 809` ``` and measure[simp]: "\X. X \ sets N \ measure N X = measure M X" ``` hoelzl@41689 ` 810` ``` shows "measure_space N" ``` hoelzl@39092 ` 811` ```proof - ``` hoelzl@41545 ` 812` ``` interpret N: sigma_algebra N by fact ``` hoelzl@39092 ` 813` ``` show ?thesis ``` hoelzl@39092 ` 814` ``` proof ``` hoelzl@41545 ` 815` ``` from `sets N \ sets M` have "\A. range A \ sets N \ range A \ sets M" by blast ``` hoelzl@41689 ` 816` ``` then show "countably_additive N (measure N)" ``` hoelzl@41689 ` 817` ``` by (auto intro!: measure_countably_additive simp: countably_additive_def subset_eq) ``` hoelzl@41981 ` 818` ``` show "positive N (measure_space.measure N)" ``` hoelzl@41981 ` 819` ``` using assms(2) by (auto simp add: positive_def) ``` hoelzl@41981 ` 820` ``` qed ``` hoelzl@41981 ` 821` ```qed ``` hoelzl@41981 ` 822` hoelzl@41981 ` 823` ```lemma (in measure_space) AE_subalgebra: ``` hoelzl@41981 ` 824` ``` assumes ae: "AE x in N. P x" ``` hoelzl@41981 ` 825` ``` and N: "sets N \ sets M" "space N = space M" "\A. A \ sets N \ measure N A = \ A" ``` hoelzl@41981 ` 826` ``` and sa: "sigma_algebra N" ``` hoelzl@41981 ` 827` ``` shows "AE x. P x" ``` hoelzl@41981 ` 828` ```proof - ``` hoelzl@41981 ` 829` ``` interpret N: measure_space N using measure_space_subalgebra[OF sa N] . ``` hoelzl@41981 ` 830` ``` from ae[THEN N.AE_E] guess N . ``` hoelzl@41981 ` 831` ``` with N show ?thesis unfolding almost_everywhere_def by auto ``` hoelzl@39092 ` 832` ```qed ``` hoelzl@39092 ` 833` hoelzl@38656 ` 834` ```section "@{text \}-finite Measures" ``` hoelzl@38656 ` 835` hoelzl@38656 ` 836` ```locale sigma_finite_measure = measure_space + ``` hoelzl@41981 ` 837` ``` assumes sigma_finite: "\A::nat \ 'a set. range A \ sets M \ (\i. A i) = space M \ (\i. \ (A i) \ \)" ``` hoelzl@38656 ` 838` hoelzl@38656 ` 839` ```lemma (in sigma_finite_measure) restricted_sigma_finite_measure: ``` hoelzl@38656 ` 840` ``` assumes "S \ sets M" ``` hoelzl@41689 ` 841` ``` shows "sigma_finite_measure (restricted_space S)" ``` hoelzl@41689 ` 842` ``` (is "sigma_finite_measure ?r") ``` hoelzl@38656 ` 843` ``` unfolding sigma_finite_measure_def sigma_finite_measure_axioms_def ``` hoelzl@38656 ` 844` ```proof safe ``` hoelzl@41689 ` 845` ``` show "measure_space ?r" using restricted_measure_space[OF assms] . ``` hoelzl@38656 ` 846` ```next ``` hoelzl@38656 ` 847` ``` obtain A :: "nat \ 'a set" where ``` hoelzl@41981 ` 848` ``` "range A \ sets M" "(\i. A i) = space M" "\i. \ (A i) \ \" ``` hoelzl@38656 ` 849` ``` using sigma_finite by auto ``` hoelzl@41981 ` 850` ``` show "\A::nat \ 'a set. range A \ sets ?r \ (\i. A i) = space ?r \ (\i. measure ?r (A i) \ \)" ``` hoelzl@38656 ` 851` ``` proof (safe intro!: exI[of _ "\i. A i \ S"] del: notI) ``` hoelzl@38656 ` 852` ``` fix i ``` hoelzl@38656 ` 853` ``` show "A i \ S \ sets ?r" ``` hoelzl@38656 ` 854` ``` using `range A \ sets M` `S \ sets M` by auto ``` hoelzl@38656 ` 855` ``` next ``` hoelzl@38656 ` 856` ``` fix x i assume "x \ S" thus "x \ space ?r" by simp ``` hoelzl@38656 ` 857` ``` next ``` hoelzl@38656 ` 858` ``` fix x assume "x \ space ?r" thus "x \ (\i. A i \ S)" ``` hoelzl@38656 ` 859` ``` using `(\i. A i) = space M` `S \ sets M` by auto ``` hoelzl@38656 ` 860` ``` next ``` hoelzl@38656 ` 861` ``` fix i ``` hoelzl@38656 ` 862` ``` have "\ (A i \ S) \ \ (A i)" ``` hoelzl@38656 ` 863` ``` using `range A \ sets M` `S \ sets M` by (auto intro!: measure_mono) ``` hoelzl@41981 ` 864` ``` then show "measure ?r (A i \ S) \ \" using `\ (A i) \ \` by auto ``` hoelzl@38656 ` 865` ``` qed ``` hoelzl@38656 ` 866` ```qed ``` hoelzl@38656 ` 867` hoelzl@40859 ` 868` ```lemma (in sigma_finite_measure) sigma_finite_measure_cong: ``` hoelzl@41689 ` 869` ``` assumes cong: "\A. A \ sets M \ measure M' A = \ A" "sets M' = sets M" "space M' = space M" ``` hoelzl@41689 ` 870` ``` shows "sigma_finite_measure M'" ``` hoelzl@40859 ` 871` ```proof - ``` hoelzl@41689 ` 872` ``` interpret M': measure_space M' by (intro measure_space_cong cong) ``` hoelzl@40859 ` 873` ``` from sigma_finite guess A .. note A = this ``` hoelzl@40859 ` 874` ``` then have "\i. A i \ sets M" by auto ``` hoelzl@41981 ` 875` ``` with A have fin: "\i. measure M' (A i) \ \" using cong by auto ``` hoelzl@40859 ` 876` ``` show ?thesis ``` hoelzl@40859 ` 877` ``` apply default ``` hoelzl@41689 ` 878` ``` using A fin cong by auto ``` hoelzl@40859 ` 879` ```qed ``` hoelzl@40859 ` 880` hoelzl@39092 ` 881` ```lemma (in sigma_finite_measure) disjoint_sigma_finite: ``` hoelzl@39092 ` 882` ``` "\A::nat\'a set. range A \ sets M \ (\i. A i) = space M \ ``` hoelzl@41981 ` 883` ``` (\i. \ (A i) \ \) \ disjoint_family A" ``` hoelzl@39092 ` 884` ```proof - ``` hoelzl@39092 ` 885` ``` obtain A :: "nat \ 'a set" where ``` hoelzl@39092 ` 886` ``` range: "range A \ sets M" and ``` hoelzl@39092 ` 887` ``` space: "(\i. A i) = space M" and ``` hoelzl@41981 ` 888` ``` measure: "\i. \ (A i) \ \" ``` hoelzl@39092 ` 889` ``` using sigma_finite by auto ``` hoelzl@39092 ` 890` ``` note range' = range_disjointed_sets[OF range] range ``` hoelzl@39092 ` 891` ``` { fix i ``` hoelzl@39092 ` 892` ``` have "\ (disjointed A i) \ \ (A i)" ``` hoelzl@39092 ` 893` ``` using range' disjointed_subset[of A i] by (auto intro!: measure_mono) ``` hoelzl@41981 ` 894` ``` then have "\ (disjointed A i) \ \" ``` hoelzl@39092 ` 895` ``` using measure[of i] by auto } ``` hoelzl@39092 ` 896` ``` with disjoint_family_disjointed UN_disjointed_eq[of A] space range' ``` hoelzl@39092 ` 897` ``` show ?thesis by (auto intro!: exI[of _ "disjointed A"]) ``` hoelzl@39092 ` 898` ```qed ``` hoelzl@39092 ` 899` hoelzl@40859 ` 900` ```lemma (in sigma_finite_measure) sigma_finite_up: ``` hoelzl@41981 ` 901` ``` "\F. range F \ sets M \ incseq F \ (\i. F i) = space M \ (\i. \ (F i) \ \)" ``` hoelzl@40859 ` 902` ```proof - ``` hoelzl@40859 ` 903` ``` obtain F :: "nat \ 'a set" where ``` hoelzl@41981 ` 904` ``` F: "range F \ sets M" "(\i. F i) = space M" "\i. \ (F i) \ \" ``` hoelzl@40859 ` 905` ``` using sigma_finite by auto ``` hoelzl@41981 ` 906` ``` then show ?thesis ``` hoelzl@40859 ` 907` ``` proof (intro exI[of _ "\n. \i\n. F i"] conjI allI) ``` hoelzl@40859 ` 908` ``` from F have "\x. x \ space M \ \i. x \ F i" by auto ``` hoelzl@40859 ` 909` ``` then show "(\n. \ i\n. F i) = space M" ``` hoelzl@40859 ` 910` ``` using F by fastsimp ``` hoelzl@40859 ` 911` ``` next ``` hoelzl@40859 ` 912` ``` fix n ``` hoelzl@40859 ` 913` ``` have "\ (\ i\n. F i) \ (\i\n. \ (F i))" using F ``` hoelzl@40859 ` 914` ``` by (auto intro!: measure_finitely_subadditive) ``` hoelzl@41981 ` 915` ``` also have "\ < \" ``` hoelzl@41981 ` 916` ``` using F by (auto simp: setsum_Pinfty) ``` hoelzl@41981 ` 917` ``` finally show "\ (\ i\n. F i) \ \" by simp ``` hoelzl@41981 ` 918` ``` qed (force simp: incseq_def)+ ``` hoelzl@40859 ` 919` ```qed ``` hoelzl@40859 ` 920` hoelzl@41831 ` 921` ```section {* Measure preserving *} ``` hoelzl@41831 ` 922` hoelzl@41831 ` 923` ```definition "measure_preserving A B = ``` hoelzl@41981 ` 924` ``` {f \ measurable A B. (\y \ sets B. measure B y = measure A (f -` y \ space A))}" ``` hoelzl@41831 ` 925` hoelzl@41831 ` 926` ```lemma measure_preservingI[intro?]: ``` hoelzl@41831 ` 927` ``` assumes "f \ measurable A B" ``` hoelzl@41831 ` 928` ``` and "\y. y \ sets B \ measure A (f -` y \ space A) = measure B y" ``` hoelzl@41831 ` 929` ``` shows "f \ measure_preserving A B" ``` hoelzl@41831 ` 930` ``` unfolding measure_preserving_def using assms by auto ``` hoelzl@41831 ` 931` hoelzl@41831 ` 932` ```lemma (in measure_space) measure_space_vimage: ``` hoelzl@41831 ` 933` ``` fixes M' :: "('c, 'd) measure_space_scheme" ``` hoelzl@41831 ` 934` ``` assumes T: "sigma_algebra M'" "T \ measure_preserving M M'" ``` hoelzl@41831 ` 935` ``` shows "measure_space M'" ``` hoelzl@41831 ` 936` ```proof - ``` hoelzl@41831 ` 937` ``` interpret M': sigma_algebra M' by fact ``` hoelzl@41831 ` 938` ``` show ?thesis ``` hoelzl@41831 ` 939` ``` proof ``` hoelzl@41981 ` 940` ``` show "positive M' (measure M')" using T ``` hoelzl@41981 ` 941` ``` by (auto simp: measure_preserving_def positive_def measurable_sets) ``` hoelzl@41831 ` 942` hoelzl@41831 ` 943` ``` show "countably_additive M' (measure M')" ``` hoelzl@41831 ` 944` ``` proof (intro countably_additiveI) ``` hoelzl@41831 ` 945` ``` fix A :: "nat \ 'c set" assume "range A \ sets M'" "disjoint_family A" ``` hoelzl@41831 ` 946` ``` then have A: "\i. A i \ sets M'" "(\i. A i) \ sets M'" by auto ``` hoelzl@41831 ` 947` ``` then have *: "range (\i. T -` (A i) \ space M) \ sets M" ``` hoelzl@41831 ` 948` ``` using T by (auto simp: measurable_def measure_preserving_def) ``` hoelzl@41831 ` 949` ``` moreover have "(\i. T -` A i \ space M) \ sets M" ``` hoelzl@41831 ` 950` ``` using * by blast ``` hoelzl@41831 ` 951` ``` moreover have **: "disjoint_family (\i. T -` A i \ space M)" ``` hoelzl@41831 ` 952` ``` using `disjoint_family A` by (auto simp: disjoint_family_on_def) ``` hoelzl@41981 ` 953` ``` ultimately show "(\i. measure M' (A i)) = measure M' (\i. A i)" ``` hoelzl@41831 ` 954` ``` using measure_countably_additive[OF _ **] A T ``` hoelzl@41831 ` 955` ``` by (auto simp: comp_def vimage_UN measure_preserving_def) ``` hoelzl@41831 ` 956` ``` qed ``` hoelzl@41831 ` 957` ``` qed ``` hoelzl@41831 ` 958` ```qed ``` hoelzl@41831 ` 959` hoelzl@41831 ` 960` ```lemma (in measure_space) almost_everywhere_vimage: ``` hoelzl@41831 ` 961` ``` assumes T: "sigma_algebra M'" "T \ measure_preserving M M'" ``` hoelzl@41831 ` 962` ``` and AE: "measure_space.almost_everywhere M' P" ``` hoelzl@41831 ` 963` ``` shows "AE x. P (T x)" ``` hoelzl@41831 ` 964` ```proof - ``` hoelzl@41831 ` 965` ``` interpret M': measure_space M' using T by (rule measure_space_vimage) ``` hoelzl@41831 ` 966` ``` from AE[THEN M'.AE_E] guess N . ``` hoelzl@41831 ` 967` ``` then show ?thesis ``` hoelzl@41831 ` 968` ``` unfolding almost_everywhere_def M'.almost_everywhere_def ``` hoelzl@41831 ` 969` ``` using T(2) unfolding measurable_def measure_preserving_def ``` hoelzl@41831 ` 970` ``` by (intro bexI[of _ "T -` N \ space M"]) auto ``` hoelzl@41831 ` 971` ```qed ``` hoelzl@41831 ` 972` hoelzl@41831 ` 973` ```lemma measure_unique_Int_stable_vimage: ``` hoelzl@41831 ` 974` ``` fixes A :: "nat \ 'a set" ``` hoelzl@41831 ` 975` ``` assumes E: "Int_stable E" ``` hoelzl@41981 ` 976` ``` and A: "range A \ sets E" "incseq A" "(\i. A i) = space E" "\i. measure M (A i) \ \" ``` hoelzl@41831 ` 977` ``` and N: "measure_space N" "T \ measurable N M" ``` hoelzl@41831 ` 978` ``` and M: "measure_space M" "sets (sigma E) = sets M" "space E = space M" ``` hoelzl@41831 ` 979` ``` and eq: "\X. X \ sets E \ measure M X = measure N (T -` X \ space N)" ``` hoelzl@41831 ` 980` ``` assumes X: "X \ sets (sigma E)" ``` hoelzl@41831 ` 981` ``` shows "measure M X = measure N (T -` X \ space N)" ``` hoelzl@41981 ` 982` ```proof (rule measure_unique_Int_stable[OF E A(1,2,3) _ _ eq _ X]) ``` hoelzl@41831 ` 983` ``` interpret M: measure_space M by fact ``` hoelzl@41831 ` 984` ``` interpret N: measure_space N by fact ``` hoelzl@41831 ` 985` ``` let "?T X" = "T -` X \ space N" ``` hoelzl@41831 ` 986` ``` show "measure_space \space = space E, sets = sets (sigma E), measure = measure M\" ``` hoelzl@41831 ` 987` ``` by (rule M.measure_space_cong) (auto simp: M) ``` hoelzl@41831 ` 988` ``` show "measure_space \space = space E, sets = sets (sigma E), measure = \X. measure N (?T X)\" (is "measure_space ?E") ``` hoelzl@41831 ` 989` ``` proof (rule N.measure_space_vimage) ``` hoelzl@41831 ` 990` ``` show "sigma_algebra ?E" ``` hoelzl@41831 ` 991` ``` by (rule M.sigma_algebra_cong) (auto simp: M) ``` hoelzl@41831 ` 992` ``` show "T \ measure_preserving N ?E" ``` hoelzl@41831 ` 993` ``` using `T \ measurable N M` by (auto simp: M measurable_def measure_preserving_def) ``` hoelzl@41831 ` 994` ``` qed ``` hoelzl@41981 ` 995` ``` show "\i. M.\ (A i) \ \" by fact ``` hoelzl@41831 ` 996` ```qed ``` hoelzl@41831 ` 997` hoelzl@41831 ` 998` ```lemma (in measure_space) measure_preserving_Int_stable: ``` hoelzl@41831 ` 999` ``` fixes A :: "nat \ 'a set" ``` hoelzl@41981 ` 1000` ``` assumes E: "Int_stable E" "range A \ sets E" "incseq A" "(\i. A i) = space E" "\i. measure E (A i) \ \" ``` hoelzl@41831 ` 1001` ``` and N: "measure_space (sigma E)" ``` hoelzl@41831 ` 1002` ``` and T: "T \ measure_preserving M E" ``` hoelzl@41831 ` 1003` ``` shows "T \ measure_preserving M (sigma E)" ``` hoelzl@41831 ` 1004` ```proof ``` hoelzl@41831 ` 1005` ``` interpret E: measure_space "sigma E" by fact ``` hoelzl@41831 ` 1006` ``` show "T \ measurable M (sigma E)" ``` hoelzl@41831 ` 1007` ``` using T E.sets_into_space ``` hoelzl@41831 ` 1008` ``` by (intro measurable_sigma) (auto simp: measure_preserving_def measurable_def) ``` hoelzl@41831 ` 1009` ``` fix X assume "X \ sets (sigma E)" ``` hoelzl@41831 ` 1010` ``` show "\ (T -` X \ space M) = E.\ X" ``` hoelzl@41831 ` 1011` ``` proof (rule measure_unique_Int_stable_vimage[symmetric]) ``` hoelzl@41831 ` 1012` ``` show "sets (sigma E) = sets (sigma E)" "space E = space (sigma E)" ``` hoelzl@41981 ` 1013` ``` "\i. E.\ (A i) \ \" using E by auto ``` hoelzl@41831 ` 1014` ``` show "measure_space M" by default ``` hoelzl@41831 ` 1015` ``` next ``` hoelzl@41831 ` 1016` ``` fix X assume "X \ sets E" then show "E.\ X = \ (T -` X \ space M)" ``` hoelzl@41831 ` 1017` ``` using T unfolding measure_preserving_def by auto ``` hoelzl@41831 ` 1018` ``` qed fact+ ``` hoelzl@41831 ` 1019` ```qed ``` hoelzl@41831 ` 1020` hoelzl@38656 ` 1021` ```section "Real measure values" ``` hoelzl@38656 ` 1022` hoelzl@38656 ` 1023` ```lemma (in measure_space) real_measure_Union: ``` hoelzl@41981 ` 1024` ``` assumes finite: "\ A \ \" "\ B \ \" ``` hoelzl@38656 ` 1025` ``` and measurable: "A \ sets M" "B \ sets M" "A \ B = {}" ``` hoelzl@38656 ` 1026` ``` shows "real (\ (A \ B)) = real (\ A) + real (\ B)" ``` hoelzl@38656 ` 1027` ``` unfolding measure_additive[symmetric, OF measurable] ``` hoelzl@41981 ` 1028` ``` using measurable(1,2)[THEN positive_measure] ``` hoelzl@41981 ` 1029` ``` using finite by (cases rule: extreal2_cases[of "\ A" "\ B"]) auto ``` hoelzl@38656 ` 1030` hoelzl@38656 ` 1031` ```lemma (in measure_space) real_measure_finite_Union: ``` hoelzl@38656 ` 1032` ``` assumes measurable: ``` hoelzl@38656 ` 1033` ``` "finite S" "\i. i \ S \ A i \ sets M" "disjoint_family_on A S" ``` hoelzl@41981 ` 1034` ``` assumes finite: "\i. i \ S \ \ (A i) \ \" ``` hoelzl@38656 ` 1035` ``` shows "real (\ (\i\S. A i)) = (\i\S. real (\ (A i)))" ``` hoelzl@41981 ` 1036` ``` using finite measurable(2)[THEN positive_measure] ``` hoelzl@41981 ` 1037` ``` by (force intro!: setsum_real_of_extreal[symmetric] ``` hoelzl@41981 ` 1038` ``` simp: measure_setsum[OF measurable, symmetric]) ``` hoelzl@38656 ` 1039` hoelzl@38656 ` 1040` ```lemma (in measure_space) real_measure_Diff: ``` hoelzl@41981 ` 1041` ``` assumes finite: "\ A \ \" ``` hoelzl@38656 ` 1042` ``` and measurable: "A \ sets M" "B \ sets M" "B \ A" ``` hoelzl@38656 ` 1043` ``` shows "real (\ (A - B)) = real (\ A) - real (\ B)" ``` hoelzl@38656 ` 1044` ```proof - ``` hoelzl@41981 ` 1045` ``` have "\ (A - B) \ \ A" "\ B \ \ A" ``` hoelzl@38656 ` 1046` ``` using measurable by (auto intro!: measure_mono) ``` hoelzl@38656 ` 1047` ``` hence "real (\ ((A - B) \ B)) = real (\ (A - B)) + real (\ B)" ``` hoelzl@38656 ` 1048` ``` using measurable finite by (rule_tac real_measure_Union) auto ``` hoelzl@38656 ` 1049` ``` thus ?thesis using `B \ A` by (auto simp: Un_absorb2) ``` hoelzl@38656 ` 1050` ```qed ``` hoelzl@38656 ` 1051` hoelzl@38656 ` 1052` ```lemma (in measure_space) real_measure_UNION: ``` hoelzl@38656 ` 1053` ``` assumes measurable: "range A \ sets M" "disjoint_family A" ``` hoelzl@41981 ` 1054` ``` assumes finite: "\ (\i. A i) \ \" ``` hoelzl@38656 ` 1055` ``` shows "(\i. real (\ (A i))) sums (real (\ (\i. A i)))" ``` hoelzl@38656 ` 1056` ```proof - ``` hoelzl@41981 ` 1057` ``` have "\i. 0 \ \ (A i)" using measurable by auto ``` hoelzl@41981 ` 1058` ``` with summable_sums[OF summable_extreal_pos, of "\i. \ (A i)"] ``` hoelzl@41981 ` 1059` ``` measure_countably_additive[OF measurable] ``` hoelzl@41981 ` 1060` ``` have "(\i. \ (A i)) sums (\ (\i. A i))" by simp ``` hoelzl@41981 ` 1061` ``` moreover ``` hoelzl@41981 ` 1062` ``` { fix i ``` hoelzl@41981 ` 1063` ``` have "\ (A i) \ \ (\i. A i)" ``` hoelzl@41981 ` 1064` ``` using measurable by (auto intro!: measure_mono) ``` hoelzl@41981 ` 1065` ``` moreover have "0 \ \ (A i)" using measurable by auto ``` hoelzl@41981 ` 1066` ``` ultimately have "\ (A i) = extreal (real (\ (A i)))" ``` hoelzl@41981 ` 1067` ``` using finite by (cases "\ (A i)") auto } ``` hoelzl@41981 ` 1068` ``` moreover ``` hoelzl@41981 ` 1069` ``` have "0 \ \ (\i. A i)" using measurable by auto ``` hoelzl@41981 ` 1070` ``` then have "\ (\i. A i) = extreal (real (\ (\i. A i)))" ``` hoelzl@41981 ` 1071` ``` using finite by (cases "\ (\i. A i)") auto ``` hoelzl@41981 ` 1072` ``` ultimately show ?thesis ``` hoelzl@41981 ` 1073` ``` unfolding sums_extreal[symmetric] by simp ``` hoelzl@38656 ` 1074` ```qed ``` hoelzl@38656 ` 1075` hoelzl@38656 ` 1076` ```lemma (in measure_space) real_measure_subadditive: ``` hoelzl@38656 ` 1077` ``` assumes measurable: "A \ sets M" "B \ sets M" ``` hoelzl@41981 ` 1078` ``` and fin: "\ A \ \" "\ B \ \" ``` hoelzl@38656 ` 1079` ``` shows "real (\ (A \ B)) \ real (\ A) + real (\ B)" ``` hoelzl@38656 ` 1080` ```proof - ``` hoelzl@41981 ` 1081` ``` have "0 \ \ (A \ B)" using measurable by auto ``` hoelzl@41981 ` 1082` ``` then show "real (\ (A \ B)) \ real (\ A) + real (\ B)" ``` hoelzl@41981 ` 1083` ``` using measure_subadditive[OF measurable] fin ``` hoelzl@41981 ` 1084` ``` by (cases rule: extreal3_cases[of "\ (A \ B)" "\ A" "\ B"]) auto ``` hoelzl@38656 ` 1085` ```qed ``` hoelzl@38656 ` 1086` hoelzl@38656 ` 1087` ```lemma (in measure_space) real_measure_setsum_singleton: ``` hoelzl@38656 ` 1088` ``` assumes S: "finite S" "\x. x \ S \ {x} \ sets M" ``` hoelzl@41981 ` 1089` ``` and fin: "\x. x \ S \ \ {x} \ \" ``` hoelzl@38656 ` 1090` ``` shows "real (\ S) = (\x\S. real (\ {x}))" ``` hoelzl@41981 ` 1091` ``` using measure_finite_singleton[OF S] fin ``` hoelzl@41981 ` 1092` ``` using positive_measure[OF S(2)] ``` hoelzl@41981 ` 1093` ``` by (force intro!: setsum_real_of_extreal[symmetric]) ``` hoelzl@38656 ` 1094` hoelzl@38656 ` 1095` ```lemma (in measure_space) real_continuity_from_below: ``` hoelzl@41981 ` 1096` ``` assumes A: "range A \ sets M" "incseq A" and fin: "\ (\i. A i) \ \" ``` hoelzl@38656 ` 1097` ``` shows "(\i. real (\ (A i))) ----> real (\ (\i. A i))" ``` hoelzl@41981 ` 1098` ```proof - ``` hoelzl@41981 ` 1099` ``` have "0 \ \ (\i. A i)" using A by auto ``` hoelzl@41981 ` 1100` ``` then have "extreal (real (\ (\i. A i))) = \ (\i. A i)" ``` hoelzl@41981 ` 1101` ``` using fin by (auto intro: extreal_real') ``` hoelzl@41981 ` 1102` ``` then show ?thesis ``` hoelzl@41981 ` 1103` ``` using continuity_from_below_Lim[OF A] ``` hoelzl@41981 ` 1104` ``` by (intro lim_real_of_extreal) simp ``` hoelzl@41981 ` 1105` ```qed ``` hoelzl@38656 ` 1106` hoelzl@41981 ` 1107` ```lemma (in measure_space) continuity_from_above_Lim: ``` hoelzl@41981 ` 1108` ``` assumes A: "range A \ sets M" "decseq A" and fin: "\i. \ (A i) \ \" ``` hoelzl@41981 ` 1109` ``` shows "(\i. (\ (A i))) ----> \ (\i. A i)" ``` hoelzl@41981 ` 1110` ``` using LIMSEQ_extreal_INFI[OF measure_decseq, OF A] ``` hoelzl@41981 ` 1111` ``` using continuity_from_above[OF A fin] by simp ``` hoelzl@38656 ` 1112` hoelzl@38656 ` 1113` ```lemma (in measure_space) real_continuity_from_above: ``` hoelzl@41981 ` 1114` ``` assumes A: "range A \ sets M" "decseq A" and fin: "\i. \ (A i) \ \" ``` hoelzl@38656 ` 1115` ``` shows "(\n. real (\ (A n))) ----> real (\ (\i. A i))" ``` hoelzl@41981 ` 1116` ```proof - ``` hoelzl@41981 ` 1117` ``` have "0 \ \ (\i. A i)" using A by auto ``` hoelzl@41981 ` 1118` ``` moreover ``` hoelzl@41981 ` 1119` ``` have "\ (\i. A i) \ \ (A 0)" ``` hoelzl@41981 ` 1120` ``` using A by (auto intro!: measure_mono) ``` hoelzl@41981 ` 1121` ``` ultimately have "extreal (real (\ (\i. A i))) = \ (\i. A i)" ``` hoelzl@41981 ` 1122` ``` using fin by (auto intro: extreal_real') ``` hoelzl@41981 ` 1123` ``` then show ?thesis ``` hoelzl@41981 ` 1124` ``` using continuity_from_above_Lim[OF A fin] ``` hoelzl@41981 ` 1125` ``` by (intro lim_real_of_extreal) simp ``` hoelzl@41981 ` 1126` ```qed ``` hoelzl@38656 ` 1127` hoelzl@41981 ` 1128` ```lemma (in measure_space) real_measure_countably_subadditive: ``` hoelzl@41981 ` 1129` ``` assumes A: "range A \ sets M" and fin: "(\i. \ (A i)) \ \" ``` hoelzl@41981 ` 1130` ``` shows "real (\ (\i. A i)) \ (\i. real (\ (A i)))" ``` hoelzl@41981 ` 1131` ```proof - ``` hoelzl@41981 ` 1132` ``` { fix i ``` hoelzl@41981 ` 1133` ``` have "0 \ \ (A i)" using A by auto ``` hoelzl@41981 ` 1134` ``` moreover have "\ (A i) \ \" using A by (intro suminf_PInfty[OF _ fin]) auto ``` hoelzl@41981 ` 1135` ``` ultimately have "\\ (A i)\ \ \" by auto } ``` hoelzl@41981 ` 1136` ``` moreover have "0 \ \ (\i. A i)" using A by auto ``` hoelzl@41981 ` 1137` ``` ultimately have "extreal (real (\ (\i. A i))) \ (\i. extreal (real (\ (A i))))" ``` hoelzl@41981 ` 1138` ``` using measure_countably_subadditive[OF A] by (auto simp: extreal_real) ``` hoelzl@41981 ` 1139` ``` also have "\ = extreal (\i. real (\ (A i)))" ``` hoelzl@41981 ` 1140` ``` using A ``` hoelzl@41981 ` 1141` ``` by (auto intro!: sums_unique[symmetric] sums_extreal[THEN iffD2] summable_sums summable_real_of_extreal fin) ``` hoelzl@41981 ` 1142` ``` finally show ?thesis by simp ``` hoelzl@41981 ` 1143` ```qed ``` hoelzl@38656 ` 1144` hoelzl@38656 ` 1145` ```locale finite_measure = measure_space + ``` hoelzl@41981 ` 1146` ``` assumes finite_measure_of_space: "\ (space M) \ \" ``` hoelzl@38656 ` 1147` hoelzl@38656 ` 1148` ```sublocale finite_measure < sigma_finite_measure ``` hoelzl@38656 ` 1149` ```proof ``` hoelzl@41981 ` 1150` ``` show "\A. range A \ sets M \ (\i. A i) = space M \ (\i. \ (A i) \ \)" ``` hoelzl@38656 ` 1151` ``` using finite_measure_of_space by (auto intro!: exI[of _ "\x. space M"]) ``` hoelzl@38656 ` 1152` ```qed ``` hoelzl@38656 ` 1153` hoelzl@39092 ` 1154` ```lemma (in finite_measure) finite_measure[simp, intro]: ``` hoelzl@38656 ` 1155` ``` assumes "A \ sets M" ``` hoelzl@41981 ` 1156` ``` shows "\ A \ \" ``` hoelzl@38656 ` 1157` ```proof - ``` hoelzl@38656 ` 1158` ``` from `A \ sets M` have "A \ space M" ``` hoelzl@38656 ` 1159` ``` using sets_into_space by blast ``` hoelzl@41981 ` 1160` ``` then have "\ A \ \ (space M)" ``` hoelzl@38656 ` 1161` ``` using assms top by (rule measure_mono) ``` hoelzl@41981 ` 1162` ``` then show ?thesis ``` hoelzl@41981 ` 1163` ``` using finite_measure_of_space by auto ``` hoelzl@38656 ` 1164` ```qed ``` hoelzl@38656 ` 1165` hoelzl@41981 ` 1166` ```lemma (in finite_measure) measure_not_inf: ``` hoelzl@41981 ` 1167` ``` assumes A: "A \ sets M" ``` hoelzl@41981 ` 1168` ``` shows "\\ A\ \ \" ``` hoelzl@41981 ` 1169` ``` using finite_measure[OF A] positive_measure[OF A] by auto ``` hoelzl@41981 ` 1170` hoelzl@41981 ` 1171` ```definition (in finite_measure) ``` hoelzl@41981 ` 1172` ``` "\' A = (if A \ sets M then real (\ A) else 0)" ``` hoelzl@41981 ` 1173` hoelzl@41981 ` 1174` ```lemma (in finite_measure) finite_measure_eq: "A \ sets M \ \ A = extreal (\' A)" ``` hoelzl@41981 ` 1175` ``` using measure_not_inf[of A] by (auto simp: \'_def) ``` hoelzl@41981 ` 1176` hoelzl@41981 ` 1177` ```lemma (in finite_measure) positive_measure': "0 \ \' A" ``` hoelzl@41981 ` 1178` ``` unfolding \'_def by (auto simp: real_of_extreal_pos) ``` hoelzl@41981 ` 1179` hoelzl@41981 ` 1180` ```lemma (in finite_measure) bounded_measure: "\' A \ \' (space M)" ``` hoelzl@41981 ` 1181` ```proof cases ``` hoelzl@41981 ` 1182` ``` assume "A \ sets M" ``` hoelzl@41981 ` 1183` ``` moreover then have "\ A \ \ (space M)" ``` hoelzl@41981 ` 1184` ``` using sets_into_space by (auto intro!: measure_mono) ``` hoelzl@41981 ` 1185` ``` ultimately show ?thesis ``` hoelzl@41981 ` 1186` ``` using measure_not_inf[of A] measure_not_inf[of "space M"] ``` hoelzl@41981 ` 1187` ``` by (auto simp: \'_def) ``` hoelzl@41981 ` 1188` ```qed (simp add: \'_def real_of_extreal_pos) ``` hoelzl@41981 ` 1189` hoelzl@38656 ` 1190` ```lemma (in finite_measure) restricted_finite_measure: ``` hoelzl@38656 ` 1191` ``` assumes "S \ sets M" ``` hoelzl@41689 ` 1192` ``` shows "finite_measure (restricted_space S)" ``` hoelzl@41689 ` 1193` ``` (is "finite_measure ?r") ``` hoelzl@38656 ` 1194` ``` unfolding finite_measure_def finite_measure_axioms_def ``` hoelzl@41981 ` 1195` ```proof (intro conjI) ``` hoelzl@41689 ` 1196` ``` show "measure_space ?r" using restricted_measure_space[OF assms] . ``` hoelzl@38656 ` 1197` ```next ``` hoelzl@41981 ` 1198` ``` show "measure ?r (space ?r) \ \" using finite_measure[OF `S \ sets M`] by auto ``` hoelzl@38656 ` 1199` ```qed ``` hoelzl@38656 ` 1200` hoelzl@40859 ` 1201` ```lemma (in measure_space) restricted_to_finite_measure: ``` hoelzl@41981 ` 1202` ``` assumes "S \ sets M" "\ S \ \" ``` hoelzl@41689 ` 1203` ``` shows "finite_measure (restricted_space S)" ``` hoelzl@40859 ` 1204` ```proof - ``` hoelzl@41689 ` 1205` ``` have "measure_space (restricted_space S)" ``` hoelzl@40859 ` 1206` ``` using `S \ sets M` by (rule restricted_measure_space) ``` hoelzl@40859 ` 1207` ``` then show ?thesis ``` hoelzl@40859 ` 1208` ``` unfolding finite_measure_def finite_measure_axioms_def ``` hoelzl@40859 ` 1209` ``` using assms by auto ``` hoelzl@40859 ` 1210` ```qed ``` hoelzl@40859 ` 1211` hoelzl@41981 ` 1212` ```lemma (in finite_measure) finite_measure_Diff: ``` hoelzl@41981 ` 1213` ``` assumes sets: "A \ sets M" "B \ sets M" and "B \ A" ``` hoelzl@41981 ` 1214` ``` shows "\' (A - B) = \' A - \' B" ``` hoelzl@41981 ` 1215` ``` using sets[THEN finite_measure_eq] ``` hoelzl@41981 ` 1216` ``` using Diff[OF sets, THEN finite_measure_eq] ``` hoelzl@41981 ` 1217` ``` using measure_Diff[OF _ assms] by simp ``` hoelzl@38656 ` 1218` hoelzl@41981 ` 1219` ```lemma (in finite_measure) finite_measure_Union: ``` hoelzl@41981 ` 1220` ``` assumes sets: "A \ sets M" "B \ sets M" and "A \ B = {}" ``` hoelzl@41981 ` 1221` ``` shows "\' (A \ B) = \' A + \' B" ``` hoelzl@41981 ` 1222` ``` using measure_additive[OF assms] ``` hoelzl@41981 ` 1223` ``` using sets[THEN finite_measure_eq] ``` hoelzl@41981 ` 1224` ``` using Un[OF sets, THEN finite_measure_eq] ``` hoelzl@41981 ` 1225` ``` by simp ``` hoelzl@38656 ` 1226` hoelzl@41981 ` 1227` ```lemma (in finite_measure) finite_measure_finite_Union: ``` hoelzl@41981 ` 1228` ``` assumes S: "finite S" "\i. i \ S \ A i \ sets M" ``` hoelzl@41981 ` 1229` ``` and dis: "disjoint_family_on A S" ``` hoelzl@41981 ` 1230` ``` shows "\' (\i\S. A i) = (\i\S. \' (A i))" ``` hoelzl@41981 ` 1231` ``` using measure_setsum[OF assms] ``` hoelzl@41981 ` 1232` ``` using finite_UN[of S A, OF S, THEN finite_measure_eq] ``` hoelzl@41981 ` 1233` ``` using S(2)[THEN finite_measure_eq] ``` hoelzl@41981 ` 1234` ``` by simp ``` hoelzl@38656 ` 1235` hoelzl@41981 ` 1236` ```lemma (in finite_measure) finite_measure_UNION: ``` hoelzl@41981 ` 1237` ``` assumes A: "range A \ sets M" "disjoint_family A" ``` hoelzl@41981 ` 1238` ``` shows "(\i. \' (A i)) sums (\' (\i. A i))" ``` hoelzl@41981 ` 1239` ``` using real_measure_UNION[OF A] ``` hoelzl@41981 ` 1240` ``` using countable_UN[OF A(1), THEN finite_measure_eq] ``` hoelzl@41981 ` 1241` ``` using A(1)[THEN subsetD, THEN finite_measure_eq] ``` hoelzl@39092 ` 1242` ``` by auto ``` hoelzl@39092 ` 1243` hoelzl@41981 ` 1244` ```lemma (in finite_measure) finite_measure_mono: ``` hoelzl@41981 ` 1245` ``` assumes B: "B \ sets M" and "A \ B" shows "\' A \ \' B" ``` hoelzl@41981 ` 1246` ```proof cases ``` hoelzl@41981 ` 1247` ``` assume "A \ sets M" ``` hoelzl@41981 ` 1248` ``` from this[THEN finite_measure_eq] B[THEN finite_measure_eq] ``` hoelzl@41981 ` 1249` ``` show ?thesis using measure_mono[OF `A \ B` `A \ sets M` `B \ sets M`] by simp ``` hoelzl@41981 ` 1250` ```next ``` hoelzl@41981 ` 1251` ``` assume "A \ sets M" then show ?thesis ``` hoelzl@41981 ` 1252` ``` using positive_measure'[of B] unfolding \'_def by auto ``` hoelzl@41981 ` 1253` ```qed ``` hoelzl@41981 ` 1254` hoelzl@41981 ` 1255` ```lemma (in finite_measure) finite_measure_subadditive: ``` hoelzl@41981 ` 1256` ``` assumes m: "A \ sets M" "B \ sets M" ``` hoelzl@41981 ` 1257` ``` shows "\' (A \ B) \ \' A + \' B" ``` hoelzl@41981 ` 1258` ``` using measure_subadditive[OF m] ``` hoelzl@41981 ` 1259` ``` using m[THEN finite_measure_eq] Un[OF m, THEN finite_measure_eq] by simp ``` hoelzl@41981 ` 1260` hoelzl@41981 ` 1261` ```lemma (in finite_measure) finite_measure_countably_subadditive: ``` hoelzl@41981 ` 1262` ``` assumes A: "range A \ sets M" and sum: "summable (\i. \' (A i))" ``` hoelzl@41981 ` 1263` ``` shows "\' (\i. A i) \ (\i. \' (A i))" ``` hoelzl@38656 ` 1264` ```proof - ``` hoelzl@41981 ` 1265` ``` note A[THEN subsetD, THEN finite_measure_eq, simp] ``` hoelzl@41981 ` 1266` ``` note countable_UN[OF A, THEN finite_measure_eq, simp] ``` hoelzl@41981 ` 1267` ``` from `summable (\i. \' (A i))` ``` hoelzl@41981 ` 1268` ``` have "(\i. extreal (\' (A i))) sums extreal (\i. \' (A i))" ``` hoelzl@41981 ` 1269` ``` by (simp add: sums_extreal) (rule summable_sums) ``` hoelzl@41981 ` 1270` ``` from sums_unique[OF this, symmetric] ``` hoelzl@41981 ` 1271` ``` measure_countably_subadditive[OF A] ``` hoelzl@41981 ` 1272` ``` show ?thesis by simp ``` hoelzl@38656 ` 1273` ```qed ``` hoelzl@38656 ` 1274` hoelzl@41981 ` 1275` ```lemma (in finite_measure) finite_measure_finite_singleton: ``` hoelzl@41981 ` 1276` ``` assumes "finite S" and *: "\x. x \ S \ {x} \ sets M" ``` hoelzl@41981 ` 1277` ``` shows "\' S = (\x\S. \' {x})" ``` hoelzl@41981 ` 1278` ``` using real_measure_setsum_singleton[OF assms] ``` hoelzl@41981 ` 1279` ``` using *[THEN finite_measure_eq] ``` hoelzl@41981 ` 1280` ``` using finite_UN[of S "\x. {x}", OF assms, THEN finite_measure_eq] ``` hoelzl@41981 ` 1281` ``` by simp ``` hoelzl@41981 ` 1282` hoelzl@41981 ` 1283` ```lemma (in finite_measure) finite_continuity_from_below: ``` hoelzl@41981 ` 1284` ``` assumes A: "range A \ sets M" and "incseq A" ``` hoelzl@41981 ` 1285` ``` shows "(\i. \' (A i)) ----> \' (\i. A i)" ``` hoelzl@41981 ` 1286` ``` using real_continuity_from_below[OF A, OF `incseq A` finite_measure] assms ``` hoelzl@41981 ` 1287` ``` using A[THEN subsetD, THEN finite_measure_eq] ``` hoelzl@41981 ` 1288` ``` using countable_UN[OF A, THEN finite_measure_eq] ``` hoelzl@41981 ` 1289` ``` by auto ``` hoelzl@41981 ` 1290` hoelzl@41981 ` 1291` ```lemma (in finite_measure) finite_continuity_from_above: ``` hoelzl@41981 ` 1292` ``` assumes A: "range A \ sets M" and "decseq A" ``` hoelzl@41981 ` 1293` ``` shows "(\n. \' (A n)) ----> \' (\i. A i)" ``` hoelzl@41981 ` 1294` ``` using real_continuity_from_above[OF A, OF `decseq A` finite_measure] assms ``` hoelzl@41981 ` 1295` ``` using A[THEN subsetD, THEN finite_measure_eq] ``` hoelzl@41981 ` 1296` ``` using countable_INT[OF A, THEN finite_measure_eq] ``` hoelzl@41981 ` 1297` ``` by auto ``` hoelzl@41981 ` 1298` hoelzl@41981 ` 1299` ```lemma (in finite_measure) finite_measure_compl: ``` hoelzl@41981 ` 1300` ``` assumes S: "S \ sets M" ``` hoelzl@41981 ` 1301` ``` shows "\' (space M - S) = \' (space M) - \' S" ``` hoelzl@41981 ` 1302` ``` using measure_compl[OF S, OF finite_measure, OF S] ``` hoelzl@41981 ` 1303` ``` using S[THEN finite_measure_eq] ``` hoelzl@41981 ` 1304` ``` using compl_sets[OF S, THEN finite_measure_eq] ``` hoelzl@41981 ` 1305` ``` using top[THEN finite_measure_eq] ``` hoelzl@41981 ` 1306` ``` by simp ``` hoelzl@41981 ` 1307` hoelzl@41981 ` 1308` ```lemma (in finite_measure) finite_measure_inter_full_set: ``` hoelzl@41981 ` 1309` ``` assumes S: "S \ sets M" "T \ sets M" ``` hoelzl@41981 ` 1310` ``` assumes T: "\' T = \' (space M)" ``` hoelzl@41981 ` 1311` ``` shows "\' (S \ T) = \' S" ``` hoelzl@41981 ` 1312` ``` using measure_inter_full_set[OF S finite_measure] ``` hoelzl@41981 ` 1313` ``` using T Diff[OF S(2,1)] Diff[OF S, THEN finite_measure_eq] ``` hoelzl@41981 ` 1314` ``` using Int[OF S, THEN finite_measure_eq] ``` hoelzl@41981 ` 1315` ``` using S[THEN finite_measure_eq] top[THEN finite_measure_eq] ``` hoelzl@41981 ` 1316` ``` by simp ``` hoelzl@41981 ` 1317` hoelzl@41981 ` 1318` ```lemma (in finite_measure) empty_measure'[simp]: "\' {} = 0" ``` hoelzl@41981 ` 1319` ``` unfolding \'_def by simp ``` hoelzl@41981 ` 1320` hoelzl@38656 ` 1321` ```section "Finite spaces" ``` hoelzl@38656 ` 1322` hoelzl@40859 ` 1323` ```locale finite_measure_space = measure_space + finite_sigma_algebra + ``` hoelzl@41981 ` 1324` ``` assumes finite_single_measure[simp]: "\x. x \ space M \ \ {x} \ \" ``` hoelzl@39092 ` 1325` hoelzl@38656 ` 1326` ```lemma (in finite_measure_space) sum_over_space: "(\x\space M. \ {x}) = \ (space M)" ``` hoelzl@41981 ` 1327` ``` using measure_setsum[of "space M" "\i. {i}"] ``` hoelzl@36624 ` 1328` ``` by (simp add: sets_eq_Pow disjoint_family_on_def finite_space) ``` hoelzl@36624 ` 1329` hoelzl@39092 ` 1330` ```lemma finite_measure_spaceI: ``` hoelzl@41981 ` 1331` ``` assumes "finite (space M)" "sets M = Pow(space M)" and space: "measure M (space M) \ \" ``` hoelzl@41689 ` 1332` ``` and add: "\A B. A\space M \ B\space M \ A \ B = {} \ measure M (A \ B) = measure M A + measure M B" ``` hoelzl@41981 ` 1333` ``` and "measure M {} = 0" "\A. A \ space M \ 0 \ measure M A" ``` hoelzl@41689 ` 1334` ``` shows "finite_measure_space M" ``` hoelzl@39092 ` 1335` ``` unfolding finite_measure_space_def finite_measure_space_axioms_def ``` hoelzl@40859 ` 1336` ```proof (intro allI impI conjI) ``` hoelzl@41689 ` 1337` ``` show "measure_space M" ``` hoelzl@41689 ` 1338` ``` proof (rule finite_additivity_sufficient) ``` hoelzl@41689 ` 1339` ``` have *: "\space = space M, sets = Pow (space M), \ = algebra.more M\ = M" ``` hoelzl@41689 ` 1340` ``` unfolding assms(2)[symmetric] by (auto intro!: algebra.equality) ``` hoelzl@39092 ` 1341` ``` show "sigma_algebra M" ``` hoelzl@41689 ` 1342` ``` using sigma_algebra_Pow[of "space M" "algebra.more M"] ``` hoelzl@41689 ` 1343` ``` unfolding * . ``` hoelzl@39092 ` 1344` ``` show "finite (space M)" by fact ``` hoelzl@41981 ` 1345` ``` show "positive M (measure M)" unfolding positive_def using assms by auto ``` hoelzl@41689 ` 1346` ``` show "additive M (measure M)" unfolding additive_def using assms by simp ``` hoelzl@39092 ` 1347` ``` qed ``` hoelzl@41689 ` 1348` ``` then interpret measure_space M . ``` hoelzl@40859 ` 1349` ``` show "finite_sigma_algebra M" ``` hoelzl@40859 ` 1350` ``` proof ``` hoelzl@40859 ` 1351` ``` show "finite (space M)" by fact ``` hoelzl@40859 ` 1352` ``` show "sets M = Pow (space M)" using assms by auto ``` hoelzl@40859 ` 1353` ``` qed ``` hoelzl@39092 ` 1354` ``` { fix x assume *: "x \ space M" ``` hoelzl@39092 ` 1355` ``` with add[of "{x}" "space M - {x}"] space ``` hoelzl@41981 ` 1356` ``` show "\ {x} \ \" by (auto simp: insert_absorb[OF *] Diff_subset) } ``` hoelzl@39092 ` 1357` ```qed ``` hoelzl@39092 ` 1358` hoelzl@40871 ` 1359` ```sublocale finite_measure_space \ finite_measure ``` hoelzl@38656 ` 1360` ```proof ``` hoelzl@41981 ` 1361` ``` show "\ (space M) \ \" ``` hoelzl@41981 ` 1362` ``` unfolding sum_over_space[symmetric] setsum_Pinfty ``` hoelzl@38656 ` 1363` ``` using finite_space finite_single_measure by auto ``` hoelzl@38656 ` 1364` ```qed ``` hoelzl@38656 ` 1365` hoelzl@39092 ` 1366` ```lemma finite_measure_space_iff: ``` hoelzl@41689 ` 1367` ``` "finite_measure_space M \ ``` hoelzl@41981 ` 1368` ``` finite (space M) \ sets M = Pow(space M) \ measure M (space M) \ \ \ ``` hoelzl@41981 ` 1369` ``` measure M {} = 0 \ (\A\space M. 0 \ measure M A) \ ``` hoelzl@41689 ` 1370` ``` (\A\space M. \B\space M. A \ B = {} \ measure M (A \ B) = measure M A + measure M B)" ``` hoelzl@39092 ` 1371` ``` (is "_ = ?rhs") ``` hoelzl@39092 ` 1372` ```proof (intro iffI) ``` hoelzl@41689 ` 1373` ``` assume "finite_measure_space M" ``` hoelzl@41689 ` 1374` ``` then interpret finite_measure_space M . ``` hoelzl@39092 ` 1375` ``` show ?rhs ``` hoelzl@39092 ` 1376` ``` using finite_space sets_eq_Pow measure_additive empty_measure finite_measure ``` hoelzl@39092 ` 1377` ``` by auto ``` hoelzl@39092 ` 1378` ```next ``` hoelzl@41689 ` 1379` ``` assume ?rhs then show "finite_measure_space M" ``` hoelzl@39092 ` 1380` ``` by (auto intro!: finite_measure_spaceI) ``` hoelzl@39092 ` 1381` ```qed ``` hoelzl@39092 ` 1382` hoelzl@41981 ` 1383` ```lemma suminf_cmult_indicator: ``` hoelzl@41981 ` 1384` ``` fixes f :: "nat \ extreal" ``` hoelzl@41981 ` 1385` ``` assumes "disjoint_family A" "x \ A i" "\i. 0 \ f i" ``` hoelzl@41981 ` 1386` ``` shows "(\n. f n * indicator (A n) x) = f i" ``` hoelzl@38656 ` 1387` ```proof - ``` hoelzl@41981 ` 1388` ``` have **: "\n. f n * indicator (A n) x = (if n = i then f n else 0 :: extreal)" ``` hoelzl@38656 ` 1389` ``` using `x \ A i` assms unfolding disjoint_family_on_def indicator_def by auto ``` hoelzl@41981 ` 1390` ``` then have "\n. (\jn. n \ UNIV \ (if i < n then f i else 0) \ y" ``` hoelzl@38656 ` 1395` ``` from this[of "Suc i"] show "f i \ y" by auto ``` hoelzl@41981 ` 1396` ``` qed (insert assms, simp) ``` hoelzl@41981 ` 1397` ``` ultimately show ?thesis using assms ``` hoelzl@41981 ` 1398` ``` by (subst suminf_extreal_eq_SUPR) (auto simp: indicator_def) ``` hoelzl@38656 ` 1399` ```qed ``` hoelzl@38656 ` 1400` hoelzl@41981 ` 1401` ```lemma suminf_indicator: ``` hoelzl@38656 ` 1402` ``` assumes "disjoint_family A" ``` hoelzl@41981 ` 1403` ``` shows "(\n. indicator (A n) x :: extreal) = indicator (\i. A i) x" ``` hoelzl@38656 ` 1404` ```proof cases ``` hoelzl@38656 ` 1405` ``` assume *: "x \ (\i. A i)" ``` hoelzl@38656 ` 1406` ``` then obtain i where "x \ A i" by auto ``` hoelzl@41981 ` 1407` ``` from suminf_cmult_indicator[OF assms(1), OF `x \ A i`, of "\k. 1"] ``` hoelzl@38656 ` 1408` ``` show ?thesis using * by simp ``` hoelzl@38656 ` 1409` ```qed simp ``` hoelzl@38656 ` 1410` hoelzl@35582 ` 1411` `end`