src/HOL/Probability/Lebesgue_Integration.thy
 author hoelzl Wed Dec 01 19:20:30 2010 +0100 (2010-12-01) changeset 40859 de0b30e6c2d2 parent 40786 0a54cfc9add3 child 40871 688f6ff859e1 permissions -rw-r--r--
Support product spaces on sigma finite measures.
Introduce the almost everywhere quantifier.
Introduce 'morphism' theorems for most constants.
Prove uniqueness of measures on cut stable generators.
Prove uniqueness of the Radon-Nikodym derivative.
Removed misleading suffix from borel_space and lebesgue_space.
Use product spaces to introduce Fubini on the Lebesgue integral.
Combine Euclidean_Lebesgue and Lebesgue_Measure.
Generalize theorems about mutual information and entropy to arbitrary probability spaces.
Remove simproc mult_log as it does not work with interpretations.
Introduce completion of measure spaces.
Change type of sigma.
Introduce dynkin systems.
 hoelzl@38656 ` 1` ```(* Author: Armin Heller, Johannes Hoelzl, TU Muenchen *) ``` hoelzl@38656 ` 2` hoelzl@35582 ` 3` ```header {*Lebesgue Integration*} ``` hoelzl@35582 ` 4` hoelzl@38656 ` 5` ```theory Lebesgue_Integration ``` hoelzl@40859 ` 6` ```imports Measure Borel_Space ``` hoelzl@35582 ` 7` ```begin ``` hoelzl@35582 ` 8` hoelzl@40859 ` 9` ```lemma image_set_cong: ``` hoelzl@40859 ` 10` ``` assumes A: "\x. x \ A \ \y\B. f x = g y" ``` hoelzl@40859 ` 11` ``` assumes B: "\y. y \ B \ \x\A. g y = f x" ``` hoelzl@40859 ` 12` ``` shows "f ` A = g ` B" ``` hoelzl@40859 ` 13` ```proof safe ``` hoelzl@40859 ` 14` ``` fix x assume "x \ A" ``` hoelzl@40859 ` 15` ``` with A obtain y where "f x = g y" "y \ B" by auto ``` hoelzl@40859 ` 16` ``` then show "f x \ g ` B" by auto ``` hoelzl@40859 ` 17` ```next ``` hoelzl@40859 ` 18` ``` fix y assume "y \ B" ``` hoelzl@40859 ` 19` ``` with B obtain x where "g y = f x" "x \ A" by auto ``` hoelzl@40859 ` 20` ``` then show "g y \ f ` A" by auto ``` hoelzl@40859 ` 21` ```qed ``` hoelzl@35582 ` 22` hoelzl@38656 ` 23` ```lemma sums_If_finite: ``` hoelzl@38656 ` 24` ``` assumes finite: "finite {r. P r}" ``` hoelzl@38656 ` 25` ``` shows "(\r. if P r then f r else 0) sums (\r\{r. P r}. f r)" (is "?F sums _") ``` hoelzl@38656 ` 26` ```proof cases ``` hoelzl@38656 ` 27` ``` assume "{r. P r} = {}" hence "\r. \ P r" by auto ``` hoelzl@38656 ` 28` ``` thus ?thesis by (simp add: sums_zero) ``` hoelzl@38656 ` 29` ```next ``` hoelzl@38656 ` 30` ``` assume not_empty: "{r. P r} \ {}" ``` hoelzl@38656 ` 31` ``` have "?F sums (\r = 0..< Suc (Max {r. P r}). ?F r)" ``` hoelzl@38656 ` 32` ``` by (rule series_zero) ``` hoelzl@38656 ` 33` ``` (auto simp add: Max_less_iff[OF finite not_empty] less_eq_Suc_le[symmetric]) ``` hoelzl@38656 ` 34` ``` also have "(\r = 0..< Suc (Max {r. P r}). ?F r) = (\r\{r. P r}. f r)" ``` hoelzl@38656 ` 35` ``` by (subst setsum_cases) ``` hoelzl@38656 ` 36` ``` (auto intro!: setsum_cong simp: Max_ge_iff[OF finite not_empty] less_Suc_eq_le) ``` hoelzl@38656 ` 37` ``` finally show ?thesis . ``` hoelzl@38656 ` 38` ```qed ``` hoelzl@35582 ` 39` hoelzl@38656 ` 40` ```lemma sums_single: ``` hoelzl@38656 ` 41` ``` "(\r. if r = i then f r else 0) sums f i" ``` hoelzl@38656 ` 42` ``` using sums_If_finite[of "\r. r = i" f] by simp ``` hoelzl@38656 ` 43` hoelzl@38656 ` 44` ```section "Simple function" ``` hoelzl@35582 ` 45` hoelzl@38656 ` 46` ```text {* ``` hoelzl@38656 ` 47` hoelzl@38656 ` 48` ```Our simple functions are not restricted to positive real numbers. Instead ``` hoelzl@38656 ` 49` ```they are just functions with a finite range and are measurable when singleton ``` hoelzl@38656 ` 50` ```sets are measurable. ``` hoelzl@35582 ` 51` hoelzl@38656 ` 52` ```*} ``` hoelzl@38656 ` 53` hoelzl@38656 ` 54` ```definition (in sigma_algebra) "simple_function g \ ``` hoelzl@38656 ` 55` ``` finite (g ` space M) \ ``` hoelzl@38656 ` 56` ``` (\x \ g ` space M. g -` {x} \ space M \ sets M)" ``` hoelzl@36624 ` 57` hoelzl@38656 ` 58` ```lemma (in sigma_algebra) simple_functionD: ``` hoelzl@38656 ` 59` ``` assumes "simple_function g" ``` hoelzl@38656 ` 60` ``` shows "finite (g ` space M)" ``` hoelzl@38656 ` 61` ``` "x \ g ` space M \ g -` {x} \ space M \ sets M" ``` hoelzl@38656 ` 62` ``` using assms unfolding simple_function_def by auto ``` hoelzl@36624 ` 63` hoelzl@38656 ` 64` ```lemma (in sigma_algebra) simple_function_indicator_representation: ``` hoelzl@38656 ` 65` ``` fixes f ::"'a \ pinfreal" ``` hoelzl@38656 ` 66` ``` assumes f: "simple_function f" and x: "x \ space M" ``` hoelzl@38656 ` 67` ``` shows "f x = (\y \ f ` space M. y * indicator (f -` {y} \ space M) x)" ``` hoelzl@38656 ` 68` ``` (is "?l = ?r") ``` hoelzl@38656 ` 69` ```proof - ``` hoelzl@38705 ` 70` ``` have "?r = (\y \ f ` space M. ``` hoelzl@38656 ` 71` ``` (if y = f x then y * indicator (f -` {y} \ space M) x else 0))" ``` hoelzl@38656 ` 72` ``` by (auto intro!: setsum_cong2) ``` hoelzl@38656 ` 73` ``` also have "... = f x * indicator (f -` {f x} \ space M) x" ``` hoelzl@38656 ` 74` ``` using assms by (auto dest: simple_functionD simp: setsum_delta) ``` hoelzl@38656 ` 75` ``` also have "... = f x" using x by (auto simp: indicator_def) ``` hoelzl@38656 ` 76` ``` finally show ?thesis by auto ``` hoelzl@38656 ` 77` ```qed ``` hoelzl@36624 ` 78` hoelzl@38656 ` 79` ```lemma (in measure_space) simple_function_notspace: ``` hoelzl@38656 ` 80` ``` "simple_function (\x. h x * indicator (- space M) x::pinfreal)" (is "simple_function ?h") ``` hoelzl@35692 ` 81` ```proof - ``` hoelzl@38656 ` 82` ``` have "?h ` space M \ {0}" unfolding indicator_def by auto ``` hoelzl@38656 ` 83` ``` hence [simp, intro]: "finite (?h ` space M)" by (auto intro: finite_subset) ``` hoelzl@38656 ` 84` ``` have "?h -` {0} \ space M = space M" by auto ``` hoelzl@38656 ` 85` ``` thus ?thesis unfolding simple_function_def by auto ``` hoelzl@38656 ` 86` ```qed ``` hoelzl@38656 ` 87` hoelzl@38656 ` 88` ```lemma (in sigma_algebra) simple_function_cong: ``` hoelzl@38656 ` 89` ``` assumes "\t. t \ space M \ f t = g t" ``` hoelzl@38656 ` 90` ``` shows "simple_function f \ simple_function g" ``` hoelzl@38656 ` 91` ```proof - ``` hoelzl@38656 ` 92` ``` have "f ` space M = g ` space M" ``` hoelzl@38656 ` 93` ``` "\x. f -` {x} \ space M = g -` {x} \ space M" ``` hoelzl@38656 ` 94` ``` using assms by (auto intro!: image_eqI) ``` hoelzl@38656 ` 95` ``` thus ?thesis unfolding simple_function_def using assms by simp ``` hoelzl@38656 ` 96` ```qed ``` hoelzl@38656 ` 97` hoelzl@38656 ` 98` ```lemma (in sigma_algebra) borel_measurable_simple_function: ``` hoelzl@38656 ` 99` ``` assumes "simple_function f" ``` hoelzl@38656 ` 100` ``` shows "f \ borel_measurable M" ``` hoelzl@38656 ` 101` ```proof (rule borel_measurableI) ``` hoelzl@38656 ` 102` ``` fix S ``` hoelzl@38656 ` 103` ``` let ?I = "f ` (f -` S \ space M)" ``` hoelzl@38656 ` 104` ``` have *: "(\x\?I. f -` {x} \ space M) = f -` S \ space M" (is "?U = _") by auto ``` hoelzl@38656 ` 105` ``` have "finite ?I" ``` hoelzl@38656 ` 106` ``` using assms unfolding simple_function_def by (auto intro: finite_subset) ``` hoelzl@38656 ` 107` ``` hence "?U \ sets M" ``` hoelzl@38656 ` 108` ``` apply (rule finite_UN) ``` hoelzl@38656 ` 109` ``` using assms unfolding simple_function_def by auto ``` hoelzl@38656 ` 110` ``` thus "f -` S \ space M \ sets M" unfolding * . ``` hoelzl@35692 ` 111` ```qed ``` hoelzl@35692 ` 112` hoelzl@38656 ` 113` ```lemma (in sigma_algebra) simple_function_borel_measurable: ``` hoelzl@38656 ` 114` ``` fixes f :: "'a \ 'x::t2_space" ``` hoelzl@38656 ` 115` ``` assumes "f \ borel_measurable M" and "finite (f ` space M)" ``` hoelzl@38656 ` 116` ``` shows "simple_function f" ``` hoelzl@38656 ` 117` ``` using assms unfolding simple_function_def ``` hoelzl@38656 ` 118` ``` by (auto intro: borel_measurable_vimage) ``` hoelzl@38656 ` 119` hoelzl@38656 ` 120` ```lemma (in sigma_algebra) simple_function_const[intro, simp]: ``` hoelzl@38656 ` 121` ``` "simple_function (\x. c)" ``` hoelzl@38656 ` 122` ``` by (auto intro: finite_subset simp: simple_function_def) ``` hoelzl@38656 ` 123` hoelzl@38656 ` 124` ```lemma (in sigma_algebra) simple_function_compose[intro, simp]: ``` hoelzl@38656 ` 125` ``` assumes "simple_function f" ``` hoelzl@38656 ` 126` ``` shows "simple_function (g \ f)" ``` hoelzl@38656 ` 127` ``` unfolding simple_function_def ``` hoelzl@38656 ` 128` ```proof safe ``` hoelzl@38656 ` 129` ``` show "finite ((g \ f) ` space M)" ``` hoelzl@38656 ` 130` ``` using assms unfolding simple_function_def by (auto simp: image_compose) ``` hoelzl@38656 ` 131` ```next ``` hoelzl@38656 ` 132` ``` fix x assume "x \ space M" ``` hoelzl@38656 ` 133` ``` let ?G = "g -` {g (f x)} \ (f`space M)" ``` hoelzl@38656 ` 134` ``` have *: "(g \ f) -` {(g \ f) x} \ space M = ``` hoelzl@38656 ` 135` ``` (\x\?G. f -` {x} \ space M)" by auto ``` hoelzl@38656 ` 136` ``` show "(g \ f) -` {(g \ f) x} \ space M \ sets M" ``` hoelzl@38656 ` 137` ``` using assms unfolding simple_function_def * ``` hoelzl@38656 ` 138` ``` by (rule_tac finite_UN) (auto intro!: finite_UN) ``` hoelzl@38656 ` 139` ```qed ``` hoelzl@38656 ` 140` hoelzl@38656 ` 141` ```lemma (in sigma_algebra) simple_function_indicator[intro, simp]: ``` hoelzl@38656 ` 142` ``` assumes "A \ sets M" ``` hoelzl@38656 ` 143` ``` shows "simple_function (indicator A)" ``` hoelzl@35692 ` 144` ```proof - ``` hoelzl@38656 ` 145` ``` have "indicator A ` space M \ {0, 1}" (is "?S \ _") ``` hoelzl@38656 ` 146` ``` by (auto simp: indicator_def) ``` hoelzl@38656 ` 147` ``` hence "finite ?S" by (rule finite_subset) simp ``` hoelzl@38656 ` 148` ``` moreover have "- A \ space M = space M - A" by auto ``` hoelzl@38656 ` 149` ``` ultimately show ?thesis unfolding simple_function_def ``` hoelzl@38656 ` 150` ``` using assms by (auto simp: indicator_def_raw) ``` hoelzl@35692 ` 151` ```qed ``` hoelzl@35692 ` 152` hoelzl@38656 ` 153` ```lemma (in sigma_algebra) simple_function_Pair[intro, simp]: ``` hoelzl@38656 ` 154` ``` assumes "simple_function f" ``` hoelzl@38656 ` 155` ``` assumes "simple_function g" ``` hoelzl@38656 ` 156` ``` shows "simple_function (\x. (f x, g x))" (is "simple_function ?p") ``` hoelzl@38656 ` 157` ``` unfolding simple_function_def ``` hoelzl@38656 ` 158` ```proof safe ``` hoelzl@38656 ` 159` ``` show "finite (?p ` space M)" ``` hoelzl@38656 ` 160` ``` using assms unfolding simple_function_def ``` hoelzl@38656 ` 161` ``` by (rule_tac finite_subset[of _ "f`space M \ g`space M"]) auto ``` hoelzl@38656 ` 162` ```next ``` hoelzl@38656 ` 163` ``` fix x assume "x \ space M" ``` hoelzl@38656 ` 164` ``` have "(\x. (f x, g x)) -` {(f x, g x)} \ space M = ``` hoelzl@38656 ` 165` ``` (f -` {f x} \ space M) \ (g -` {g x} \ space M)" ``` hoelzl@38656 ` 166` ``` by auto ``` hoelzl@38656 ` 167` ``` with `x \ space M` show "(\x. (f x, g x)) -` {(f x, g x)} \ space M \ sets M" ``` hoelzl@38656 ` 168` ``` using assms unfolding simple_function_def by auto ``` hoelzl@38656 ` 169` ```qed ``` hoelzl@35692 ` 170` hoelzl@38656 ` 171` ```lemma (in sigma_algebra) simple_function_compose1: ``` hoelzl@38656 ` 172` ``` assumes "simple_function f" ``` hoelzl@38656 ` 173` ``` shows "simple_function (\x. g (f x))" ``` hoelzl@38656 ` 174` ``` using simple_function_compose[OF assms, of g] ``` hoelzl@38656 ` 175` ``` by (simp add: comp_def) ``` hoelzl@35582 ` 176` hoelzl@38656 ` 177` ```lemma (in sigma_algebra) simple_function_compose2: ``` hoelzl@38656 ` 178` ``` assumes "simple_function f" and "simple_function g" ``` hoelzl@38656 ` 179` ``` shows "simple_function (\x. h (f x) (g x))" ``` hoelzl@38656 ` 180` ```proof - ``` hoelzl@38656 ` 181` ``` have "simple_function ((\(x, y). h x y) \ (\x. (f x, g x)))" ``` hoelzl@38656 ` 182` ``` using assms by auto ``` hoelzl@38656 ` 183` ``` thus ?thesis by (simp_all add: comp_def) ``` hoelzl@38656 ` 184` ```qed ``` hoelzl@35582 ` 185` hoelzl@38656 ` 186` ```lemmas (in sigma_algebra) simple_function_add[intro, simp] = simple_function_compose2[where h="op +"] ``` hoelzl@38656 ` 187` ``` and simple_function_diff[intro, simp] = simple_function_compose2[where h="op -"] ``` hoelzl@38656 ` 188` ``` and simple_function_uminus[intro, simp] = simple_function_compose[where g="uminus"] ``` hoelzl@38656 ` 189` ``` and simple_function_mult[intro, simp] = simple_function_compose2[where h="op *"] ``` hoelzl@38656 ` 190` ``` and simple_function_div[intro, simp] = simple_function_compose2[where h="op /"] ``` hoelzl@38656 ` 191` ``` and simple_function_inverse[intro, simp] = simple_function_compose[where g="inverse"] ``` hoelzl@38656 ` 192` hoelzl@38656 ` 193` ```lemma (in sigma_algebra) simple_function_setsum[intro, simp]: ``` hoelzl@38656 ` 194` ``` assumes "\i. i \ P \ simple_function (f i)" ``` hoelzl@38656 ` 195` ``` shows "simple_function (\x. \i\P. f i x)" ``` hoelzl@38656 ` 196` ```proof cases ``` hoelzl@38656 ` 197` ``` assume "finite P" from this assms show ?thesis by induct auto ``` hoelzl@38656 ` 198` ```qed auto ``` hoelzl@35582 ` 199` hoelzl@38656 ` 200` ```lemma (in sigma_algebra) simple_function_le_measurable: ``` hoelzl@38656 ` 201` ``` assumes "simple_function f" "simple_function g" ``` hoelzl@38656 ` 202` ``` shows "{x \ space M. f x \ g x} \ sets M" ``` hoelzl@38656 ` 203` ```proof - ``` hoelzl@38656 ` 204` ``` have *: "{x \ space M. f x \ g x} = ``` hoelzl@38656 ` 205` ``` (\(F, G)\f`space M \ g`space M. ``` hoelzl@38656 ` 206` ``` if F \ G then (f -` {F} \ space M) \ (g -` {G} \ space M) else {})" ``` hoelzl@38656 ` 207` ``` apply (auto split: split_if_asm) ``` hoelzl@38656 ` 208` ``` apply (rule_tac x=x in bexI) ``` hoelzl@38656 ` 209` ``` apply (rule_tac x=x in bexI) ``` hoelzl@38656 ` 210` ``` by simp_all ``` hoelzl@38656 ` 211` ``` have **: "\x y. x \ space M \ y \ space M \ ``` hoelzl@38656 ` 212` ``` (f -` {f x} \ space M) \ (g -` {g y} \ space M) \ sets M" ``` hoelzl@38656 ` 213` ``` using assms unfolding simple_function_def by auto ``` hoelzl@38656 ` 214` ``` have "finite (f`space M \ g`space M)" ``` hoelzl@38656 ` 215` ``` using assms unfolding simple_function_def by auto ``` hoelzl@38656 ` 216` ``` thus ?thesis unfolding * ``` hoelzl@38656 ` 217` ``` apply (rule finite_UN) ``` hoelzl@38656 ` 218` ``` using assms unfolding simple_function_def ``` hoelzl@38656 ` 219` ``` by (auto intro!: **) ``` hoelzl@35582 ` 220` ```qed ``` hoelzl@35582 ` 221` hoelzl@38656 ` 222` ```lemma (in sigma_algebra) borel_measurable_implies_simple_function_sequence: ``` hoelzl@38656 ` 223` ``` fixes u :: "'a \ pinfreal" ``` hoelzl@38656 ` 224` ``` assumes u: "u \ borel_measurable M" ``` hoelzl@38656 ` 225` ``` shows "\f. (\i. simple_function (f i) \ (\x\space M. f i x \ \)) \ f \ u" ``` hoelzl@35582 ` 226` ```proof - ``` hoelzl@38656 ` 227` ``` have "\f. \x j. (of_nat j \ u x \ f x j = j*2^j) \ ``` hoelzl@38656 ` 228` ``` (u x < of_nat j \ of_nat (f x j) \ u x * 2^j \ u x * 2^j < of_nat (Suc (f x j)))" ``` hoelzl@38656 ` 229` ``` (is "\f. \x j. ?P x j (f x j)") ``` hoelzl@38656 ` 230` ``` proof(rule choice, rule, rule choice, rule) ``` hoelzl@38656 ` 231` ``` fix x j show "\n. ?P x j n" ``` hoelzl@38656 ` 232` ``` proof cases ``` hoelzl@38656 ` 233` ``` assume *: "u x < of_nat j" ``` hoelzl@38656 ` 234` ``` then obtain r where r: "u x = Real r" "0 \ r" by (cases "u x") auto ``` hoelzl@38656 ` 235` ``` from reals_Archimedean6a[of "r * 2^j"] ``` hoelzl@38656 ` 236` ``` obtain n :: nat where "real n \ r * 2 ^ j" "r * 2 ^ j < real (Suc n)" ``` hoelzl@38656 ` 237` ``` using `0 \ r` by (auto simp: zero_le_power zero_le_mult_iff) ``` hoelzl@38656 ` 238` ``` thus ?thesis using r * by (auto intro!: exI[of _ n]) ``` hoelzl@38656 ` 239` ``` qed auto ``` hoelzl@35582 ` 240` ``` qed ``` hoelzl@38656 ` 241` ``` then obtain f where top: "\j x. of_nat j \ u x \ f x j = j*2^j" and ``` hoelzl@38656 ` 242` ``` upper: "\j x. u x < of_nat j \ of_nat (f x j) \ u x * 2^j" and ``` hoelzl@38656 ` 243` ``` lower: "\j x. u x < of_nat j \ u x * 2^j < of_nat (Suc (f x j))" by blast ``` hoelzl@35582 ` 244` hoelzl@38656 ` 245` ``` { fix j x P ``` hoelzl@38656 ` 246` ``` assume 1: "of_nat j \ u x \ P (j * 2^j)" ``` hoelzl@38656 ` 247` ``` assume 2: "\k. \ u x < of_nat j ; of_nat k \ u x * 2^j ; u x * 2^j < of_nat (Suc k) \ \ P k" ``` hoelzl@38656 ` 248` ``` have "P (f x j)" ``` hoelzl@38656 ` 249` ``` proof cases ``` hoelzl@38656 ` 250` ``` assume "of_nat j \ u x" thus "P (f x j)" ``` hoelzl@38656 ` 251` ``` using top[of j x] 1 by auto ``` hoelzl@38656 ` 252` ``` next ``` hoelzl@38656 ` 253` ``` assume "\ of_nat j \ u x" ``` hoelzl@38656 ` 254` ``` hence "u x < of_nat j" "of_nat (f x j) \ u x * 2^j" "u x * 2^j < of_nat (Suc (f x j))" ``` hoelzl@38656 ` 255` ``` using upper lower by auto ``` hoelzl@38656 ` 256` ``` from 2[OF this] show "P (f x j)" . ``` hoelzl@38656 ` 257` ``` qed } ``` hoelzl@38656 ` 258` ``` note fI = this ``` hoelzl@38656 ` 259` hoelzl@38656 ` 260` ``` { fix j x ``` hoelzl@38656 ` 261` ``` have "f x j = j * 2 ^ j \ of_nat j \ u x" ``` hoelzl@38656 ` 262` ``` by (rule fI, simp, cases "u x") (auto split: split_if_asm) } ``` hoelzl@38656 ` 263` ``` note f_eq = this ``` hoelzl@35582 ` 264` hoelzl@38656 ` 265` ``` { fix j x ``` hoelzl@38656 ` 266` ``` have "f x j \ j * 2 ^ j" ``` hoelzl@38656 ` 267` ``` proof (rule fI) ``` hoelzl@38656 ` 268` ``` fix k assume *: "u x < of_nat j" ``` hoelzl@38656 ` 269` ``` assume "of_nat k \ u x * 2 ^ j" ``` hoelzl@38656 ` 270` ``` also have "\ \ of_nat (j * 2^j)" ``` hoelzl@38656 ` 271` ``` using * by (cases "u x") (auto simp: zero_le_mult_iff) ``` hoelzl@38656 ` 272` ``` finally show "k \ j*2^j" by (auto simp del: real_of_nat_mult) ``` hoelzl@38656 ` 273` ``` qed simp } ``` hoelzl@38656 ` 274` ``` note f_upper = this ``` hoelzl@35582 ` 275` hoelzl@38656 ` 276` ``` let "?g j x" = "of_nat (f x j) / 2^j :: pinfreal" ``` hoelzl@38656 ` 277` ``` show ?thesis unfolding simple_function_def isoton_fun_expand unfolding isoton_def ``` hoelzl@38656 ` 278` ``` proof (safe intro!: exI[of _ ?g]) ``` hoelzl@38656 ` 279` ``` fix j ``` hoelzl@38656 ` 280` ``` have *: "?g j ` space M \ (\x. of_nat x / 2^j) ` {..j * 2^j}" ``` hoelzl@38656 ` 281` ``` using f_upper by auto ``` hoelzl@38656 ` 282` ``` thus "finite (?g j ` space M)" by (rule finite_subset) auto ``` hoelzl@38656 ` 283` ``` next ``` hoelzl@38656 ` 284` ``` fix j t assume "t \ space M" ``` hoelzl@38656 ` 285` ``` have **: "?g j -` {?g j t} \ space M = {x \ space M. f t j = f x j}" ``` hoelzl@38656 ` 286` ``` by (auto simp: power_le_zero_eq Real_eq_Real mult_le_0_iff) ``` hoelzl@35582 ` 287` hoelzl@38656 ` 288` ``` show "?g j -` {?g j t} \ space M \ sets M" ``` hoelzl@38656 ` 289` ``` proof cases ``` hoelzl@38656 ` 290` ``` assume "of_nat j \ u t" ``` hoelzl@38656 ` 291` ``` hence "?g j -` {?g j t} \ space M = {x\space M. of_nat j \ u x}" ``` hoelzl@38656 ` 292` ``` unfolding ** f_eq[symmetric] by auto ``` hoelzl@38656 ` 293` ``` thus "?g j -` {?g j t} \ space M \ sets M" ``` hoelzl@38656 ` 294` ``` using u by auto ``` hoelzl@35582 ` 295` ``` next ``` hoelzl@38656 ` 296` ``` assume not_t: "\ of_nat j \ u t" ``` hoelzl@38656 ` 297` ``` hence less: "f t j < j*2^j" using f_eq[symmetric] `f t j \ j*2^j` by auto ``` hoelzl@38656 ` 298` ``` have split_vimage: "?g j -` {?g j t} \ space M = ``` hoelzl@38656 ` 299` ``` {x\space M. of_nat (f t j)/2^j \ u x} \ {x\space M. u x < of_nat (Suc (f t j))/2^j}" ``` hoelzl@38656 ` 300` ``` unfolding ** ``` hoelzl@38656 ` 301` ``` proof safe ``` hoelzl@38656 ` 302` ``` fix x assume [simp]: "f t j = f x j" ``` hoelzl@38656 ` 303` ``` have *: "\ of_nat j \ u x" using not_t f_eq[symmetric] by simp ``` hoelzl@38656 ` 304` ``` hence "of_nat (f t j) \ u x * 2^j \ u x * 2^j < of_nat (Suc (f t j))" ``` hoelzl@38656 ` 305` ``` using upper lower by auto ``` hoelzl@38656 ` 306` ``` hence "of_nat (f t j) / 2^j \ u x \ u x < of_nat (Suc (f t j))/2^j" using * ``` hoelzl@38656 ` 307` ``` by (cases "u x") (auto simp: zero_le_mult_iff power_le_zero_eq divide_real_def[symmetric] field_simps) ``` hoelzl@38656 ` 308` ``` thus "of_nat (f t j) / 2^j \ u x" "u x < of_nat (Suc (f t j))/2^j" by auto ``` hoelzl@38656 ` 309` ``` next ``` hoelzl@38656 ` 310` ``` fix x ``` hoelzl@38656 ` 311` ``` assume "of_nat (f t j) / 2^j \ u x" "u x < of_nat (Suc (f t j))/2^j" ``` hoelzl@38656 ` 312` ``` hence "of_nat (f t j) \ u x * 2 ^ j \ u x * 2 ^ j < of_nat (Suc (f t j))" ``` hoelzl@38656 ` 313` ``` by (cases "u x") (auto simp: zero_le_mult_iff power_le_zero_eq divide_real_def[symmetric] field_simps) ``` hoelzl@38656 ` 314` ``` hence 1: "of_nat (f t j) \ u x * 2 ^ j" and 2: "u x * 2 ^ j < of_nat (Suc (f t j))" by auto ``` hoelzl@38656 ` 315` ``` note 2 ``` hoelzl@38656 ` 316` ``` also have "\ \ of_nat (j*2^j)" ``` hoelzl@38656 ` 317` ``` using less by (auto simp: zero_le_mult_iff simp del: real_of_nat_mult) ``` hoelzl@38656 ` 318` ``` finally have bound_ux: "u x < of_nat j" ``` hoelzl@38656 ` 319` ``` by (cases "u x") (auto simp: zero_le_mult_iff power_le_zero_eq) ``` hoelzl@38656 ` 320` ``` show "f t j = f x j" ``` hoelzl@38656 ` 321` ``` proof (rule antisym) ``` hoelzl@38656 ` 322` ``` from 1 lower[OF bound_ux] ``` hoelzl@38656 ` 323` ``` show "f t j \ f x j" by (cases "u x") (auto split: split_if_asm) ``` hoelzl@38656 ` 324` ``` from upper[OF bound_ux] 2 ``` hoelzl@38656 ` 325` ``` show "f x j \ f t j" by (cases "u x") (auto split: split_if_asm) ``` hoelzl@38656 ` 326` ``` qed ``` hoelzl@38656 ` 327` ``` qed ``` hoelzl@38656 ` 328` ``` show ?thesis unfolding split_vimage using u by auto ``` hoelzl@35582 ` 329` ``` qed ``` hoelzl@38656 ` 330` ``` next ``` hoelzl@38656 ` 331` ``` fix j t assume "?g j t = \" thus False by (auto simp: power_le_zero_eq) ``` hoelzl@38656 ` 332` ``` next ``` hoelzl@38656 ` 333` ``` fix t ``` hoelzl@38656 ` 334` ``` { fix i ``` hoelzl@38656 ` 335` ``` have "f t i * 2 \ f t (Suc i)" ``` hoelzl@38656 ` 336` ``` proof (rule fI) ``` hoelzl@38656 ` 337` ``` assume "of_nat (Suc i) \ u t" ``` hoelzl@38656 ` 338` ``` hence "of_nat i \ u t" by (cases "u t") auto ``` hoelzl@38656 ` 339` ``` thus "f t i * 2 \ Suc i * 2 ^ Suc i" unfolding f_eq[symmetric] by simp ``` hoelzl@38656 ` 340` ``` next ``` hoelzl@38656 ` 341` ``` fix k ``` hoelzl@38656 ` 342` ``` assume *: "u t * 2 ^ Suc i < of_nat (Suc k)" ``` hoelzl@38656 ` 343` ``` show "f t i * 2 \ k" ``` hoelzl@38656 ` 344` ``` proof (rule fI) ``` hoelzl@38656 ` 345` ``` assume "of_nat i \ u t" ``` hoelzl@38656 ` 346` ``` hence "of_nat (i * 2^Suc i) \ u t * 2^Suc i" ``` hoelzl@38656 ` 347` ``` by (cases "u t") (auto simp: zero_le_mult_iff power_le_zero_eq) ``` hoelzl@38656 ` 348` ``` also have "\ < of_nat (Suc k)" using * by auto ``` hoelzl@38656 ` 349` ``` finally show "i * 2 ^ i * 2 \ k" ``` hoelzl@38656 ` 350` ``` by (auto simp del: real_of_nat_mult) ``` hoelzl@38656 ` 351` ``` next ``` hoelzl@38656 ` 352` ``` fix j assume "of_nat j \ u t * 2 ^ i" ``` hoelzl@38656 ` 353` ``` with * show "j * 2 \ k" by (cases "u t") (auto simp: zero_le_mult_iff power_le_zero_eq) ``` hoelzl@38656 ` 354` ``` qed ``` hoelzl@38656 ` 355` ``` qed ``` hoelzl@38656 ` 356` ``` thus "?g i t \ ?g (Suc i) t" ``` hoelzl@38656 ` 357` ``` by (auto simp: zero_le_mult_iff power_le_zero_eq divide_real_def[symmetric] field_simps) } ``` hoelzl@38656 ` 358` ``` hence mono: "mono (\i. ?g i t)" unfolding mono_iff_le_Suc by auto ``` hoelzl@35582 ` 359` hoelzl@38656 ` 360` ``` show "(SUP j. of_nat (f t j) / 2 ^ j) = u t" ``` hoelzl@38656 ` 361` ``` proof (rule pinfreal_SUPI) ``` hoelzl@38656 ` 362` ``` fix j show "of_nat (f t j) / 2 ^ j \ u t" ``` hoelzl@38656 ` 363` ``` proof (rule fI) ``` hoelzl@38656 ` 364` ``` assume "of_nat j \ u t" thus "of_nat (j * 2 ^ j) / 2 ^ j \ u t" ``` hoelzl@38656 ` 365` ``` by (cases "u t") (auto simp: power_le_zero_eq divide_real_def[symmetric] field_simps) ``` hoelzl@38656 ` 366` ``` next ``` hoelzl@38656 ` 367` ``` fix k assume "of_nat k \ u t * 2 ^ j" ``` hoelzl@38656 ` 368` ``` thus "of_nat k / 2 ^ j \ u t" ``` hoelzl@38656 ` 369` ``` by (cases "u t") ``` hoelzl@38656 ` 370` ``` (auto simp: power_le_zero_eq divide_real_def[symmetric] field_simps zero_le_mult_iff) ``` hoelzl@38656 ` 371` ``` qed ``` hoelzl@38656 ` 372` ``` next ``` hoelzl@38656 ` 373` ``` fix y :: pinfreal assume *: "\j. j \ UNIV \ of_nat (f t j) / 2 ^ j \ y" ``` hoelzl@38656 ` 374` ``` show "u t \ y" ``` hoelzl@38656 ` 375` ``` proof (cases "u t") ``` hoelzl@38656 ` 376` ``` case (preal r) ``` hoelzl@38656 ` 377` ``` show ?thesis ``` hoelzl@38656 ` 378` ``` proof (rule ccontr) ``` hoelzl@38656 ` 379` ``` assume "\ u t \ y" ``` hoelzl@38656 ` 380` ``` then obtain p where p: "y = Real p" "0 \ p" "p < r" using preal by (cases y) auto ``` hoelzl@38656 ` 381` ``` with LIMSEQ_inverse_realpow_zero[of 2, unfolded LIMSEQ_iff, rule_format, of "r - p"] ``` hoelzl@38656 ` 382` ``` obtain n where n: "\N. n \ N \ inverse (2^N) < r - p" by auto ``` hoelzl@38656 ` 383` ``` let ?N = "max n (natfloor r + 1)" ``` hoelzl@38656 ` 384` ``` have "u t < of_nat ?N" "n \ ?N" ``` hoelzl@38656 ` 385` ``` using ge_natfloor_plus_one_imp_gt[of r n] preal ``` hoelzl@38705 ` 386` ``` using real_natfloor_add_one_gt ``` hoelzl@38705 ` 387` ``` by (auto simp: max_def real_of_nat_Suc) ``` hoelzl@38656 ` 388` ``` from lower[OF this(1)] ``` hoelzl@38656 ` 389` ``` have "r < (real (f t ?N) + 1) / 2 ^ ?N" unfolding less_divide_eq ``` hoelzl@38656 ` 390` ``` using preal by (auto simp add: power_le_zero_eq zero_le_mult_iff real_of_nat_Suc split: split_if_asm) ``` hoelzl@38656 ` 391` ``` hence "u t < of_nat (f t ?N) / 2 ^ ?N + 1 / 2 ^ ?N" ``` hoelzl@38656 ` 392` ``` using preal by (auto simp: field_simps divide_real_def[symmetric]) ``` hoelzl@38656 ` 393` ``` with n[OF `n \ ?N`] p preal *[of ?N] ``` hoelzl@38656 ` 394` ``` show False ``` hoelzl@38656 ` 395` ``` by (cases "f t ?N") (auto simp: power_le_zero_eq split: split_if_asm) ``` hoelzl@38656 ` 396` ``` qed ``` hoelzl@38656 ` 397` ``` next ``` hoelzl@38656 ` 398` ``` case infinite ``` hoelzl@38656 ` 399` ``` { fix j have "f t j = j*2^j" using top[of j t] infinite by simp ``` hoelzl@38656 ` 400` ``` hence "of_nat j \ y" using *[of j] ``` hoelzl@38656 ` 401` ``` by (cases y) (auto simp: power_le_zero_eq zero_le_mult_iff field_simps) } ``` hoelzl@38656 ` 402` ``` note all_less_y = this ``` hoelzl@38656 ` 403` ``` show ?thesis unfolding infinite ``` hoelzl@38656 ` 404` ``` proof (rule ccontr) ``` hoelzl@38656 ` 405` ``` assume "\ \ \ y" then obtain r where r: "y = Real r" "0 \ r" by (cases y) auto ``` hoelzl@38656 ` 406` ``` moreover obtain n ::nat where "r < real n" using ex_less_of_nat by (auto simp: real_eq_of_nat) ``` hoelzl@38656 ` 407` ``` with all_less_y[of n] r show False by auto ``` hoelzl@38656 ` 408` ``` qed ``` hoelzl@38656 ` 409` ``` qed ``` hoelzl@38656 ` 410` ``` qed ``` hoelzl@35582 ` 411` ``` qed ``` hoelzl@35582 ` 412` ```qed ``` hoelzl@35582 ` 413` hoelzl@38656 ` 414` ```lemma (in sigma_algebra) borel_measurable_implies_simple_function_sequence': ``` hoelzl@38656 ` 415` ``` fixes u :: "'a \ pinfreal" ``` hoelzl@38656 ` 416` ``` assumes "u \ borel_measurable M" ``` hoelzl@38656 ` 417` ``` obtains (x) f where "f \ u" "\i. simple_function (f i)" "\i. \\f i`space M" ``` hoelzl@35582 ` 418` ```proof - ``` hoelzl@38656 ` 419` ``` from borel_measurable_implies_simple_function_sequence[OF assms] ``` hoelzl@38656 ` 420` ``` obtain f where x: "\i. simple_function (f i)" "f \ u" ``` hoelzl@38656 ` 421` ``` and fin: "\i. \x. x\space M \ f i x \ \" by auto ``` hoelzl@38656 ` 422` ``` { fix i from fin[of _ i] have "\ \ f i`space M" by fastsimp } ``` hoelzl@38656 ` 423` ``` with x show thesis by (auto intro!: that[of f]) ``` hoelzl@38656 ` 424` ```qed ``` hoelzl@38656 ` 425` hoelzl@39092 ` 426` ```lemma (in sigma_algebra) simple_function_eq_borel_measurable: ``` hoelzl@39092 ` 427` ``` fixes f :: "'a \ pinfreal" ``` hoelzl@39092 ` 428` ``` shows "simple_function f \ ``` hoelzl@39092 ` 429` ``` finite (f`space M) \ f \ borel_measurable M" ``` hoelzl@39092 ` 430` ``` using simple_function_borel_measurable[of f] ``` hoelzl@39092 ` 431` ``` borel_measurable_simple_function[of f] ``` hoelzl@39092 ` 432` ``` by (fastsimp simp: simple_function_def) ``` hoelzl@39092 ` 433` hoelzl@39092 ` 434` ```lemma (in measure_space) simple_function_restricted: ``` hoelzl@39092 ` 435` ``` fixes f :: "'a \ pinfreal" assumes "A \ sets M" ``` hoelzl@39092 ` 436` ``` shows "sigma_algebra.simple_function (restricted_space A) f \ simple_function (\x. f x * indicator A x)" ``` hoelzl@39092 ` 437` ``` (is "sigma_algebra.simple_function ?R f \ simple_function ?f") ``` hoelzl@39092 ` 438` ```proof - ``` hoelzl@39092 ` 439` ``` interpret R: sigma_algebra ?R by (rule restricted_sigma_algebra[OF `A \ sets M`]) ``` hoelzl@39092 ` 440` ``` have "finite (f`A) \ finite (?f`space M)" ``` hoelzl@39092 ` 441` ``` proof cases ``` hoelzl@39092 ` 442` ``` assume "A = space M" ``` hoelzl@39092 ` 443` ``` then have "f`A = ?f`space M" by (fastsimp simp: image_iff) ``` hoelzl@39092 ` 444` ``` then show ?thesis by simp ``` hoelzl@39092 ` 445` ``` next ``` hoelzl@39092 ` 446` ``` assume "A \ space M" ``` hoelzl@39092 ` 447` ``` then obtain x where x: "x \ space M" "x \ A" ``` hoelzl@39092 ` 448` ``` using sets_into_space `A \ sets M` by auto ``` hoelzl@39092 ` 449` ``` have *: "?f`space M = f`A \ {0}" ``` hoelzl@39092 ` 450` ``` proof (auto simp add: image_iff) ``` hoelzl@39092 ` 451` ``` show "\x\space M. f x = 0 \ indicator A x = 0" ``` hoelzl@39092 ` 452` ``` using x by (auto intro!: bexI[of _ x]) ``` hoelzl@39092 ` 453` ``` next ``` hoelzl@39092 ` 454` ``` fix x assume "x \ A" ``` hoelzl@39092 ` 455` ``` then show "\y\space M. f x = f y * indicator A y" ``` hoelzl@39092 ` 456` ``` using `A \ sets M` sets_into_space by (auto intro!: bexI[of _ x]) ``` hoelzl@39092 ` 457` ``` next ``` hoelzl@39092 ` 458` ``` fix x ``` hoelzl@39092 ` 459` ``` assume "indicator A x \ (0::pinfreal)" ``` hoelzl@39092 ` 460` ``` then have "x \ A" by (auto simp: indicator_def split: split_if_asm) ``` hoelzl@39092 ` 461` ``` moreover assume "x \ space M" "\y\A. ?f x \ f y" ``` hoelzl@39092 ` 462` ``` ultimately show "f x = 0" by auto ``` hoelzl@39092 ` 463` ``` qed ``` hoelzl@39092 ` 464` ``` then show ?thesis by auto ``` hoelzl@39092 ` 465` ``` qed ``` hoelzl@39092 ` 466` ``` then show ?thesis ``` hoelzl@39092 ` 467` ``` unfolding simple_function_eq_borel_measurable ``` hoelzl@39092 ` 468` ``` R.simple_function_eq_borel_measurable ``` hoelzl@39092 ` 469` ``` unfolding borel_measurable_restricted[OF `A \ sets M`] ``` hoelzl@39092 ` 470` ``` by auto ``` hoelzl@39092 ` 471` ```qed ``` hoelzl@39092 ` 472` hoelzl@39092 ` 473` ```lemma (in sigma_algebra) simple_function_subalgebra: ``` hoelzl@39092 ` 474` ``` assumes "sigma_algebra.simple_function (M\sets:=N\) f" ``` hoelzl@39092 ` 475` ``` and N_subalgebra: "N \ sets M" "sigma_algebra (M\sets:=N\)" ``` hoelzl@39092 ` 476` ``` shows "simple_function f" ``` hoelzl@39092 ` 477` ``` using assms ``` hoelzl@39092 ` 478` ``` unfolding simple_function_def ``` hoelzl@39092 ` 479` ``` unfolding sigma_algebra.simple_function_def[OF N_subalgebra(2)] ``` hoelzl@39092 ` 480` ``` by auto ``` hoelzl@39092 ` 481` hoelzl@40859 ` 482` ```lemma (in sigma_algebra) simple_function_vimage: ``` hoelzl@40859 ` 483` ``` fixes g :: "'a \ pinfreal" and f :: "'d \ 'a" ``` hoelzl@40859 ` 484` ``` assumes g: "simple_function g" and f: "f \ S \ space M" ``` hoelzl@40859 ` 485` ``` shows "sigma_algebra.simple_function (vimage_algebra S f) (\x. g (f x))" ``` hoelzl@40859 ` 486` ```proof - ``` hoelzl@40859 ` 487` ``` have subset: "(\x. g (f x)) ` S \ g ` space M" ``` hoelzl@40859 ` 488` ``` using f by auto ``` hoelzl@40859 ` 489` ``` interpret V: sigma_algebra "vimage_algebra S f" ``` hoelzl@40859 ` 490` ``` using f by (rule sigma_algebra_vimage) ``` hoelzl@40859 ` 491` ``` show ?thesis using g ``` hoelzl@40859 ` 492` ``` unfolding simple_function_eq_borel_measurable ``` hoelzl@40859 ` 493` ``` unfolding V.simple_function_eq_borel_measurable ``` hoelzl@40859 ` 494` ``` using measurable_vimage[OF _ f, of g borel] ``` hoelzl@40859 ` 495` ``` using finite_subset[OF subset] by auto ``` hoelzl@40859 ` 496` ```qed ``` hoelzl@40859 ` 497` hoelzl@38656 ` 498` ```section "Simple integral" ``` hoelzl@38656 ` 499` hoelzl@38656 ` 500` ```definition (in measure_space) ``` hoelzl@38656 ` 501` ``` "simple_integral f = (\x \ f ` space M. x * \ (f -` {x} \ space M))" ``` hoelzl@35582 ` 502` hoelzl@38656 ` 503` ```lemma (in measure_space) simple_integral_cong: ``` hoelzl@38656 ` 504` ``` assumes "\t. t \ space M \ f t = g t" ``` hoelzl@38656 ` 505` ``` shows "simple_integral f = simple_integral g" ``` hoelzl@38656 ` 506` ```proof - ``` hoelzl@38656 ` 507` ``` have "f ` space M = g ` space M" ``` hoelzl@38656 ` 508` ``` "\x. f -` {x} \ space M = g -` {x} \ space M" ``` hoelzl@38656 ` 509` ``` using assms by (auto intro!: image_eqI) ``` hoelzl@38656 ` 510` ``` thus ?thesis unfolding simple_integral_def by simp ``` hoelzl@38656 ` 511` ```qed ``` hoelzl@38656 ` 512` hoelzl@40859 ` 513` ```lemma (in measure_space) simple_integral_cong_measure: ``` hoelzl@40859 ` 514` ``` assumes "\A. A \ sets M \ \ A = \ A" and "simple_function f" ``` hoelzl@40859 ` 515` ``` shows "measure_space.simple_integral M \ f = simple_integral f" ``` hoelzl@40859 ` 516` ```proof - ``` hoelzl@40859 ` 517` ``` interpret v: measure_space M \ ``` hoelzl@40859 ` 518` ``` by (rule measure_space_cong) fact ``` hoelzl@40859 ` 519` ``` have "\x. x \ space M \ f -` {f x} \ space M \ sets M" ``` hoelzl@40859 ` 520` ``` using `simple_function f`[THEN simple_functionD(2)] by auto ``` hoelzl@40859 ` 521` ``` with assms show ?thesis ``` hoelzl@40859 ` 522` ``` unfolding simple_integral_def v.simple_integral_def ``` hoelzl@40859 ` 523` ``` by (auto intro!: setsum_cong) ``` hoelzl@40859 ` 524` ```qed ``` hoelzl@40859 ` 525` hoelzl@38656 ` 526` ```lemma (in measure_space) simple_integral_const[simp]: ``` hoelzl@38656 ` 527` ``` "simple_integral (\x. c) = c * \ (space M)" ``` hoelzl@38656 ` 528` ```proof (cases "space M = {}") ``` hoelzl@38656 ` 529` ``` case True thus ?thesis unfolding simple_integral_def by simp ``` hoelzl@38656 ` 530` ```next ``` hoelzl@38656 ` 531` ``` case False hence "(\x. c) ` space M = {c}" by auto ``` hoelzl@38656 ` 532` ``` thus ?thesis unfolding simple_integral_def by simp ``` hoelzl@35582 ` 533` ```qed ``` hoelzl@35582 ` 534` hoelzl@38656 ` 535` ```lemma (in measure_space) simple_function_partition: ``` hoelzl@38656 ` 536` ``` assumes "simple_function f" and "simple_function g" ``` haftmann@39910 ` 537` ``` shows "simple_integral f = (\A\(\x. f -` {f x} \ g -` {g x} \ space M) ` space M. the_elem (f`A) * \ A)" ``` hoelzl@38656 ` 538` ``` (is "_ = setsum _ (?p ` space M)") ``` hoelzl@38656 ` 539` ```proof- ``` hoelzl@38656 ` 540` ``` let "?sub x" = "?p ` (f -` {x} \ space M)" ``` hoelzl@38656 ` 541` ``` let ?SIGMA = "Sigma (f`space M) ?sub" ``` hoelzl@35582 ` 542` hoelzl@38656 ` 543` ``` have [intro]: ``` hoelzl@38656 ` 544` ``` "finite (f ` space M)" ``` hoelzl@38656 ` 545` ``` "finite (g ` space M)" ``` hoelzl@38656 ` 546` ``` using assms unfolding simple_function_def by simp_all ``` hoelzl@38656 ` 547` hoelzl@38656 ` 548` ``` { fix A ``` hoelzl@38656 ` 549` ``` have "?p ` (A \ space M) \ ``` hoelzl@38656 ` 550` ``` (\(x,y). f -` {x} \ g -` {y} \ space M) ` (f`space M \ g`space M)" ``` hoelzl@38656 ` 551` ``` by auto ``` hoelzl@38656 ` 552` ``` hence "finite (?p ` (A \ space M))" ``` nipkow@40786 ` 553` ``` by (rule finite_subset) auto } ``` hoelzl@38656 ` 554` ``` note this[intro, simp] ``` hoelzl@35582 ` 555` hoelzl@38656 ` 556` ``` { fix x assume "x \ space M" ``` hoelzl@38656 ` 557` ``` have "\(?sub (f x)) = (f -` {f x} \ space M)" by auto ``` hoelzl@38656 ` 558` ``` moreover { ``` hoelzl@38656 ` 559` ``` fix x y ``` hoelzl@38656 ` 560` ``` have *: "f -` {f x} \ g -` {g x} \ space M ``` hoelzl@38656 ` 561` ``` = (f -` {f x} \ space M) \ (g -` {g x} \ space M)" by auto ``` hoelzl@38656 ` 562` ``` assume "x \ space M" "y \ space M" ``` hoelzl@38656 ` 563` ``` hence "f -` {f x} \ g -` {g x} \ space M \ sets M" ``` hoelzl@38656 ` 564` ``` using assms unfolding simple_function_def * by auto } ``` hoelzl@38656 ` 565` ``` ultimately ``` hoelzl@38656 ` 566` ``` have "\ (f -` {f x} \ space M) = setsum (\) (?sub (f x))" ``` hoelzl@38656 ` 567` ``` by (subst measure_finitely_additive) auto } ``` hoelzl@38656 ` 568` ``` hence "simple_integral f = (\(x,A)\?SIGMA. x * \ A)" ``` hoelzl@38656 ` 569` ``` unfolding simple_integral_def ``` hoelzl@38656 ` 570` ``` by (subst setsum_Sigma[symmetric], ``` hoelzl@38656 ` 571` ``` auto intro!: setsum_cong simp: setsum_right_distrib[symmetric]) ``` haftmann@39910 ` 572` ``` also have "\ = (\A\?p ` space M. the_elem (f`A) * \ A)" ``` hoelzl@38656 ` 573` ``` proof - ``` hoelzl@38656 ` 574` ``` have [simp]: "\x. x \ space M \ f ` ?p x = {f x}" by (auto intro!: imageI) ``` haftmann@39910 ` 575` ``` have "(\A. (the_elem (f ` A), A)) ` ?p ` space M ``` hoelzl@38656 ` 576` ``` = (\x. (f x, ?p x)) ` space M" ``` hoelzl@38656 ` 577` ``` proof safe ``` hoelzl@38656 ` 578` ``` fix x assume "x \ space M" ``` haftmann@39910 ` 579` ``` thus "(f x, ?p x) \ (\A. (the_elem (f`A), A)) ` ?p ` space M" ``` hoelzl@38656 ` 580` ``` by (auto intro!: image_eqI[of _ _ "?p x"]) ``` hoelzl@38656 ` 581` ``` qed auto ``` hoelzl@38656 ` 582` ``` thus ?thesis ``` haftmann@39910 ` 583` ``` apply (auto intro!: setsum_reindex_cong[of "\A. (the_elem (f`A), A)"] inj_onI) ``` hoelzl@38656 ` 584` ``` apply (rule_tac x="xa" in image_eqI) ``` hoelzl@38656 ` 585` ``` by simp_all ``` hoelzl@38656 ` 586` ``` qed ``` hoelzl@38656 ` 587` ``` finally show ?thesis . ``` hoelzl@35582 ` 588` ```qed ``` hoelzl@35582 ` 589` hoelzl@38656 ` 590` ```lemma (in measure_space) simple_integral_add[simp]: ``` hoelzl@38656 ` 591` ``` assumes "simple_function f" and "simple_function g" ``` hoelzl@38656 ` 592` ``` shows "simple_integral (\x. f x + g x) = simple_integral f + simple_integral g" ``` hoelzl@35582 ` 593` ```proof - ``` hoelzl@38656 ` 594` ``` { fix x let ?S = "g -` {g x} \ f -` {f x} \ space M" ``` hoelzl@38656 ` 595` ``` assume "x \ space M" ``` hoelzl@38656 ` 596` ``` hence "(\a. f a + g a) ` ?S = {f x + g x}" "f ` ?S = {f x}" "g ` ?S = {g x}" ``` hoelzl@38656 ` 597` ``` "(\x. (f x, g x)) -` {(f x, g x)} \ space M = ?S" ``` hoelzl@38656 ` 598` ``` by auto } ``` hoelzl@38656 ` 599` ``` thus ?thesis ``` hoelzl@38656 ` 600` ``` unfolding ``` hoelzl@38656 ` 601` ``` simple_function_partition[OF simple_function_add[OF assms] simple_function_Pair[OF assms]] ``` hoelzl@38656 ` 602` ``` simple_function_partition[OF `simple_function f` `simple_function g`] ``` hoelzl@38656 ` 603` ``` simple_function_partition[OF `simple_function g` `simple_function f`] ``` hoelzl@38656 ` 604` ``` apply (subst (3) Int_commute) ``` hoelzl@38656 ` 605` ``` by (auto simp add: field_simps setsum_addf[symmetric] intro!: setsum_cong) ``` hoelzl@35582 ` 606` ```qed ``` hoelzl@35582 ` 607` hoelzl@38656 ` 608` ```lemma (in measure_space) simple_integral_setsum[simp]: ``` hoelzl@38656 ` 609` ``` assumes "\i. i \ P \ simple_function (f i)" ``` hoelzl@38656 ` 610` ``` shows "simple_integral (\x. \i\P. f i x) = (\i\P. simple_integral (f i))" ``` hoelzl@38656 ` 611` ```proof cases ``` hoelzl@38656 ` 612` ``` assume "finite P" ``` hoelzl@38656 ` 613` ``` from this assms show ?thesis ``` hoelzl@38656 ` 614` ``` by induct (auto simp: simple_function_setsum simple_integral_add) ``` hoelzl@38656 ` 615` ```qed auto ``` hoelzl@38656 ` 616` hoelzl@38656 ` 617` ```lemma (in measure_space) simple_integral_mult[simp]: ``` hoelzl@38656 ` 618` ``` assumes "simple_function f" ``` hoelzl@38656 ` 619` ``` shows "simple_integral (\x. c * f x) = c * simple_integral f" ``` hoelzl@38656 ` 620` ```proof - ``` hoelzl@38656 ` 621` ``` note mult = simple_function_mult[OF simple_function_const[of c] assms] ``` hoelzl@38656 ` 622` ``` { fix x let ?S = "f -` {f x} \ (\x. c * f x) -` {c * f x} \ space M" ``` hoelzl@38656 ` 623` ``` assume "x \ space M" ``` hoelzl@38656 ` 624` ``` hence "(\x. c * f x) ` ?S = {c * f x}" "f ` ?S = {f x}" ``` hoelzl@38656 ` 625` ``` by auto } ``` hoelzl@38656 ` 626` ``` thus ?thesis ``` hoelzl@38656 ` 627` ``` unfolding simple_function_partition[OF mult assms] ``` hoelzl@38656 ` 628` ``` simple_function_partition[OF assms mult] ``` hoelzl@38656 ` 629` ``` by (auto simp: setsum_right_distrib field_simps intro!: setsum_cong) ``` hoelzl@35582 ` 630` ```qed ``` hoelzl@35582 ` 631` hoelzl@40859 ` 632` ```lemma (in measure_space) simple_integral_mono_AE: ``` hoelzl@40859 ` 633` ``` assumes "simple_function f" and "simple_function g" ``` hoelzl@40859 ` 634` ``` and mono: "AE x. f x \ g x" ``` hoelzl@40859 ` 635` ``` shows "simple_integral f \ simple_integral g" ``` hoelzl@40859 ` 636` ```proof - ``` hoelzl@40859 ` 637` ``` let "?S x" = "(g -` {g x} \ space M) \ (f -` {f x} \ space M)" ``` hoelzl@40859 ` 638` ``` have *: "\x. g -` {g x} \ f -` {f x} \ space M = ?S x" ``` hoelzl@40859 ` 639` ``` "\x. f -` {f x} \ g -` {g x} \ space M = ?S x" by auto ``` hoelzl@40859 ` 640` ``` show ?thesis ``` hoelzl@40859 ` 641` ``` unfolding * ``` hoelzl@40859 ` 642` ``` simple_function_partition[OF `simple_function f` `simple_function g`] ``` hoelzl@40859 ` 643` ``` simple_function_partition[OF `simple_function g` `simple_function f`] ``` hoelzl@40859 ` 644` ``` proof (safe intro!: setsum_mono) ``` hoelzl@40859 ` 645` ``` fix x assume "x \ space M" ``` hoelzl@40859 ` 646` ``` then have *: "f ` ?S x = {f x}" "g ` ?S x = {g x}" by auto ``` hoelzl@40859 ` 647` ``` show "the_elem (f`?S x) * \ (?S x) \ the_elem (g`?S x) * \ (?S x)" ``` hoelzl@40859 ` 648` ``` proof (cases "f x \ g x") ``` hoelzl@40859 ` 649` ``` case True then show ?thesis using * by (auto intro!: mult_right_mono) ``` hoelzl@40859 ` 650` ``` next ``` hoelzl@40859 ` 651` ``` case False ``` hoelzl@40859 ` 652` ``` obtain N where N: "{x\space M. \ f x \ g x} \ N" "N \ sets M" "\ N = 0" ``` hoelzl@40859 ` 653` ``` using mono by (auto elim!: AE_E) ``` hoelzl@40859 ` 654` ``` have "?S x \ N" using N `x \ space M` False by auto ``` hoelzl@40859 ` 655` ``` moreover have "?S x \ sets M" using assms `x \ space M` ``` hoelzl@40859 ` 656` ``` by (rule_tac Int) (auto intro!: simple_functionD(2)) ``` hoelzl@40859 ` 657` ``` ultimately have "\ (?S x) \ \ N" ``` hoelzl@40859 ` 658` ``` using `N \ sets M` by (auto intro!: measure_mono) ``` hoelzl@40859 ` 659` ``` then show ?thesis using `\ N = 0` by auto ``` hoelzl@40859 ` 660` ``` qed ``` hoelzl@40859 ` 661` ``` qed ``` hoelzl@40859 ` 662` ```qed ``` hoelzl@40859 ` 663` hoelzl@38656 ` 664` ```lemma (in measure_space) simple_integral_mono: ``` hoelzl@38656 ` 665` ``` assumes "simple_function f" and "simple_function g" ``` hoelzl@38656 ` 666` ``` and mono: "\ x. x \ space M \ f x \ g x" ``` hoelzl@38656 ` 667` ``` shows "simple_integral f \ simple_integral g" ``` hoelzl@40859 ` 668` ```proof (rule simple_integral_mono_AE[OF assms(1, 2)]) ``` hoelzl@40859 ` 669` ``` show "AE x. f x \ g x" ``` hoelzl@40859 ` 670` ``` using mono by (rule AE_cong) auto ``` hoelzl@35582 ` 671` ```qed ``` hoelzl@35582 ` 672` hoelzl@40859 ` 673` ```lemma (in measure_space) simple_integral_cong_AE: ``` hoelzl@40859 ` 674` ``` assumes "simple_function f" "simple_function g" and "AE x. f x = g x" ``` hoelzl@40859 ` 675` ``` shows "simple_integral f = simple_integral g" ``` hoelzl@40859 ` 676` ``` using assms by (auto simp: eq_iff intro!: simple_integral_mono_AE) ``` hoelzl@40859 ` 677` hoelzl@40859 ` 678` ```lemma (in measure_space) simple_integral_cong': ``` hoelzl@40859 ` 679` ``` assumes sf: "simple_function f" "simple_function g" ``` hoelzl@40859 ` 680` ``` and mea: "\ {x\space M. f x \ g x} = 0" ``` hoelzl@40859 ` 681` ``` shows "simple_integral f = simple_integral g" ``` hoelzl@40859 ` 682` ```proof (intro simple_integral_cong_AE sf AE_I) ``` hoelzl@40859 ` 683` ``` show "\ {x\space M. f x \ g x} = 0" by fact ``` hoelzl@40859 ` 684` ``` show "{x \ space M. f x \ g x} \ sets M" ``` hoelzl@40859 ` 685` ``` using sf[THEN borel_measurable_simple_function] by auto ``` hoelzl@40859 ` 686` ```qed simp ``` hoelzl@40859 ` 687` hoelzl@38656 ` 688` ```lemma (in measure_space) simple_integral_indicator: ``` hoelzl@38656 ` 689` ``` assumes "A \ sets M" ``` hoelzl@38656 ` 690` ``` assumes "simple_function f" ``` hoelzl@38656 ` 691` ``` shows "simple_integral (\x. f x * indicator A x) = ``` hoelzl@38656 ` 692` ``` (\x \ f ` space M. x * \ (f -` {x} \ space M \ A))" ``` hoelzl@38656 ` 693` ```proof cases ``` hoelzl@38656 ` 694` ``` assume "A = space M" ``` hoelzl@38656 ` 695` ``` moreover hence "simple_integral (\x. f x * indicator A x) = simple_integral f" ``` hoelzl@38656 ` 696` ``` by (auto intro!: simple_integral_cong) ``` hoelzl@38656 ` 697` ``` moreover have "\X. X \ space M \ space M = X \ space M" by auto ``` hoelzl@38656 ` 698` ``` ultimately show ?thesis by (simp add: simple_integral_def) ``` hoelzl@38656 ` 699` ```next ``` hoelzl@38656 ` 700` ``` assume "A \ space M" ``` hoelzl@38656 ` 701` ``` then obtain x where x: "x \ space M" "x \ A" using sets_into_space[OF assms(1)] by auto ``` hoelzl@38656 ` 702` ``` have I: "(\x. f x * indicator A x) ` space M = f ` A \ {0}" (is "?I ` _ = _") ``` hoelzl@35582 ` 703` ``` proof safe ``` hoelzl@38656 ` 704` ``` fix y assume "?I y \ f ` A" hence "y \ A" by auto thus "?I y = 0" by auto ``` hoelzl@38656 ` 705` ``` next ``` hoelzl@38656 ` 706` ``` fix y assume "y \ A" thus "f y \ ?I ` space M" ``` hoelzl@38656 ` 707` ``` using sets_into_space[OF assms(1)] by (auto intro!: image_eqI[of _ _ y]) ``` hoelzl@38656 ` 708` ``` next ``` hoelzl@38656 ` 709` ``` show "0 \ ?I ` space M" using x by (auto intro!: image_eqI[of _ _ x]) ``` hoelzl@35582 ` 710` ``` qed ``` hoelzl@38656 ` 711` ``` have *: "simple_integral (\x. f x * indicator A x) = ``` hoelzl@38656 ` 712` ``` (\x \ f ` space M \ {0}. x * \ (f -` {x} \ space M \ A))" ``` hoelzl@38656 ` 713` ``` unfolding simple_integral_def I ``` hoelzl@38656 ` 714` ``` proof (rule setsum_mono_zero_cong_left) ``` hoelzl@38656 ` 715` ``` show "finite (f ` space M \ {0})" ``` hoelzl@38656 ` 716` ``` using assms(2) unfolding simple_function_def by auto ``` hoelzl@38656 ` 717` ``` show "f ` A \ {0} \ f`space M \ {0}" ``` hoelzl@38656 ` 718` ``` using sets_into_space[OF assms(1)] by auto ``` hoelzl@40859 ` 719` ``` have "\x. f x \ f ` A \ f -` {f x} \ space M \ A = {}" ``` hoelzl@40859 ` 720` ``` by (auto simp: image_iff) ``` hoelzl@38656 ` 721` ``` thus "\i\f ` space M \ {0} - (f ` A \ {0}). ``` hoelzl@38656 ` 722` ``` i * \ (f -` {i} \ space M \ A) = 0" by auto ``` hoelzl@38656 ` 723` ``` next ``` hoelzl@38656 ` 724` ``` fix x assume "x \ f`A \ {0}" ``` hoelzl@38656 ` 725` ``` hence "x \ 0 \ ?I -` {x} \ space M = f -` {x} \ space M \ A" ``` hoelzl@38656 ` 726` ``` by (auto simp: indicator_def split: split_if_asm) ``` hoelzl@38656 ` 727` ``` thus "x * \ (?I -` {x} \ space M) = ``` hoelzl@38656 ` 728` ``` x * \ (f -` {x} \ space M \ A)" by (cases "x = 0") simp_all ``` hoelzl@38656 ` 729` ``` qed ``` hoelzl@38656 ` 730` ``` show ?thesis unfolding * ``` hoelzl@38656 ` 731` ``` using assms(2) unfolding simple_function_def ``` hoelzl@38656 ` 732` ``` by (auto intro!: setsum_mono_zero_cong_right) ``` hoelzl@38656 ` 733` ```qed ``` hoelzl@35582 ` 734` hoelzl@38656 ` 735` ```lemma (in measure_space) simple_integral_indicator_only[simp]: ``` hoelzl@38656 ` 736` ``` assumes "A \ sets M" ``` hoelzl@38656 ` 737` ``` shows "simple_integral (indicator A) = \ A" ``` hoelzl@38656 ` 738` ```proof cases ``` hoelzl@38656 ` 739` ``` assume "space M = {}" hence "A = {}" using sets_into_space[OF assms] by auto ``` hoelzl@38656 ` 740` ``` thus ?thesis unfolding simple_integral_def using `space M = {}` by auto ``` hoelzl@38656 ` 741` ```next ``` hoelzl@38656 ` 742` ``` assume "space M \ {}" hence "(\x. 1) ` space M = {1::pinfreal}" by auto ``` hoelzl@38656 ` 743` ``` thus ?thesis ``` hoelzl@38656 ` 744` ``` using simple_integral_indicator[OF assms simple_function_const[of 1]] ``` hoelzl@38656 ` 745` ``` using sets_into_space[OF assms] ``` hoelzl@38656 ` 746` ``` by (auto intro!: arg_cong[where f="\"]) ``` hoelzl@38656 ` 747` ```qed ``` hoelzl@35582 ` 748` hoelzl@38656 ` 749` ```lemma (in measure_space) simple_integral_null_set: ``` hoelzl@38656 ` 750` ``` assumes "simple_function u" "N \ null_sets" ``` hoelzl@38656 ` 751` ``` shows "simple_integral (\x. u x * indicator N x) = 0" ``` hoelzl@38656 ` 752` ```proof - ``` hoelzl@40859 ` 753` ``` have "AE x. indicator N x = (0 :: pinfreal)" ``` hoelzl@40859 ` 754` ``` using `N \ null_sets` by (auto simp: indicator_def intro!: AE_I[of _ N]) ``` hoelzl@40859 ` 755` ``` then have "simple_integral (\x. u x * indicator N x) = simple_integral (\x. 0)" ``` hoelzl@40859 ` 756` ``` using assms by (intro simple_integral_cong_AE) (auto intro!: AE_disjI2) ``` hoelzl@40859 ` 757` ``` then show ?thesis by simp ``` hoelzl@38656 ` 758` ```qed ``` hoelzl@35582 ` 759` hoelzl@40859 ` 760` ```lemma (in measure_space) simple_integral_cong_AE_mult_indicator: ``` hoelzl@40859 ` 761` ``` assumes sf: "simple_function f" and eq: "AE x. x \ S" and "S \ sets M" ``` hoelzl@40859 ` 762` ``` shows "simple_integral f = simple_integral (\x. f x * indicator S x)" ``` hoelzl@40859 ` 763` ```proof (rule simple_integral_cong_AE) ``` hoelzl@40859 ` 764` ``` show "simple_function f" by fact ``` hoelzl@40859 ` 765` ``` show "simple_function (\x. f x * indicator S x)" ``` hoelzl@40859 ` 766` ``` using sf `S \ sets M` by auto ``` hoelzl@40859 ` 767` ``` from eq show "AE x. f x = f x * indicator S x" ``` hoelzl@40859 ` 768` ``` by (rule AE_mp) simp ``` hoelzl@35582 ` 769` ```qed ``` hoelzl@35582 ` 770` hoelzl@39092 ` 771` ```lemma (in measure_space) simple_integral_restricted: ``` hoelzl@39092 ` 772` ``` assumes "A \ sets M" ``` hoelzl@39092 ` 773` ``` assumes sf: "simple_function (\x. f x * indicator A x)" ``` hoelzl@39092 ` 774` ``` shows "measure_space.simple_integral (restricted_space A) \ f = simple_integral (\x. f x * indicator A x)" ``` hoelzl@39092 ` 775` ``` (is "_ = simple_integral ?f") ``` hoelzl@39092 ` 776` ``` unfolding measure_space.simple_integral_def[OF restricted_measure_space[OF `A \ sets M`]] ``` hoelzl@39092 ` 777` ``` unfolding simple_integral_def ``` hoelzl@39092 ` 778` ```proof (simp, safe intro!: setsum_mono_zero_cong_left) ``` hoelzl@39092 ` 779` ``` from sf show "finite (?f ` space M)" ``` hoelzl@39092 ` 780` ``` unfolding simple_function_def by auto ``` hoelzl@39092 ` 781` ```next ``` hoelzl@39092 ` 782` ``` fix x assume "x \ A" ``` hoelzl@39092 ` 783` ``` then show "f x \ ?f ` space M" ``` hoelzl@39092 ` 784` ``` using sets_into_space `A \ sets M` by (auto intro!: image_eqI[of _ _ x]) ``` hoelzl@39092 ` 785` ```next ``` hoelzl@39092 ` 786` ``` fix x assume "x \ space M" "?f x \ f`A" ``` hoelzl@39092 ` 787` ``` then have "x \ A" by (auto simp: image_iff) ``` hoelzl@39092 ` 788` ``` then show "?f x * \ (?f -` {?f x} \ space M) = 0" by simp ``` hoelzl@39092 ` 789` ```next ``` hoelzl@39092 ` 790` ``` fix x assume "x \ A" ``` hoelzl@39092 ` 791` ``` then have "f x \ 0 \ ``` hoelzl@39092 ` 792` ``` f -` {f x} \ A = ?f -` {f x} \ space M" ``` hoelzl@39092 ` 793` ``` using `A \ sets M` sets_into_space ``` hoelzl@39092 ` 794` ``` by (auto simp: indicator_def split: split_if_asm) ``` hoelzl@39092 ` 795` ``` then show "f x * \ (f -` {f x} \ A) = ``` hoelzl@39092 ` 796` ``` f x * \ (?f -` {f x} \ space M)" ``` hoelzl@39092 ` 797` ``` unfolding pinfreal_mult_cancel_left by auto ``` hoelzl@39092 ` 798` ```qed ``` hoelzl@39092 ` 799` hoelzl@39092 ` 800` ```lemma (in measure_space) simple_integral_subalgebra[simp]: ``` hoelzl@39092 ` 801` ``` assumes "measure_space (M\sets := N\) \" ``` hoelzl@39092 ` 802` ``` shows "measure_space.simple_integral (M\sets := N\) \ = simple_integral" ``` hoelzl@39092 ` 803` ``` unfolding simple_integral_def_raw ``` hoelzl@39092 ` 804` ``` unfolding measure_space.simple_integral_def_raw[OF assms] by simp ``` hoelzl@39092 ` 805` hoelzl@40859 ` 806` ```lemma (in measure_space) simple_integral_vimage: ``` hoelzl@40859 ` 807` ``` fixes g :: "'a \ pinfreal" and f :: "'d \ 'a" ``` hoelzl@40859 ` 808` ``` assumes f: "bij_betw f S (space M)" ``` hoelzl@40859 ` 809` ``` shows "simple_integral g = ``` hoelzl@40859 ` 810` ``` measure_space.simple_integral (vimage_algebra S f) (\A. \ (f ` A)) (\x. g (f x))" ``` hoelzl@40859 ` 811` ``` (is "_ = measure_space.simple_integral ?T ?\ _") ``` hoelzl@40859 ` 812` ```proof - ``` hoelzl@40859 ` 813` ``` from f interpret T: measure_space ?T ?\ by (rule measure_space_isomorphic) ``` hoelzl@40859 ` 814` ``` have surj: "f`S = space M" ``` hoelzl@40859 ` 815` ``` using f unfolding bij_betw_def by simp ``` hoelzl@40859 ` 816` ``` have *: "(\x. g (f x)) ` S = g ` f ` S" by auto ``` hoelzl@40859 ` 817` ``` have **: "f`S = space M" using f unfolding bij_betw_def by auto ``` hoelzl@40859 ` 818` ``` { fix x assume "x \ space M" ``` hoelzl@40859 ` 819` ``` have "(f ` ((\x. g (f x)) -` {g x} \ S)) = ``` hoelzl@40859 ` 820` ``` (f ` (f -` (g -` {g x}) \ S))" by auto ``` hoelzl@40859 ` 821` ``` also have "f -` (g -` {g x}) \ S = f -` (g -` {g x} \ space M) \ S" ``` hoelzl@40859 ` 822` ``` using f unfolding bij_betw_def by auto ``` hoelzl@40859 ` 823` ``` also have "(f ` (f -` (g -` {g x} \ space M) \ S)) = g -` {g x} \ space M" ``` hoelzl@40859 ` 824` ``` using ** by (intro image_vimage_inter_eq) auto ``` hoelzl@40859 ` 825` ``` finally have "(f ` ((\x. g (f x)) -` {g x} \ S)) = g -` {g x} \ space M" by auto } ``` hoelzl@40859 ` 826` ``` then show ?thesis using assms ``` hoelzl@40859 ` 827` ``` unfolding simple_integral_def T.simple_integral_def bij_betw_def ``` hoelzl@40859 ` 828` ``` by (auto simp add: * intro!: setsum_cong) ``` hoelzl@40859 ` 829` ```qed ``` hoelzl@40859 ` 830` hoelzl@35692 ` 831` ```section "Continuous posititve integration" ``` hoelzl@35692 ` 832` hoelzl@38656 ` 833` ```definition (in measure_space) ``` hoelzl@38656 ` 834` ``` "positive_integral f = ``` hoelzl@38656 ` 835` ``` (SUP g : {g. simple_function g \ g \ f \ \ \ g`space M}. simple_integral g)" ``` hoelzl@35582 ` 836` hoelzl@40859 ` 837` ```lemma (in measure_space) positive_integral_cong_measure: ``` hoelzl@40859 ` 838` ``` assumes "\A. A \ sets M \ \ A = \ A" ``` hoelzl@40859 ` 839` ``` shows "measure_space.positive_integral M \ f = positive_integral f" ``` hoelzl@40859 ` 840` ```proof - ``` hoelzl@40859 ` 841` ``` interpret v: measure_space M \ ``` hoelzl@40859 ` 842` ``` by (rule measure_space_cong) fact ``` hoelzl@40859 ` 843` ``` with assms show ?thesis ``` hoelzl@40859 ` 844` ``` unfolding positive_integral_def v.positive_integral_def SUPR_def ``` hoelzl@40859 ` 845` ``` by (auto intro!: arg_cong[where f=Sup] image_cong ``` hoelzl@40859 ` 846` ``` simp: simple_integral_cong_measure[of \]) ``` hoelzl@40859 ` 847` ```qed ``` hoelzl@40859 ` 848` hoelzl@38656 ` 849` ```lemma (in measure_space) positive_integral_alt1: ``` hoelzl@38656 ` 850` ``` "positive_integral f = ``` hoelzl@38656 ` 851` ``` (SUP g : {g. simple_function g \ (\x\space M. g x \ f x \ g x \ \)}. simple_integral g)" ``` hoelzl@38656 ` 852` ``` unfolding positive_integral_def SUPR_def ``` hoelzl@38656 ` 853` ```proof (safe intro!: arg_cong[where f=Sup]) ``` hoelzl@38656 ` 854` ``` fix g let ?g = "\x. if x \ space M then g x else f x" ``` hoelzl@38656 ` 855` ``` assume "simple_function g" "\x\space M. g x \ f x \ g x \ \" ``` hoelzl@38656 ` 856` ``` hence "?g \ f" "simple_function ?g" "simple_integral g = simple_integral ?g" ``` hoelzl@38656 ` 857` ``` "\ \ g`space M" ``` hoelzl@38656 ` 858` ``` unfolding le_fun_def by (auto cong: simple_function_cong simple_integral_cong) ``` hoelzl@38656 ` 859` ``` thus "simple_integral g \ simple_integral ` {g. simple_function g \ g \ f \ \ \ g`space M}" ``` hoelzl@38656 ` 860` ``` by auto ``` hoelzl@38656 ` 861` ```next ``` hoelzl@38656 ` 862` ``` fix g assume "simple_function g" "g \ f" "\ \ g`space M" ``` hoelzl@38656 ` 863` ``` hence "simple_function g" "\x\space M. g x \ f x \ g x \ \" ``` hoelzl@38656 ` 864` ``` by (auto simp add: le_fun_def image_iff) ``` hoelzl@38656 ` 865` ``` thus "simple_integral g \ simple_integral ` {g. simple_function g \ (\x\space M. g x \ f x \ g x \ \)}" ``` hoelzl@38656 ` 866` ``` by auto ``` hoelzl@35582 ` 867` ```qed ``` hoelzl@35582 ` 868` hoelzl@38656 ` 869` ```lemma (in measure_space) positive_integral_alt: ``` hoelzl@38656 ` 870` ``` "positive_integral f = ``` hoelzl@38656 ` 871` ``` (SUP g : {g. simple_function g \ g \ f}. simple_integral g)" ``` hoelzl@38656 ` 872` ``` apply(rule order_class.antisym) unfolding positive_integral_def ``` hoelzl@38656 ` 873` ``` apply(rule SUPR_subset) apply blast apply(rule SUPR_mono_lim) ``` hoelzl@38656 ` 874` ```proof safe fix u assume u:"simple_function u" and uf:"u \ f" ``` hoelzl@38656 ` 875` ``` let ?u = "\n x. if u x = \ then Real (real (n::nat)) else u x" ``` hoelzl@38656 ` 876` ``` have su:"\n. simple_function (?u n)" using simple_function_compose1[OF u] . ``` hoelzl@38656 ` 877` ``` show "\b. \n. b n \ {g. simple_function g \ g \ f \ \ \ g ` space M} \ ``` hoelzl@38656 ` 878` ``` (\n. simple_integral (b n)) ----> simple_integral u" ``` hoelzl@38656 ` 879` ``` apply(rule_tac x="?u" in exI, safe) apply(rule su) ``` hoelzl@38656 ` 880` ``` proof- fix n::nat have "?u n \ u" unfolding le_fun_def by auto ``` hoelzl@38656 ` 881` ``` also note uf finally show "?u n \ f" . ``` hoelzl@38656 ` 882` ``` let ?s = "{x \ space M. u x = \}" ``` hoelzl@38656 ` 883` ``` show "(\n. simple_integral (?u n)) ----> simple_integral u" ``` hoelzl@38656 ` 884` ``` proof(cases "\ ?s = 0") ``` hoelzl@38656 ` 885` ``` case True have *:"\n. {x\space M. ?u n x \ u x} = {x\space M. u x = \}" by auto ``` hoelzl@38656 ` 886` ``` have *:"\n. simple_integral (?u n) = simple_integral u" ``` hoelzl@38656 ` 887` ``` apply(rule simple_integral_cong'[OF su u]) unfolding * True .. ``` hoelzl@38656 ` 888` ``` show ?thesis unfolding * by auto ``` hoelzl@38656 ` 889` ``` next case False note m0=this ``` hoelzl@38656 ` 890` ``` have s:"{x \ space M. u x = \} \ sets M" using u by (auto simp: borel_measurable_simple_function) ``` hoelzl@38656 ` 891` ``` have "\ = simple_integral (\x. \ * indicator {x\space M. u x = \} x)" ``` hoelzl@38656 ` 892` ``` apply(subst simple_integral_mult) using s ``` hoelzl@38656 ` 893` ``` unfolding simple_integral_indicator_only[OF s] using False by auto ``` hoelzl@38656 ` 894` ``` also have "... \ simple_integral u" ``` hoelzl@38656 ` 895` ``` apply (rule simple_integral_mono) ``` hoelzl@38656 ` 896` ``` apply (rule simple_function_mult) ``` hoelzl@38656 ` 897` ``` apply (rule simple_function_const) ``` hoelzl@38656 ` 898` ``` apply(rule ) prefer 3 apply(subst indicator_def) ``` hoelzl@38656 ` 899` ``` using s u by auto ``` hoelzl@38656 ` 900` ``` finally have *:"simple_integral u = \" by auto ``` hoelzl@38656 ` 901` ``` show ?thesis unfolding * Lim_omega_pos ``` hoelzl@38656 ` 902` ``` proof safe case goal1 ``` hoelzl@38656 ` 903` ``` from real_arch_simple[of "B / real (\ ?s)"] guess N0 .. note N=this ``` hoelzl@38656 ` 904` ``` def N \ "Suc N0" have N:"real N \ B / real (\ ?s)" "N > 0" ``` hoelzl@38656 ` 905` ``` unfolding N_def using N by auto ``` hoelzl@38656 ` 906` ``` show ?case apply-apply(rule_tac x=N in exI,safe) ``` hoelzl@38656 ` 907` ``` proof- case goal1 ``` hoelzl@38656 ` 908` ``` have "Real B \ Real (real N) * \ ?s" ``` hoelzl@38656 ` 909` ``` proof(cases "\ ?s = \") ``` hoelzl@38656 ` 910` ``` case True thus ?thesis using `B>0` N by auto ``` hoelzl@38656 ` 911` ``` next case False ``` hoelzl@38656 ` 912` ``` have *:"B \ real N * real (\ ?s)" ``` hoelzl@38656 ` 913` ``` using N(1) apply-apply(subst (asm) pos_divide_le_eq) ``` hoelzl@38656 ` 914` ``` apply rule using m0 False by auto ``` hoelzl@38656 ` 915` ``` show ?thesis apply(subst Real_real'[THEN sym,OF False]) ``` hoelzl@38656 ` 916` ``` apply(subst pinfreal_times,subst if_P) defer ``` hoelzl@38656 ` 917` ``` apply(subst pinfreal_less_eq,subst if_P) defer ``` hoelzl@38656 ` 918` ``` using * N `B>0` by(auto intro: mult_nonneg_nonneg) ``` hoelzl@38656 ` 919` ``` qed ``` hoelzl@38656 ` 920` ``` also have "... \ Real (real n) * \ ?s" ``` hoelzl@38656 ` 921` ``` apply(rule mult_right_mono) using goal1 by auto ``` hoelzl@38656 ` 922` ``` also have "... = simple_integral (\x. Real (real n) * indicator ?s x)" ``` hoelzl@38656 ` 923` ``` apply(subst simple_integral_mult) apply(rule simple_function_indicator[OF s]) ``` hoelzl@38656 ` 924` ``` unfolding simple_integral_indicator_only[OF s] .. ``` hoelzl@38656 ` 925` ``` also have "... \ simple_integral (\x. if u x = \ then Real (real n) else u x)" ``` hoelzl@38656 ` 926` ``` apply(rule simple_integral_mono) apply(rule simple_function_mult) ``` hoelzl@38656 ` 927` ``` apply(rule simple_function_const) ``` hoelzl@38656 ` 928` ``` apply(rule simple_function_indicator) apply(rule s su)+ by auto ``` hoelzl@38656 ` 929` ``` finally show ?case . ``` hoelzl@38656 ` 930` ``` qed qed qed ``` hoelzl@38656 ` 931` ``` fix x assume x:"\ = (if u x = \ then Real (real n) else u x)" "x \ space M" ``` hoelzl@38656 ` 932` ``` hence "u x = \" apply-apply(rule ccontr) by auto ``` hoelzl@38656 ` 933` ``` hence "\ = Real (real n)" using x by auto ``` hoelzl@38656 ` 934` ``` thus False by auto ``` hoelzl@35582 ` 935` ``` qed ``` hoelzl@35582 ` 936` ```qed ``` hoelzl@35582 ` 937` hoelzl@38656 ` 938` ```lemma (in measure_space) positive_integral_cong: ``` hoelzl@38656 ` 939` ``` assumes "\x. x \ space M \ f x = g x" ``` hoelzl@38656 ` 940` ``` shows "positive_integral f = positive_integral g" ``` hoelzl@38656 ` 941` ```proof - ``` hoelzl@38656 ` 942` ``` have "\h. (\x\space M. h x \ f x \ h x \ \) = (\x\space M. h x \ g x \ h x \ \)" ``` hoelzl@38656 ` 943` ``` using assms by auto ``` hoelzl@38656 ` 944` ``` thus ?thesis unfolding positive_integral_alt1 by auto ``` hoelzl@38656 ` 945` ```qed ``` hoelzl@38656 ` 946` hoelzl@38656 ` 947` ```lemma (in measure_space) positive_integral_eq_simple_integral: ``` hoelzl@38656 ` 948` ``` assumes "simple_function f" ``` hoelzl@38656 ` 949` ``` shows "positive_integral f = simple_integral f" ``` hoelzl@38656 ` 950` ``` unfolding positive_integral_alt ``` hoelzl@38656 ` 951` ```proof (safe intro!: pinfreal_SUPI) ``` hoelzl@38656 ` 952` ``` fix g assume "simple_function g" "g \ f" ``` hoelzl@38656 ` 953` ``` with assms show "simple_integral g \ simple_integral f" ``` hoelzl@38656 ` 954` ``` by (auto intro!: simple_integral_mono simp: le_fun_def) ``` hoelzl@38656 ` 955` ```next ``` hoelzl@38656 ` 956` ``` fix y assume "\x. x\{g. simple_function g \ g \ f} \ simple_integral x \ y" ``` hoelzl@38656 ` 957` ``` with assms show "simple_integral f \ y" by auto ``` hoelzl@38656 ` 958` ```qed ``` hoelzl@35582 ` 959` hoelzl@40859 ` 960` ```lemma (in measure_space) positive_integral_mono_AE: ``` hoelzl@40859 ` 961` ``` assumes ae: "AE x. u x \ v x" ``` hoelzl@38656 ` 962` ``` shows "positive_integral u \ positive_integral v" ``` hoelzl@38656 ` 963` ``` unfolding positive_integral_alt1 ``` hoelzl@38656 ` 964` ```proof (safe intro!: SUPR_mono) ``` hoelzl@40859 ` 965` ``` fix a assume a: "simple_function a" and mono: "\x\space M. a x \ u x \ a x \ \" ``` hoelzl@40859 ` 966` ``` from ae obtain N where N: "{x\space M. \ u x \ v x} \ N" "N \ sets M" "\ N = 0" ``` hoelzl@40859 ` 967` ``` by (auto elim!: AE_E) ``` hoelzl@40859 ` 968` ``` have "simple_function (\x. a x * indicator (space M - N) x)" ``` hoelzl@40859 ` 969` ``` using `N \ sets M` a by auto ``` hoelzl@40859 ` 970` ``` with a show "\b\{g. simple_function g \ (\x\space M. g x \ v x \ g x \ \)}. ``` hoelzl@40859 ` 971` ``` simple_integral a \ simple_integral b" ``` hoelzl@40859 ` 972` ``` proof (safe intro!: bexI[of _ "\x. a x * indicator (space M - N) x"] ``` hoelzl@40859 ` 973` ``` simple_integral_mono_AE) ``` hoelzl@40859 ` 974` ``` show "AE x. a x \ a x * indicator (space M - N) x" ``` hoelzl@40859 ` 975` ``` proof (rule AE_I, rule subset_refl) ``` hoelzl@40859 ` 976` ``` have *: "{x \ space M. \ a x \ a x * indicator (space M - N) x} = ``` hoelzl@40859 ` 977` ``` N \ {x \ space M. a x \ 0}" (is "?N = _") ``` hoelzl@40859 ` 978` ``` using `N \ sets M`[THEN sets_into_space] by (auto simp: indicator_def) ``` hoelzl@40859 ` 979` ``` then show "?N \ sets M" ``` hoelzl@40859 ` 980` ``` using `N \ sets M` `simple_function a`[THEN borel_measurable_simple_function] ``` hoelzl@40859 ` 981` ``` by (auto intro!: measure_mono Int) ``` hoelzl@40859 ` 982` ``` then have "\ ?N \ \ N" ``` hoelzl@40859 ` 983` ``` unfolding * using `N \ sets M` by (auto intro!: measure_mono) ``` hoelzl@40859 ` 984` ``` then show "\ ?N = 0" using `\ N = 0` by auto ``` hoelzl@40859 ` 985` ``` qed ``` hoelzl@40859 ` 986` ``` next ``` hoelzl@40859 ` 987` ``` fix x assume "x \ space M" ``` hoelzl@40859 ` 988` ``` show "a x * indicator (space M - N) x \ v x" ``` hoelzl@40859 ` 989` ``` proof (cases "x \ N") ``` hoelzl@40859 ` 990` ``` case True then show ?thesis by simp ``` hoelzl@40859 ` 991` ``` next ``` hoelzl@40859 ` 992` ``` case False ``` hoelzl@40859 ` 993` ``` with N mono have "a x \ u x" "u x \ v x" using `x \ space M` by auto ``` hoelzl@40859 ` 994` ``` with False `x \ space M` show "a x * indicator (space M - N) x \ v x" by auto ``` hoelzl@40859 ` 995` ``` qed ``` hoelzl@40859 ` 996` ``` assume "a x * indicator (space M - N) x = \" ``` hoelzl@40859 ` 997` ``` with mono `x \ space M` show False ``` hoelzl@40859 ` 998` ``` by (simp split: split_if_asm add: indicator_def) ``` hoelzl@40859 ` 999` ``` qed ``` hoelzl@40859 ` 1000` ```qed ``` hoelzl@40859 ` 1001` hoelzl@40859 ` 1002` ```lemma (in measure_space) positive_integral_cong_AE: ``` hoelzl@40859 ` 1003` ``` "AE x. u x = v x \ positive_integral u = positive_integral v" ``` hoelzl@40859 ` 1004` ``` by (auto simp: eq_iff intro!: positive_integral_mono_AE) ``` hoelzl@40859 ` 1005` hoelzl@40859 ` 1006` ```lemma (in measure_space) positive_integral_mono: ``` hoelzl@40859 ` 1007` ``` assumes mono: "\x. x \ space M \ u x \ v x" ``` hoelzl@40859 ` 1008` ``` shows "positive_integral u \ positive_integral v" ``` hoelzl@40859 ` 1009` ``` using mono by (auto intro!: AE_cong positive_integral_mono_AE) ``` hoelzl@40859 ` 1010` hoelzl@40859 ` 1011` ```lemma (in measure_space) positive_integral_vimage: ``` hoelzl@40859 ` 1012` ``` fixes g :: "'a \ pinfreal" and f :: "'d \ 'a" ``` hoelzl@40859 ` 1013` ``` assumes f: "bij_betw f S (space M)" ``` hoelzl@40859 ` 1014` ``` shows "positive_integral g = ``` hoelzl@40859 ` 1015` ``` measure_space.positive_integral (vimage_algebra S f) (\A. \ (f ` A)) (\x. g (f x))" ``` hoelzl@40859 ` 1016` ``` (is "_ = measure_space.positive_integral ?T ?\ _") ``` hoelzl@40859 ` 1017` ```proof - ``` hoelzl@40859 ` 1018` ``` from f interpret T: measure_space ?T ?\ by (rule measure_space_isomorphic) ``` hoelzl@40859 ` 1019` ``` have f_fun: "f \ S \ space M" using assms unfolding bij_betw_def by auto ``` hoelzl@40859 ` 1020` ``` from assms have inv: "bij_betw (the_inv_into S f) (space M) S" ``` hoelzl@40859 ` 1021` ``` by (rule bij_betw_the_inv_into) ``` hoelzl@40859 ` 1022` ``` then have inv_fun: "the_inv_into S f \ space M \ S" unfolding bij_betw_def by auto ``` hoelzl@40859 ` 1023` hoelzl@40859 ` 1024` ``` have surj: "f`S = space M" ``` hoelzl@40859 ` 1025` ``` using f unfolding bij_betw_def by simp ``` hoelzl@40859 ` 1026` ``` have inj: "inj_on f S" ``` hoelzl@40859 ` 1027` ``` using f unfolding bij_betw_def by simp ``` hoelzl@40859 ` 1028` ``` have inv_f: "\x. x \ space M \ f (the_inv_into S f x) = x" ``` hoelzl@40859 ` 1029` ``` using f_the_inv_into_f[of f S] f unfolding bij_betw_def by auto ``` hoelzl@40859 ` 1030` hoelzl@40859 ` 1031` ``` from simple_integral_vimage[OF assms, symmetric] ``` hoelzl@40859 ` 1032` ``` have *: "simple_integral = T.simple_integral \ (\g. g \ f)" by (simp add: comp_def) ``` hoelzl@40859 ` 1033` ``` show ?thesis ``` hoelzl@40859 ` 1034` ``` unfolding positive_integral_alt1 T.positive_integral_alt1 SUPR_def * image_compose ``` hoelzl@40859 ` 1035` ``` proof (safe intro!: arg_cong[where f=Sup] image_set_cong, simp_all add: comp_def) ``` hoelzl@40859 ` 1036` ``` fix g' :: "'a \ pinfreal" assume "simple_function g'" "\x\space M. g' x \ g x \ g' x \ \" ``` hoelzl@40859 ` 1037` ``` then show "\h. T.simple_function h \ (\x\S. h x \ g (f x) \ h x \ \) \ ``` hoelzl@40859 ` 1038` ``` T.simple_integral (\x. g' (f x)) = T.simple_integral h" ``` hoelzl@40859 ` 1039` ``` using f unfolding bij_betw_def ``` hoelzl@40859 ` 1040` ``` by (auto intro!: exI[of _ "\x. g' (f x)"] ``` hoelzl@40859 ` 1041` ``` simp add: le_fun_def simple_function_vimage[OF _ f_fun]) ``` hoelzl@40859 ` 1042` ``` next ``` hoelzl@40859 ` 1043` ``` fix g' :: "'d \ pinfreal" assume g': "T.simple_function g'" "\x\S. g' x \ g (f x) \ g' x \ \" ``` hoelzl@40859 ` 1044` ``` let ?g = "\x. g' (the_inv_into S f x)" ``` hoelzl@40859 ` 1045` ``` show "\h. simple_function h \ (\x\space M. h x \ g x \ h x \ \) \ ``` hoelzl@40859 ` 1046` ``` T.simple_integral g' = T.simple_integral (\x. h (f x))" ``` hoelzl@40859 ` 1047` ``` proof (intro exI[of _ ?g] conjI ballI) ``` hoelzl@40859 ` 1048` ``` { fix x assume x: "x \ space M" ``` hoelzl@40859 ` 1049` ``` then have "the_inv_into S f x \ S" using inv_fun by auto ``` hoelzl@40859 ` 1050` ``` with g' have "g' (the_inv_into S f x) \ g (f (the_inv_into S f x)) \ g' (the_inv_into S f x) \ \" ``` hoelzl@40859 ` 1051` ``` by auto ``` hoelzl@40859 ` 1052` ``` then show "g' (the_inv_into S f x) \ g x" "g' (the_inv_into S f x) \ \" ``` hoelzl@40859 ` 1053` ``` using f_the_inv_into_f[of f S x] x f unfolding bij_betw_def by auto } ``` hoelzl@40859 ` 1054` ``` note vimage_vimage_inv[OF f inv_f inv_fun, simp] ``` hoelzl@40859 ` 1055` ``` from T.simple_function_vimage[OF g'(1), unfolded space_vimage_algebra, OF inv_fun] ``` hoelzl@40859 ` 1056` ``` show "simple_function (\x. g' (the_inv_into S f x))" ``` hoelzl@40859 ` 1057` ``` unfolding simple_function_def by (simp add: simple_function_def) ``` hoelzl@40859 ` 1058` ``` show "T.simple_integral g' = T.simple_integral (\x. ?g (f x))" ``` hoelzl@40859 ` 1059` ``` using the_inv_into_f_f[OF inj] by (auto intro!: T.simple_integral_cong) ``` hoelzl@40859 ` 1060` ``` qed ``` hoelzl@40859 ` 1061` ``` qed ``` hoelzl@40859 ` 1062` ```qed ``` hoelzl@40859 ` 1063` hoelzl@40859 ` 1064` ```lemma (in measure_space) positive_integral_vimage_inv: ``` hoelzl@40859 ` 1065` ``` fixes g :: "'d \ pinfreal" and f :: "'d \ 'a" ``` hoelzl@40859 ` 1066` ``` assumes f: "bij_betw f S (space M)" ``` hoelzl@40859 ` 1067` ``` shows "measure_space.positive_integral (vimage_algebra S f) (\A. \ (f ` A)) g = ``` hoelzl@40859 ` 1068` ``` positive_integral (\x. g (the_inv_into S f x))" ``` hoelzl@40859 ` 1069` ```proof - ``` hoelzl@40859 ` 1070` ``` interpret v: measure_space "vimage_algebra S f" "\A. \ (f ` A)" ``` hoelzl@40859 ` 1071` ``` using f by (rule measure_space_isomorphic) ``` hoelzl@40859 ` 1072` ``` show ?thesis ``` hoelzl@40859 ` 1073` ``` unfolding positive_integral_vimage[OF f, of "\x. g (the_inv_into S f x)"] ``` hoelzl@40859 ` 1074` ``` using f[unfolded bij_betw_def] ``` hoelzl@40859 ` 1075` ``` by (auto intro!: v.positive_integral_cong simp: the_inv_into_f_f) ``` hoelzl@38656 ` 1076` ```qed ``` hoelzl@38656 ` 1077` hoelzl@38656 ` 1078` ```lemma (in measure_space) positive_integral_SUP_approx: ``` hoelzl@38656 ` 1079` ``` assumes "f \ s" ``` hoelzl@38656 ` 1080` ``` and f: "\i. f i \ borel_measurable M" ``` hoelzl@38656 ` 1081` ``` and "simple_function u" ``` hoelzl@38656 ` 1082` ``` and le: "u \ s" and real: "\ \ u`space M" ``` hoelzl@38656 ` 1083` ``` shows "simple_integral u \ (SUP i. positive_integral (f i))" (is "_ \ ?S") ``` hoelzl@38656 ` 1084` ```proof (rule pinfreal_le_mult_one_interval) ``` hoelzl@38656 ` 1085` ``` fix a :: pinfreal assume "0 < a" "a < 1" ``` hoelzl@38656 ` 1086` ``` hence "a \ 0" by auto ``` hoelzl@38656 ` 1087` ``` let "?B i" = "{x \ space M. a * u x \ f i x}" ``` hoelzl@38656 ` 1088` ``` have B: "\i. ?B i \ sets M" ``` hoelzl@38656 ` 1089` ``` using f `simple_function u` by (auto simp: borel_measurable_simple_function) ``` hoelzl@38656 ` 1090` hoelzl@38656 ` 1091` ``` let "?uB i x" = "u x * indicator (?B i) x" ``` hoelzl@38656 ` 1092` hoelzl@38656 ` 1093` ``` { fix i have "?B i \ ?B (Suc i)" ``` hoelzl@38656 ` 1094` ``` proof safe ``` hoelzl@38656 ` 1095` ``` fix i x assume "a * u x \ f i x" ``` hoelzl@38656 ` 1096` ``` also have "\ \ f (Suc i) x" ``` hoelzl@38656 ` 1097` ``` using `f \ s` unfolding isoton_def le_fun_def by auto ``` hoelzl@38656 ` 1098` ``` finally show "a * u x \ f (Suc i) x" . ``` hoelzl@38656 ` 1099` ``` qed } ``` hoelzl@38656 ` 1100` ``` note B_mono = this ``` hoelzl@35582 ` 1101` hoelzl@38656 ` 1102` ``` have u: "\x. x \ space M \ u -` {u x} \ space M \ sets M" ``` hoelzl@38656 ` 1103` ``` using `simple_function u` by (auto simp add: simple_function_def) ``` hoelzl@38656 ` 1104` hoelzl@40859 ` 1105` ``` have "\i. (\n. (u -` {i} \ space M) \ ?B n) \ (u -` {i} \ space M)" using B_mono unfolding isoton_def ``` hoelzl@40859 ` 1106` ``` proof safe ``` hoelzl@40859 ` 1107` ``` fix x i assume "x \ space M" ``` hoelzl@40859 ` 1108` ``` show "x \ (\i. (u -` {u x} \ space M) \ ?B i)" ``` hoelzl@40859 ` 1109` ``` proof cases ``` hoelzl@40859 ` 1110` ``` assume "u x = 0" thus ?thesis using `x \ space M` by simp ``` hoelzl@40859 ` 1111` ``` next ``` hoelzl@40859 ` 1112` ``` assume "u x \ 0" ``` hoelzl@40859 ` 1113` ``` with `a < 1` real `x \ space M` ``` hoelzl@40859 ` 1114` ``` have "a * u x < 1 * u x" by (rule_tac pinfreal_mult_strict_right_mono) (auto simp: image_iff) ``` hoelzl@40859 ` 1115` ``` also have "\ \ (SUP i. f i x)" using le `f \ s` ``` hoelzl@40859 ` 1116` ``` unfolding isoton_fun_expand by (auto simp: isoton_def le_fun_def) ``` hoelzl@40859 ` 1117` ``` finally obtain i where "a * u x < f i x" unfolding SUPR_def ``` hoelzl@40859 ` 1118` ``` by (auto simp add: less_Sup_iff) ``` hoelzl@40859 ` 1119` ``` hence "a * u x \ f i x" by auto ``` hoelzl@40859 ` 1120` ``` thus ?thesis using `x \ space M` by auto ``` hoelzl@40859 ` 1121` ``` qed ``` hoelzl@40859 ` 1122` ``` qed auto ``` hoelzl@40859 ` 1123` ``` note measure_conv = measure_up[OF Int[OF u B] this] ``` hoelzl@38656 ` 1124` hoelzl@38656 ` 1125` ``` have "simple_integral u = (SUP i. simple_integral (?uB i))" ``` hoelzl@38656 ` 1126` ``` unfolding simple_integral_indicator[OF B `simple_function u`] ``` hoelzl@38656 ` 1127` ``` proof (subst SUPR_pinfreal_setsum, safe) ``` hoelzl@38656 ` 1128` ``` fix x n assume "x \ space M" ``` hoelzl@38656 ` 1129` ``` have "\ (u -` {u x} \ space M \ {x \ space M. a * u x \ f n x}) ``` hoelzl@38656 ` 1130` ``` \ \ (u -` {u x} \ space M \ {x \ space M. a * u x \ f (Suc n) x})" ``` hoelzl@38656 ` 1131` ``` using B_mono Int[OF u[OF `x \ space M`] B] by (auto intro!: measure_mono) ``` hoelzl@38656 ` 1132` ``` thus "u x * \ (u -` {u x} \ space M \ ?B n) ``` hoelzl@38656 ` 1133` ``` \ u x * \ (u -` {u x} \ space M \ ?B (Suc n))" ``` hoelzl@38656 ` 1134` ``` by (auto intro: mult_left_mono) ``` hoelzl@38656 ` 1135` ``` next ``` hoelzl@38656 ` 1136` ``` show "simple_integral u = ``` hoelzl@38656 ` 1137` ``` (\i\u ` space M. SUP n. i * \ (u -` {i} \ space M \ ?B n))" ``` hoelzl@38656 ` 1138` ``` using measure_conv unfolding simple_integral_def isoton_def ``` hoelzl@38656 ` 1139` ``` by (auto intro!: setsum_cong simp: pinfreal_SUP_cmult) ``` hoelzl@38656 ` 1140` ``` qed ``` hoelzl@38656 ` 1141` ``` moreover ``` hoelzl@38656 ` 1142` ``` have "a * (SUP i. simple_integral (?uB i)) \ ?S" ``` hoelzl@38656 ` 1143` ``` unfolding pinfreal_SUP_cmult[symmetric] ``` hoelzl@38705 ` 1144` ``` proof (safe intro!: SUP_mono bexI) ``` hoelzl@38656 ` 1145` ``` fix i ``` hoelzl@38656 ` 1146` ``` have "a * simple_integral (?uB i) = simple_integral (\x. a * ?uB i x)" ``` hoelzl@38656 ` 1147` ``` using B `simple_function u` ``` hoelzl@38656 ` 1148` ``` by (subst simple_integral_mult[symmetric]) (auto simp: field_simps) ``` hoelzl@38656 ` 1149` ``` also have "\ \ positive_integral (f i)" ``` hoelzl@38656 ` 1150` ``` proof - ``` hoelzl@38656 ` 1151` ``` have "\x. a * ?uB i x \ f i x" unfolding indicator_def by auto ``` hoelzl@38656 ` 1152` ``` hence *: "simple_function (\x. a * ?uB i x)" using B assms(3) ``` hoelzl@38656 ` 1153` ``` by (auto intro!: simple_integral_mono) ``` hoelzl@38656 ` 1154` ``` show ?thesis unfolding positive_integral_eq_simple_integral[OF *, symmetric] ``` hoelzl@38656 ` 1155` ``` by (auto intro!: positive_integral_mono simp: indicator_def) ``` hoelzl@38656 ` 1156` ``` qed ``` hoelzl@38656 ` 1157` ``` finally show "a * simple_integral (?uB i) \ positive_integral (f i)" ``` hoelzl@38656 ` 1158` ``` by auto ``` hoelzl@38705 ` 1159` ``` qed simp ``` hoelzl@38656 ` 1160` ``` ultimately show "a * simple_integral u \ ?S" by simp ``` hoelzl@35582 ` 1161` ```qed ``` hoelzl@35582 ` 1162` hoelzl@35582 ` 1163` ```text {* Beppo-Levi monotone convergence theorem *} ``` hoelzl@38656 ` 1164` ```lemma (in measure_space) positive_integral_isoton: ``` hoelzl@38656 ` 1165` ``` assumes "f \ u" "\i. f i \ borel_measurable M" ``` hoelzl@38656 ` 1166` ``` shows "(\i. positive_integral (f i)) \ positive_integral u" ``` hoelzl@38656 ` 1167` ``` unfolding isoton_def ``` hoelzl@38656 ` 1168` ```proof safe ``` hoelzl@38656 ` 1169` ``` fix i show "positive_integral (f i) \ positive_integral (f (Suc i))" ``` hoelzl@38656 ` 1170` ``` apply (rule positive_integral_mono) ``` hoelzl@38656 ` 1171` ``` using `f \ u` unfolding isoton_def le_fun_def by auto ``` hoelzl@38656 ` 1172` ```next ``` hoelzl@38656 ` 1173` ``` have "u \ borel_measurable M" ``` hoelzl@38656 ` 1174` ``` using borel_measurable_SUP[of UNIV f] assms by (auto simp: isoton_def) ``` hoelzl@38656 ` 1175` ``` have u: "u = (SUP i. f i)" using `f \ u` unfolding isoton_def by auto ``` hoelzl@35582 ` 1176` hoelzl@38656 ` 1177` ``` show "(SUP i. positive_integral (f i)) = positive_integral u" ``` hoelzl@38656 ` 1178` ``` proof (rule antisym) ``` hoelzl@38656 ` 1179` ``` from `f \ u`[THEN isoton_Sup, unfolded le_fun_def] ``` hoelzl@38656 ` 1180` ``` show "(SUP j. positive_integral (f j)) \ positive_integral u" ``` hoelzl@38656 ` 1181` ``` by (auto intro!: SUP_leI positive_integral_mono) ``` hoelzl@38656 ` 1182` ``` next ``` hoelzl@38656 ` 1183` ``` show "positive_integral u \ (SUP i. positive_integral (f i))" ``` hoelzl@38656 ` 1184` ``` unfolding positive_integral_def[of u] ``` hoelzl@38656 ` 1185` ``` by (auto intro!: SUP_leI positive_integral_SUP_approx[OF assms]) ``` hoelzl@35582 ` 1186` ``` qed ``` hoelzl@35582 ` 1187` ```qed ``` hoelzl@35582 ` 1188` hoelzl@40859 ` 1189` ```lemma (in measure_space) positive_integral_monotone_convergence_SUP: ``` hoelzl@40859 ` 1190` ``` assumes "\i x. x \ space M \ f i x \ f (Suc i) x" ``` hoelzl@40859 ` 1191` ``` assumes "\i. f i \ borel_measurable M" ``` hoelzl@40859 ` 1192` ``` shows "(SUP i. positive_integral (f i)) = positive_integral (\x. SUP i. f i x)" ``` hoelzl@40859 ` 1193` ``` (is "_ = positive_integral ?u") ``` hoelzl@40859 ` 1194` ```proof - ``` hoelzl@40859 ` 1195` ``` have "?u \ borel_measurable M" ``` hoelzl@40859 ` 1196` ``` using borel_measurable_SUP[of _ f] assms by (simp add: SUPR_fun_expand) ``` hoelzl@40859 ` 1197` hoelzl@40859 ` 1198` ``` show ?thesis ``` hoelzl@40859 ` 1199` ``` proof (rule antisym) ``` hoelzl@40859 ` 1200` ``` show "(SUP j. positive_integral (f j)) \ positive_integral ?u" ``` hoelzl@40859 ` 1201` ``` by (auto intro!: SUP_leI positive_integral_mono le_SUPI) ``` hoelzl@40859 ` 1202` ``` next ``` hoelzl@40859 ` 1203` ``` def rf \ "\i. \x\space M. f i x" and ru \ "\x\space M. ?u x" ``` hoelzl@40859 ` 1204` ``` have "\i. rf i \ borel_measurable M" unfolding rf_def ``` hoelzl@40859 ` 1205` ``` using assms by (simp cong: measurable_cong) ``` hoelzl@40859 ` 1206` ``` moreover have iso: "rf \ ru" using assms unfolding rf_def ru_def ``` hoelzl@40859 ` 1207` ``` unfolding isoton_def SUPR_fun_expand le_fun_def fun_eq_iff ``` hoelzl@40859 ` 1208` ``` by (auto simp: restrict_def le_fun_def SUPR_fun_expand fun_eq_iff) ``` hoelzl@40859 ` 1209` ``` ultimately have "positive_integral ru \ (SUP i. positive_integral (rf i))" ``` hoelzl@40859 ` 1210` ``` unfolding positive_integral_def[of ru] ``` hoelzl@40859 ` 1211` ``` by (auto simp: le_fun_def intro!: SUP_leI positive_integral_SUP_approx) ``` hoelzl@40859 ` 1212` ``` then show "positive_integral ?u \ (SUP i. positive_integral (f i))" ``` hoelzl@40859 ` 1213` ``` unfolding ru_def rf_def by (simp cong: positive_integral_cong) ``` hoelzl@40859 ` 1214` ``` qed ``` hoelzl@40859 ` 1215` ```qed ``` hoelzl@40859 ` 1216` hoelzl@38656 ` 1217` ```lemma (in measure_space) SUP_simple_integral_sequences: ``` hoelzl@38656 ` 1218` ``` assumes f: "f \ u" "\i. simple_function (f i)" ``` hoelzl@38656 ` 1219` ``` and g: "g \ u" "\i. simple_function (g i)" ``` hoelzl@38656 ` 1220` ``` shows "(SUP i. simple_integral (f i)) = (SUP i. simple_integral (g i))" ``` hoelzl@38656 ` 1221` ``` (is "SUPR _ ?F = SUPR _ ?G") ``` hoelzl@38656 ` 1222` ```proof - ``` hoelzl@38656 ` 1223` ``` have "(SUP i. ?F i) = (SUP i. positive_integral (f i))" ``` hoelzl@38656 ` 1224` ``` using assms by (simp add: positive_integral_eq_simple_integral) ``` hoelzl@38656 ` 1225` ``` also have "\ = positive_integral u" ``` hoelzl@38656 ` 1226` ``` using positive_integral_isoton[OF f(1) borel_measurable_simple_function[OF f(2)]] ``` hoelzl@38656 ` 1227` ``` unfolding isoton_def by simp ``` hoelzl@38656 ` 1228` ``` also have "\ = (SUP i. positive_integral (g i))" ``` hoelzl@38656 ` 1229` ``` using positive_integral_isoton[OF g(1) borel_measurable_simple_function[OF g(2)]] ``` hoelzl@38656 ` 1230` ``` unfolding isoton_def by simp ``` hoelzl@38656 ` 1231` ``` also have "\ = (SUP i. ?G i)" ``` hoelzl@38656 ` 1232` ``` using assms by (simp add: positive_integral_eq_simple_integral) ``` hoelzl@38656 ` 1233` ``` finally show ?thesis . ``` hoelzl@38656 ` 1234` ```qed ``` hoelzl@38656 ` 1235` hoelzl@38656 ` 1236` ```lemma (in measure_space) positive_integral_const[simp]: ``` hoelzl@38656 ` 1237` ``` "positive_integral (\x. c) = c * \ (space M)" ``` hoelzl@38656 ` 1238` ``` by (subst positive_integral_eq_simple_integral) auto ``` hoelzl@38656 ` 1239` hoelzl@38656 ` 1240` ```lemma (in measure_space) positive_integral_isoton_simple: ``` hoelzl@38656 ` 1241` ``` assumes "f \ u" and e: "\i. simple_function (f i)" ``` hoelzl@38656 ` 1242` ``` shows "(\i. simple_integral (f i)) \ positive_integral u" ``` hoelzl@38656 ` 1243` ``` using positive_integral_isoton[OF `f \ u` e(1)[THEN borel_measurable_simple_function]] ``` hoelzl@38656 ` 1244` ``` unfolding positive_integral_eq_simple_integral[OF e] . ``` hoelzl@38656 ` 1245` hoelzl@38656 ` 1246` ```lemma (in measure_space) positive_integral_linear: ``` hoelzl@38656 ` 1247` ``` assumes f: "f \ borel_measurable M" ``` hoelzl@38656 ` 1248` ``` and g: "g \ borel_measurable M" ``` hoelzl@38656 ` 1249` ``` shows "positive_integral (\x. a * f x + g x) = ``` hoelzl@38656 ` 1250` ``` a * positive_integral f + positive_integral g" ``` hoelzl@38656 ` 1251` ``` (is "positive_integral ?L = _") ``` hoelzl@35582 ` 1252` ```proof - ``` hoelzl@38656 ` 1253` ``` from borel_measurable_implies_simple_function_sequence'[OF f] guess u . ``` hoelzl@38656 ` 1254` ``` note u = this positive_integral_isoton_simple[OF this(1-2)] ``` hoelzl@38656 ` 1255` ``` from borel_measurable_implies_simple_function_sequence'[OF g] guess v . ``` hoelzl@38656 ` 1256` ``` note v = this positive_integral_isoton_simple[OF this(1-2)] ``` hoelzl@38656 ` 1257` ``` let "?L' i x" = "a * u i x + v i x" ``` hoelzl@38656 ` 1258` hoelzl@38656 ` 1259` ``` have "?L \ borel_measurable M" ``` hoelzl@38656 ` 1260` ``` using assms by simp ``` hoelzl@38656 ` 1261` ``` from borel_measurable_implies_simple_function_sequence'[OF this] guess l . ``` hoelzl@38656 ` 1262` ``` note positive_integral_isoton_simple[OF this(1-2)] and l = this ``` hoelzl@38656 ` 1263` ``` moreover have ``` hoelzl@38656 ` 1264` ``` "(SUP i. simple_integral (l i)) = (SUP i. simple_integral (?L' i))" ``` hoelzl@38656 ` 1265` ``` proof (rule SUP_simple_integral_sequences[OF l(1-2)]) ``` hoelzl@38656 ` 1266` ``` show "?L' \ ?L" "\i. simple_function (?L' i)" ``` hoelzl@38656 ` 1267` ``` using u v by (auto simp: isoton_fun_expand isoton_add isoton_cmult_right) ``` hoelzl@38656 ` 1268` ``` qed ``` hoelzl@38656 ` 1269` ``` moreover from u v have L'_isoton: ``` hoelzl@38656 ` 1270` ``` "(\i. simple_integral (?L' i)) \ a * positive_integral f + positive_integral g" ``` hoelzl@38656 ` 1271` ``` by (simp add: isoton_add isoton_cmult_right) ``` hoelzl@38656 ` 1272` ``` ultimately show ?thesis by (simp add: isoton_def) ``` hoelzl@38656 ` 1273` ```qed ``` hoelzl@38656 ` 1274` hoelzl@38656 ` 1275` ```lemma (in measure_space) positive_integral_cmult: ``` hoelzl@38656 ` 1276` ``` assumes "f \ borel_measurable M" ``` hoelzl@38656 ` 1277` ``` shows "positive_integral (\x. c * f x) = c * positive_integral f" ``` hoelzl@38656 ` 1278` ``` using positive_integral_linear[OF assms, of "\x. 0" c] by auto ``` hoelzl@38656 ` 1279` hoelzl@38656 ` 1280` ```lemma (in measure_space) positive_integral_indicator[simp]: ``` hoelzl@38656 ` 1281` ``` "A \ sets M \ positive_integral (\x. indicator A x) = \ A" ``` hoelzl@38656 ` 1282` ```by (subst positive_integral_eq_simple_integral) (auto simp: simple_function_indicator simple_integral_indicator) ``` hoelzl@38656 ` 1283` hoelzl@38656 ` 1284` ```lemma (in measure_space) positive_integral_cmult_indicator: ``` hoelzl@38656 ` 1285` ``` "A \ sets M \ positive_integral (\x. c * indicator A x) = c * \ A" ``` hoelzl@38656 ` 1286` ```by (subst positive_integral_eq_simple_integral) (auto simp: simple_function_indicator simple_integral_indicator) ``` hoelzl@38656 ` 1287` hoelzl@38656 ` 1288` ```lemma (in measure_space) positive_integral_add: ``` hoelzl@38656 ` 1289` ``` assumes "f \ borel_measurable M" "g \ borel_measurable M" ``` hoelzl@38656 ` 1290` ``` shows "positive_integral (\x. f x + g x) = positive_integral f + positive_integral g" ``` hoelzl@38656 ` 1291` ``` using positive_integral_linear[OF assms, of 1] by simp ``` hoelzl@38656 ` 1292` hoelzl@38656 ` 1293` ```lemma (in measure_space) positive_integral_setsum: ``` hoelzl@38656 ` 1294` ``` assumes "\i. i\P \ f i \ borel_measurable M" ``` hoelzl@38656 ` 1295` ``` shows "positive_integral (\x. \i\P. f i x) = (\i\P. positive_integral (f i))" ``` hoelzl@38656 ` 1296` ```proof cases ``` hoelzl@38656 ` 1297` ``` assume "finite P" ``` hoelzl@38656 ` 1298` ``` from this assms show ?thesis ``` hoelzl@38656 ` 1299` ``` proof induct ``` hoelzl@38656 ` 1300` ``` case (insert i P) ``` hoelzl@38656 ` 1301` ``` have "f i \ borel_measurable M" ``` hoelzl@38656 ` 1302` ``` "(\x. \i\P. f i x) \ borel_measurable M" ``` hoelzl@38656 ` 1303` ``` using insert by (auto intro!: borel_measurable_pinfreal_setsum) ``` hoelzl@38656 ` 1304` ``` from positive_integral_add[OF this] ``` hoelzl@38656 ` 1305` ``` show ?case using insert by auto ``` hoelzl@38656 ` 1306` ``` qed simp ``` hoelzl@38656 ` 1307` ```qed simp ``` hoelzl@38656 ` 1308` hoelzl@38656 ` 1309` ```lemma (in measure_space) positive_integral_diff: ``` hoelzl@38656 ` 1310` ``` assumes f: "f \ borel_measurable M" and g: "g \ borel_measurable M" ``` hoelzl@38656 ` 1311` ``` and fin: "positive_integral g \ \" ``` hoelzl@38656 ` 1312` ``` and mono: "\x. x \ space M \ g x \ f x" ``` hoelzl@38656 ` 1313` ``` shows "positive_integral (\x. f x - g x) = positive_integral f - positive_integral g" ``` hoelzl@38656 ` 1314` ```proof - ``` hoelzl@38656 ` 1315` ``` have borel: "(\x. f x - g x) \ borel_measurable M" ``` hoelzl@38656 ` 1316` ``` using f g by (rule borel_measurable_pinfreal_diff) ``` hoelzl@38656 ` 1317` ``` have "positive_integral (\x. f x - g x) + positive_integral g = ``` hoelzl@38656 ` 1318` ``` positive_integral f" ``` hoelzl@38656 ` 1319` ``` unfolding positive_integral_add[OF borel g, symmetric] ``` hoelzl@38656 ` 1320` ``` proof (rule positive_integral_cong) ``` hoelzl@38656 ` 1321` ``` fix x assume "x \ space M" ``` hoelzl@38656 ` 1322` ``` from mono[OF this] show "f x - g x + g x = f x" ``` hoelzl@38656 ` 1323` ``` by (cases "f x", cases "g x", simp, simp, cases "g x", auto) ``` hoelzl@38656 ` 1324` ``` qed ``` hoelzl@38656 ` 1325` ``` with mono show ?thesis ``` hoelzl@38656 ` 1326` ``` by (subst minus_pinfreal_eq2[OF _ fin]) (auto intro!: positive_integral_mono) ``` hoelzl@38656 ` 1327` ```qed ``` hoelzl@38656 ` 1328` hoelzl@38656 ` 1329` ```lemma (in measure_space) positive_integral_psuminf: ``` hoelzl@38656 ` 1330` ``` assumes "\i. f i \ borel_measurable M" ``` hoelzl@38656 ` 1331` ``` shows "positive_integral (\x. \\<^isub>\ i. f i x) = (\\<^isub>\ i. positive_integral (f i))" ``` hoelzl@38656 ` 1332` ```proof - ``` hoelzl@38656 ` 1333` ``` have "(\i. positive_integral (\x. \i positive_integral (\x. \\<^isub>\i. f i x)" ``` hoelzl@38656 ` 1334` ``` by (rule positive_integral_isoton) ``` hoelzl@38656 ` 1335` ``` (auto intro!: borel_measurable_pinfreal_setsum assms positive_integral_mono ``` hoelzl@38656 ` 1336` ``` arg_cong[where f=Sup] ``` nipkow@39302 ` 1337` ``` simp: isoton_def le_fun_def psuminf_def fun_eq_iff SUPR_def Sup_fun_def) ``` hoelzl@38656 ` 1338` ``` thus ?thesis ``` hoelzl@38656 ` 1339` ``` by (auto simp: isoton_def psuminf_def positive_integral_setsum[OF assms]) ``` hoelzl@38656 ` 1340` ```qed ``` hoelzl@38656 ` 1341` hoelzl@38656 ` 1342` ```text {* Fatou's lemma: convergence theorem on limes inferior *} ``` hoelzl@38656 ` 1343` ```lemma (in measure_space) positive_integral_lim_INF: ``` hoelzl@38656 ` 1344` ``` fixes u :: "nat \ 'a \ pinfreal" ``` hoelzl@38656 ` 1345` ``` assumes "\i. u i \ borel_measurable M" ``` hoelzl@38656 ` 1346` ``` shows "positive_integral (SUP n. INF m. u (m + n)) \ ``` hoelzl@38656 ` 1347` ``` (SUP n. INF m. positive_integral (u (m + n)))" ``` hoelzl@38656 ` 1348` ```proof - ``` hoelzl@38656 ` 1349` ``` have "(SUP n. INF m. u (m + n)) \ borel_measurable M" ``` hoelzl@38656 ` 1350` ``` by (auto intro!: borel_measurable_SUP borel_measurable_INF assms) ``` hoelzl@38656 ` 1351` hoelzl@38656 ` 1352` ``` have "(\n. INF m. u (m + n)) \ (SUP n. INF m. u (m + n))" ``` hoelzl@38705 ` 1353` ``` proof (unfold isoton_def, safe intro!: INF_mono bexI) ``` hoelzl@38705 ` 1354` ``` fix i m show "u (Suc m + i) \ u (m + Suc i)" by simp ``` hoelzl@38705 ` 1355` ``` qed simp ``` hoelzl@38656 ` 1356` ``` from positive_integral_isoton[OF this] assms ``` hoelzl@38656 ` 1357` ``` have "positive_integral (SUP n. INF m. u (m + n)) = ``` hoelzl@38656 ` 1358` ``` (SUP n. positive_integral (INF m. u (m + n)))" ``` hoelzl@38656 ` 1359` ``` unfolding isoton_def by (simp add: borel_measurable_INF) ``` hoelzl@38656 ` 1360` ``` also have "\ \ (SUP n. INF m. positive_integral (u (m + n)))" ``` hoelzl@38705 ` 1361` ``` apply (rule SUP_mono) ``` hoelzl@38705 ` 1362` ``` apply (rule_tac x=n in bexI) ``` hoelzl@38705 ` 1363` ``` by (auto intro!: positive_integral_mono INFI_bound INF_leI exI simp: INFI_fun_expand) ``` hoelzl@38656 ` 1364` ``` finally show ?thesis . ``` hoelzl@35582 ` 1365` ```qed ``` hoelzl@35582 ` 1366` hoelzl@38656 ` 1367` ```lemma (in measure_space) measure_space_density: ``` hoelzl@38656 ` 1368` ``` assumes borel: "u \ borel_measurable M" ``` hoelzl@38656 ` 1369` ``` shows "measure_space M (\A. positive_integral (\x. u x * indicator A x))" (is "measure_space M ?v") ``` hoelzl@38656 ` 1370` ```proof ``` hoelzl@38656 ` 1371` ``` show "?v {} = 0" by simp ``` hoelzl@38656 ` 1372` ``` show "countably_additive M ?v" ``` hoelzl@38656 ` 1373` ``` unfolding countably_additive_def ``` hoelzl@38656 ` 1374` ``` proof safe ``` hoelzl@38656 ` 1375` ``` fix A :: "nat \ 'a set" ``` hoelzl@38656 ` 1376` ``` assume "range A \ sets M" ``` hoelzl@38656 ` 1377` ``` hence "\i. (\x. u x * indicator (A i) x) \ borel_measurable M" ``` hoelzl@38656 ` 1378` ``` using borel by (auto intro: borel_measurable_indicator) ``` hoelzl@38656 ` 1379` ``` moreover assume "disjoint_family A" ``` hoelzl@38656 ` 1380` ``` note psuminf_indicator[OF this] ``` hoelzl@38656 ` 1381` ``` ultimately show "(\\<^isub>\n. ?v (A n)) = ?v (\x. A x)" ``` hoelzl@38656 ` 1382` ``` by (simp add: positive_integral_psuminf[symmetric]) ``` hoelzl@38656 ` 1383` ``` qed ``` hoelzl@38656 ` 1384` ```qed ``` hoelzl@35582 ` 1385` hoelzl@39092 ` 1386` ```lemma (in measure_space) positive_integral_translated_density: ``` hoelzl@39092 ` 1387` ``` assumes "f \ borel_measurable M" "g \ borel_measurable M" ``` hoelzl@39092 ` 1388` ``` shows "measure_space.positive_integral M (\A. positive_integral (\x. f x * indicator A x)) g = ``` hoelzl@39092 ` 1389` ``` positive_integral (\x. f x * g x)" (is "measure_space.positive_integral M ?T _ = _") ``` hoelzl@39092 ` 1390` ```proof - ``` hoelzl@39092 ` 1391` ``` from measure_space_density[OF assms(1)] ``` hoelzl@39092 ` 1392` ``` interpret T: measure_space M ?T . ``` hoelzl@39092 ` 1393` ``` from borel_measurable_implies_simple_function_sequence[OF assms(2)] ``` hoelzl@39092 ` 1394` ``` obtain G where G: "\i. simple_function (G i)" "G \ g" by blast ``` hoelzl@39092 ` 1395` ``` note G_borel = borel_measurable_simple_function[OF this(1)] ``` hoelzl@39092 ` 1396` ``` from T.positive_integral_isoton[OF `G \ g` G_borel] ``` hoelzl@39092 ` 1397` ``` have *: "(\i. T.positive_integral (G i)) \ T.positive_integral g" . ``` hoelzl@39092 ` 1398` ``` { fix i ``` hoelzl@39092 ` 1399` ``` have [simp]: "finite (G i ` space M)" ``` hoelzl@39092 ` 1400` ``` using G(1) unfolding simple_function_def by auto ``` hoelzl@39092 ` 1401` ``` have "T.positive_integral (G i) = T.simple_integral (G i)" ``` hoelzl@39092 ` 1402` ``` using G T.positive_integral_eq_simple_integral by simp ``` hoelzl@39092 ` 1403` ``` also have "\ = positive_integral (\x. f x * (\y\G i`space M. y * indicator (G i -` {y} \ space M) x))" ``` hoelzl@39092 ` 1404` ``` apply (simp add: T.simple_integral_def) ``` hoelzl@39092 ` 1405` ``` apply (subst positive_integral_cmult[symmetric]) ``` hoelzl@39092 ` 1406` ``` using G_borel assms(1) apply (fastsimp intro: borel_measurable_indicator borel_measurable_vimage) ``` hoelzl@39092 ` 1407` ``` apply (subst positive_integral_setsum[symmetric]) ``` hoelzl@39092 ` 1408` ``` using G_borel assms(1) apply (fastsimp intro: borel_measurable_indicator borel_measurable_vimage) ``` hoelzl@39092 ` 1409` ``` by (simp add: setsum_right_distrib field_simps) ``` hoelzl@39092 ` 1410` ``` also have "\ = positive_integral (\x. f x * G i x)" ``` hoelzl@39092 ` 1411` ``` by (auto intro!: positive_integral_cong ``` hoelzl@39092 ` 1412` ``` simp: indicator_def if_distrib setsum_cases) ``` hoelzl@39092 ` 1413` ``` finally have "T.positive_integral (G i) = positive_integral (\x. f x * G i x)" . } ``` hoelzl@39092 ` 1414` ``` with * have eq_Tg: "(\i. positive_integral (\x. f x * G i x)) \ T.positive_integral g" by simp ``` hoelzl@39092 ` 1415` ``` from G(2) have "(\i x. f x * G i x) \ (\x. f x * g x)" ``` hoelzl@39092 ` 1416` ``` unfolding isoton_fun_expand by (auto intro!: isoton_cmult_right) ``` hoelzl@39092 ` 1417` ``` then have "(\i. positive_integral (\x. f x * G i x)) \ positive_integral (\x. f x * g x)" ``` hoelzl@39092 ` 1418` ``` using assms(1) G_borel by (auto intro!: positive_integral_isoton borel_measurable_pinfreal_times) ``` hoelzl@39092 ` 1419` ``` with eq_Tg show "T.positive_integral g = positive_integral (\x. f x * g x)" ``` hoelzl@39092 ` 1420` ``` unfolding isoton_def by simp ``` hoelzl@39092 ` 1421` ```qed ``` hoelzl@39092 ` 1422` hoelzl@38656 ` 1423` ```lemma (in measure_space) positive_integral_null_set: ``` hoelzl@40859 ` 1424` ``` assumes "N \ null_sets" shows "positive_integral (\x. u x * indicator N x) = 0" ``` hoelzl@38656 ` 1425` ```proof - ``` hoelzl@40859 ` 1426` ``` have "positive_integral (\x. u x * indicator N x) = positive_integral (\x. 0)" ``` hoelzl@40859 ` 1427` ``` proof (intro positive_integral_cong_AE AE_I) ``` hoelzl@40859 ` 1428` ``` show "{x \ space M. u x * indicator N x \ 0} \ N" ``` hoelzl@40859 ` 1429` ``` by (auto simp: indicator_def) ``` hoelzl@40859 ` 1430` ``` show "\ N = 0" "N \ sets M" ``` hoelzl@40859 ` 1431` ``` using assms by auto ``` hoelzl@35582 ` 1432` ``` qed ``` hoelzl@40859 ` 1433` ``` then show ?thesis by simp ``` hoelzl@38656 ` 1434` ```qed ``` hoelzl@35582 ` 1435` hoelzl@38656 ` 1436` ```lemma (in measure_space) positive_integral_Markov_inequality: ``` hoelzl@38656 ` 1437` ``` assumes borel: "u \ borel_measurable M" and "A \ sets M" and c: "c \ \" ``` hoelzl@38656 ` 1438` ``` shows "\ ({x\space M. 1 \ c * u x} \ A) \ c * positive_integral (\x. u x * indicator A x)" ``` hoelzl@38656 ` 1439` ``` (is "\ ?A \ _ * ?PI") ``` hoelzl@38656 ` 1440` ```proof - ``` hoelzl@38656 ` 1441` ``` have "?A \ sets M" ``` hoelzl@38656 ` 1442` ``` using `A \ sets M` borel by auto ``` hoelzl@38656 ` 1443` ``` hence "\ ?A = positive_integral (\x. indicator ?A x)" ``` hoelzl@38656 ` 1444` ``` using positive_integral_indicator by simp ``` hoelzl@38656 ` 1445` ``` also have "\ \ positive_integral (\x. c * (u x * indicator A x))" ``` hoelzl@38656 ` 1446` ``` proof (rule positive_integral_mono) ``` hoelzl@38656 ` 1447` ``` fix x assume "x \ space M" ``` hoelzl@38656 ` 1448` ``` show "indicator ?A x \ c * (u x * indicator A x)" ``` hoelzl@38656 ` 1449` ``` by (cases "x \ ?A") auto ``` hoelzl@38656 ` 1450` ``` qed ``` hoelzl@38656 ` 1451` ``` also have "\ = c * positive_integral (\x. u x * indicator A x)" ``` hoelzl@38656 ` 1452` ``` using assms ``` hoelzl@38656 ` 1453` ``` by (auto intro!: positive_integral_cmult borel_measurable_indicator) ``` hoelzl@38656 ` 1454` ``` finally show ?thesis . ``` hoelzl@35582 ` 1455` ```qed ``` hoelzl@35582 ` 1456` hoelzl@38656 ` 1457` ```lemma (in measure_space) positive_integral_0_iff: ``` hoelzl@38656 ` 1458` ``` assumes borel: "u \ borel_measurable M" ``` hoelzl@38656 ` 1459` ``` shows "positive_integral u = 0 \ \ {x\space M. u x \ 0} = 0" ``` hoelzl@38656 ` 1460` ``` (is "_ \ \ ?A = 0") ``` hoelzl@35582 ` 1461` ```proof - ``` hoelzl@38656 ` 1462` ``` have A: "?A \ sets M" using borel by auto ``` hoelzl@38656 ` 1463` ``` have u: "positive_integral (\x. u x * indicator ?A x) = positive_integral u" ``` hoelzl@38656 ` 1464` ``` by (auto intro!: positive_integral_cong simp: indicator_def) ``` hoelzl@35582 ` 1465` hoelzl@38656 ` 1466` ``` show ?thesis ``` hoelzl@38656 ` 1467` ``` proof ``` hoelzl@38656 ` 1468` ``` assume "\ ?A = 0" ``` hoelzl@38656 ` 1469` ``` hence "?A \ null_sets" using `?A \ sets M` by auto ``` hoelzl@40859 ` 1470` ``` from positive_integral_null_set[OF this] ``` hoelzl@38656 ` 1471` ``` have "0 = positive_integral (\x. u x * indicator ?A x)" by simp ``` hoelzl@38656 ` 1472` ``` thus "positive_integral u = 0" unfolding u by simp ``` hoelzl@38656