src/HOL/Probability/Lebesgue_Integration.thy
 author hoelzl Mon Aug 23 19:35:57 2010 +0200 (2010-08-23) changeset 38656 d5d342611edb parent 38642 src/HOL/Probability/Lebesgue.thy@8fa437809c67 child 38705 aaee86c0e237 permissions -rw-r--r--
Rewrite the Probability theory.

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