src/HOL/Probability/Lebesgue_Integration.thy
 author haftmann Tue Mar 18 22:11:46 2014 +0100 (2014-03-18) changeset 56212 3253aaf73a01 parent 56193 c726ecfb22b6 child 56213 e5720d3c18f0 permissions -rw-r--r--
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
 hoelzl@42067 ` 1` ```(* Title: HOL/Probability/Lebesgue_Integration.thy ``` hoelzl@42067 ` 2` ``` Author: Johannes Hölzl, TU München ``` hoelzl@42067 ` 3` ``` Author: Armin Heller, TU München ``` hoelzl@42067 ` 4` ```*) ``` hoelzl@38656 ` 5` hoelzl@35582 ` 6` ```header {*Lebesgue Integration*} ``` hoelzl@35582 ` 7` hoelzl@38656 ` 8` ```theory Lebesgue_Integration ``` hoelzl@47694 ` 9` ``` imports Measure_Space Borel_Space ``` hoelzl@35582 ` 10` ```begin ``` hoelzl@35582 ` 11` hoelzl@41981 ` 12` ```lemma tendsto_real_max: ``` hoelzl@41981 ` 13` ``` fixes x y :: real ``` hoelzl@41981 ` 14` ``` assumes "(X ---> x) net" ``` hoelzl@41981 ` 15` ``` assumes "(Y ---> y) net" ``` hoelzl@41981 ` 16` ``` shows "((\x. max (X x) (Y x)) ---> max x y) net" ``` hoelzl@41981 ` 17` ```proof - ``` hoelzl@41981 ` 18` ``` have *: "\x y :: real. max x y = y + ((x - y) + norm (x - y)) / 2" ``` hoelzl@41981 ` 19` ``` by (auto split: split_max simp: field_simps) ``` hoelzl@41981 ` 20` ``` show ?thesis ``` hoelzl@41981 ` 21` ``` unfolding * ``` hoelzl@41981 ` 22` ``` by (intro tendsto_add assms tendsto_divide tendsto_norm tendsto_diff) auto ``` hoelzl@41981 ` 23` ```qed ``` hoelzl@41981 ` 24` hoelzl@47694 ` 25` ```lemma measurable_sets2[intro]: ``` hoelzl@41981 ` 26` ``` assumes "f \ measurable M M'" "g \ measurable M M''" ``` hoelzl@41981 ` 27` ``` and "A \ sets M'" "B \ sets M''" ``` hoelzl@41981 ` 28` ``` shows "f -` A \ g -` B \ space M \ sets M" ``` hoelzl@41981 ` 29` ```proof - ``` hoelzl@41981 ` 30` ``` have "f -` A \ g -` B \ space M = (f -` A \ space M) \ (g -` B \ space M)" ``` hoelzl@41981 ` 31` ``` by auto ``` hoelzl@41981 ` 32` ``` then show ?thesis using assms by (auto intro: measurable_sets) ``` hoelzl@41981 ` 33` ```qed ``` hoelzl@41981 ` 34` hoelzl@38656 ` 35` ```section "Simple function" ``` hoelzl@35582 ` 36` hoelzl@38656 ` 37` ```text {* ``` hoelzl@38656 ` 38` hoelzl@38656 ` 39` ```Our simple functions are not restricted to positive real numbers. Instead ``` hoelzl@38656 ` 40` ```they are just functions with a finite range and are measurable when singleton ``` hoelzl@38656 ` 41` ```sets are measurable. ``` hoelzl@35582 ` 42` hoelzl@38656 ` 43` ```*} ``` hoelzl@38656 ` 44` hoelzl@41689 ` 45` ```definition "simple_function M g \ ``` hoelzl@38656 ` 46` ``` finite (g ` space M) \ ``` hoelzl@38656 ` 47` ``` (\x \ g ` space M. g -` {x} \ space M \ sets M)" ``` hoelzl@36624 ` 48` hoelzl@47694 ` 49` ```lemma simple_functionD: ``` hoelzl@41689 ` 50` ``` assumes "simple_function M g" ``` hoelzl@40875 ` 51` ``` shows "finite (g ` space M)" and "g -` X \ space M \ sets M" ``` hoelzl@40871 ` 52` ```proof - ``` hoelzl@40871 ` 53` ``` show "finite (g ` space M)" ``` hoelzl@40871 ` 54` ``` using assms unfolding simple_function_def by auto ``` hoelzl@40875 ` 55` ``` have "g -` X \ space M = g -` (X \ g`space M) \ space M" by auto ``` hoelzl@40875 ` 56` ``` also have "\ = (\x\X \ g`space M. g-`{x} \ space M)" by auto ``` hoelzl@40875 ` 57` ``` finally show "g -` X \ space M \ sets M" using assms ``` hoelzl@50002 ` 58` ``` by (auto simp del: UN_simps simp: simple_function_def) ``` hoelzl@40871 ` 59` ```qed ``` hoelzl@36624 ` 60` hoelzl@47694 ` 61` ```lemma simple_function_measurable2[intro]: ``` hoelzl@41981 ` 62` ``` assumes "simple_function M f" "simple_function M g" ``` hoelzl@41981 ` 63` ``` shows "f -` A \ g -` B \ space M \ sets M" ``` hoelzl@41981 ` 64` ```proof - ``` hoelzl@41981 ` 65` ``` have "f -` A \ g -` B \ space M = (f -` A \ space M) \ (g -` B \ space M)" ``` hoelzl@41981 ` 66` ``` by auto ``` hoelzl@41981 ` 67` ``` then show ?thesis using assms[THEN simple_functionD(2)] by auto ``` hoelzl@41981 ` 68` ```qed ``` hoelzl@41981 ` 69` hoelzl@47694 ` 70` ```lemma simple_function_indicator_representation: ``` hoelzl@43920 ` 71` ``` fixes f ::"'a \ ereal" ``` hoelzl@41689 ` 72` ``` assumes f: "simple_function M f" and x: "x \ space M" ``` hoelzl@38656 ` 73` ``` shows "f x = (\y \ f ` space M. y * indicator (f -` {y} \ space M) x)" ``` hoelzl@38656 ` 74` ``` (is "?l = ?r") ``` hoelzl@38656 ` 75` ```proof - ``` hoelzl@38705 ` 76` ``` have "?r = (\y \ f ` space M. ``` hoelzl@38656 ` 77` ``` (if y = f x then y * indicator (f -` {y} \ space M) x else 0))" ``` hoelzl@38656 ` 78` ``` by (auto intro!: setsum_cong2) ``` hoelzl@38656 ` 79` ``` also have "... = f x * indicator (f -` {f x} \ space M) x" ``` hoelzl@38656 ` 80` ``` using assms by (auto dest: simple_functionD simp: setsum_delta) ``` hoelzl@38656 ` 81` ``` also have "... = f x" using x by (auto simp: indicator_def) ``` hoelzl@38656 ` 82` ``` finally show ?thesis by auto ``` hoelzl@38656 ` 83` ```qed ``` hoelzl@36624 ` 84` hoelzl@47694 ` 85` ```lemma simple_function_notspace: ``` hoelzl@43920 ` 86` ``` "simple_function M (\x. h x * indicator (- space M) x::ereal)" (is "simple_function M ?h") ``` hoelzl@35692 ` 87` ```proof - ``` hoelzl@38656 ` 88` ``` have "?h ` space M \ {0}" unfolding indicator_def by auto ``` hoelzl@38656 ` 89` ``` hence [simp, intro]: "finite (?h ` space M)" by (auto intro: finite_subset) ``` hoelzl@38656 ` 90` ``` have "?h -` {0} \ space M = space M" by auto ``` hoelzl@38656 ` 91` ``` thus ?thesis unfolding simple_function_def by auto ``` hoelzl@38656 ` 92` ```qed ``` hoelzl@38656 ` 93` hoelzl@47694 ` 94` ```lemma simple_function_cong: ``` hoelzl@38656 ` 95` ``` assumes "\t. t \ space M \ f t = g t" ``` hoelzl@41689 ` 96` ``` shows "simple_function M f \ simple_function M g" ``` hoelzl@38656 ` 97` ```proof - ``` hoelzl@38656 ` 98` ``` have "f ` space M = g ` space M" ``` hoelzl@38656 ` 99` ``` "\x. f -` {x} \ space M = g -` {x} \ space M" ``` hoelzl@38656 ` 100` ``` using assms by (auto intro!: image_eqI) ``` hoelzl@38656 ` 101` ``` thus ?thesis unfolding simple_function_def using assms by simp ``` hoelzl@38656 ` 102` ```qed ``` hoelzl@38656 ` 103` hoelzl@47694 ` 104` ```lemma simple_function_cong_algebra: ``` hoelzl@41689 ` 105` ``` assumes "sets N = sets M" "space N = space M" ``` hoelzl@41689 ` 106` ``` shows "simple_function M f \ simple_function N f" ``` hoelzl@41689 ` 107` ``` unfolding simple_function_def assms .. ``` hoelzl@41689 ` 108` hoelzl@50003 ` 109` ```lemma borel_measurable_simple_function[measurable_dest]: ``` hoelzl@41689 ` 110` ``` assumes "simple_function M f" ``` hoelzl@38656 ` 111` ``` shows "f \ borel_measurable M" ``` hoelzl@38656 ` 112` ```proof (rule borel_measurableI) ``` hoelzl@38656 ` 113` ``` fix S ``` hoelzl@38656 ` 114` ``` let ?I = "f ` (f -` S \ space M)" ``` hoelzl@38656 ` 115` ``` have *: "(\x\?I. f -` {x} \ space M) = f -` S \ space M" (is "?U = _") by auto ``` hoelzl@38656 ` 116` ``` have "finite ?I" ``` hoelzl@41689 ` 117` ``` using assms unfolding simple_function_def ``` hoelzl@41689 ` 118` ``` using finite_subset[of "f ` (f -` S \ space M)" "f ` space M"] by auto ``` hoelzl@38656 ` 119` ``` hence "?U \ sets M" ``` immler@50244 ` 120` ``` apply (rule sets.finite_UN) ``` hoelzl@38656 ` 121` ``` using assms unfolding simple_function_def by auto ``` hoelzl@38656 ` 122` ``` thus "f -` S \ space M \ sets M" unfolding * . ``` hoelzl@35692 ` 123` ```qed ``` hoelzl@35692 ` 124` hoelzl@47694 ` 125` ```lemma simple_function_borel_measurable: ``` hoelzl@41981 ` 126` ``` fixes f :: "'a \ 'x::{t2_space}" ``` hoelzl@38656 ` 127` ``` assumes "f \ borel_measurable M" and "finite (f ` space M)" ``` hoelzl@41689 ` 128` ``` shows "simple_function M f" ``` hoelzl@38656 ` 129` ``` using assms unfolding simple_function_def ``` hoelzl@38656 ` 130` ``` by (auto intro: borel_measurable_vimage) ``` hoelzl@38656 ` 131` hoelzl@47694 ` 132` ```lemma simple_function_eq_borel_measurable: ``` hoelzl@43920 ` 133` ``` fixes f :: "'a \ ereal" ``` hoelzl@41981 ` 134` ``` shows "simple_function M f \ finite (f`space M) \ f \ borel_measurable M" ``` hoelzl@47694 ` 135` ``` using simple_function_borel_measurable[of f] borel_measurable_simple_function[of M f] ``` nipkow@44890 ` 136` ``` by (fastforce simp: simple_function_def) ``` hoelzl@41981 ` 137` hoelzl@47694 ` 138` ```lemma simple_function_const[intro, simp]: ``` hoelzl@41689 ` 139` ``` "simple_function M (\x. c)" ``` hoelzl@38656 ` 140` ``` by (auto intro: finite_subset simp: simple_function_def) ``` hoelzl@47694 ` 141` ```lemma simple_function_compose[intro, simp]: ``` hoelzl@41689 ` 142` ``` assumes "simple_function M f" ``` hoelzl@41689 ` 143` ``` shows "simple_function M (g \ f)" ``` hoelzl@38656 ` 144` ``` unfolding simple_function_def ``` hoelzl@38656 ` 145` ```proof safe ``` hoelzl@38656 ` 146` ``` show "finite ((g \ f) ` space M)" ``` haftmann@56154 ` 147` ``` using assms unfolding simple_function_def by (auto simp: image_comp [symmetric]) ``` hoelzl@38656 ` 148` ```next ``` hoelzl@38656 ` 149` ``` fix x assume "x \ space M" ``` hoelzl@38656 ` 150` ``` let ?G = "g -` {g (f x)} \ (f`space M)" ``` hoelzl@38656 ` 151` ``` have *: "(g \ f) -` {(g \ f) x} \ space M = ``` hoelzl@38656 ` 152` ``` (\x\?G. f -` {x} \ space M)" by auto ``` hoelzl@38656 ` 153` ``` show "(g \ f) -` {(g \ f) x} \ space M \ sets M" ``` hoelzl@38656 ` 154` ``` using assms unfolding simple_function_def * ``` immler@50244 ` 155` ``` by (rule_tac sets.finite_UN) auto ``` hoelzl@38656 ` 156` ```qed ``` hoelzl@38656 ` 157` hoelzl@47694 ` 158` ```lemma simple_function_indicator[intro, simp]: ``` hoelzl@38656 ` 159` ``` assumes "A \ sets M" ``` hoelzl@41689 ` 160` ``` shows "simple_function M (indicator A)" ``` hoelzl@35692 ` 161` ```proof - ``` hoelzl@38656 ` 162` ``` have "indicator A ` space M \ {0, 1}" (is "?S \ _") ``` hoelzl@38656 ` 163` ``` by (auto simp: indicator_def) ``` hoelzl@38656 ` 164` ``` hence "finite ?S" by (rule finite_subset) simp ``` hoelzl@38656 ` 165` ``` moreover have "- A \ space M = space M - A" by auto ``` hoelzl@38656 ` 166` ``` ultimately show ?thesis unfolding simple_function_def ``` wenzelm@46905 ` 167` ``` using assms by (auto simp: indicator_def [abs_def]) ``` hoelzl@35692 ` 168` ```qed ``` hoelzl@35692 ` 169` hoelzl@47694 ` 170` ```lemma simple_function_Pair[intro, simp]: ``` hoelzl@41689 ` 171` ``` assumes "simple_function M f" ``` hoelzl@41689 ` 172` ``` assumes "simple_function M g" ``` hoelzl@41689 ` 173` ``` shows "simple_function M (\x. (f x, g x))" (is "simple_function M ?p") ``` hoelzl@38656 ` 174` ``` unfolding simple_function_def ``` hoelzl@38656 ` 175` ```proof safe ``` hoelzl@38656 ` 176` ``` show "finite (?p ` space M)" ``` hoelzl@38656 ` 177` ``` using assms unfolding simple_function_def ``` hoelzl@38656 ` 178` ``` by (rule_tac finite_subset[of _ "f`space M \ g`space M"]) auto ``` hoelzl@38656 ` 179` ```next ``` hoelzl@38656 ` 180` ``` fix x assume "x \ space M" ``` hoelzl@38656 ` 181` ``` have "(\x. (f x, g x)) -` {(f x, g x)} \ space M = ``` hoelzl@38656 ` 182` ``` (f -` {f x} \ space M) \ (g -` {g x} \ space M)" ``` hoelzl@38656 ` 183` ``` by auto ``` hoelzl@38656 ` 184` ``` with `x \ space M` show "(\x. (f x, g x)) -` {(f x, g x)} \ space M \ sets M" ``` hoelzl@38656 ` 185` ``` using assms unfolding simple_function_def by auto ``` hoelzl@38656 ` 186` ```qed ``` hoelzl@35692 ` 187` hoelzl@47694 ` 188` ```lemma simple_function_compose1: ``` hoelzl@41689 ` 189` ``` assumes "simple_function M f" ``` hoelzl@41689 ` 190` ``` shows "simple_function M (\x. g (f x))" ``` hoelzl@38656 ` 191` ``` using simple_function_compose[OF assms, of g] ``` hoelzl@38656 ` 192` ``` by (simp add: comp_def) ``` hoelzl@35582 ` 193` hoelzl@47694 ` 194` ```lemma simple_function_compose2: ``` hoelzl@41689 ` 195` ``` assumes "simple_function M f" and "simple_function M g" ``` hoelzl@41689 ` 196` ``` shows "simple_function M (\x. h (f x) (g x))" ``` hoelzl@38656 ` 197` ```proof - ``` hoelzl@41689 ` 198` ``` have "simple_function M ((\(x, y). h x y) \ (\x. (f x, g x)))" ``` hoelzl@38656 ` 199` ``` using assms by auto ``` hoelzl@38656 ` 200` ``` thus ?thesis by (simp_all add: comp_def) ``` hoelzl@38656 ` 201` ```qed ``` hoelzl@35582 ` 202` hoelzl@47694 ` 203` ```lemmas simple_function_add[intro, simp] = simple_function_compose2[where h="op +"] ``` hoelzl@38656 ` 204` ``` and simple_function_diff[intro, simp] = simple_function_compose2[where h="op -"] ``` hoelzl@38656 ` 205` ``` and simple_function_uminus[intro, simp] = simple_function_compose[where g="uminus"] ``` hoelzl@38656 ` 206` ``` and simple_function_mult[intro, simp] = simple_function_compose2[where h="op *"] ``` hoelzl@38656 ` 207` ``` and simple_function_div[intro, simp] = simple_function_compose2[where h="op /"] ``` hoelzl@38656 ` 208` ``` and simple_function_inverse[intro, simp] = simple_function_compose[where g="inverse"] ``` hoelzl@41981 ` 209` ``` and simple_function_max[intro, simp] = simple_function_compose2[where h=max] ``` hoelzl@38656 ` 210` hoelzl@47694 ` 211` ```lemma simple_function_setsum[intro, simp]: ``` hoelzl@41689 ` 212` ``` assumes "\i. i \ P \ simple_function M (f i)" ``` hoelzl@41689 ` 213` ``` shows "simple_function M (\x. \i\P. f i x)" ``` hoelzl@38656 ` 214` ```proof cases ``` hoelzl@38656 ` 215` ``` assume "finite P" from this assms show ?thesis by induct auto ``` hoelzl@38656 ` 216` ```qed auto ``` hoelzl@35582 ` 217` hoelzl@47694 ` 218` ```lemma ``` hoelzl@41981 ` 219` ``` fixes f g :: "'a \ real" assumes sf: "simple_function M f" ``` hoelzl@43920 ` 220` ``` shows simple_function_ereal[intro, simp]: "simple_function M (\x. ereal (f x))" ``` hoelzl@41981 ` 221` ``` by (auto intro!: simple_function_compose1[OF sf]) ``` hoelzl@41981 ` 222` hoelzl@47694 ` 223` ```lemma ``` hoelzl@41981 ` 224` ``` fixes f g :: "'a \ nat" assumes sf: "simple_function M f" ``` hoelzl@41981 ` 225` ``` shows simple_function_real_of_nat[intro, simp]: "simple_function M (\x. real (f x))" ``` hoelzl@41981 ` 226` ``` by (auto intro!: simple_function_compose1[OF sf]) ``` hoelzl@35582 ` 227` hoelzl@47694 ` 228` ```lemma borel_measurable_implies_simple_function_sequence: ``` hoelzl@43920 ` 229` ``` fixes u :: "'a \ ereal" ``` hoelzl@38656 ` 230` ``` assumes u: "u \ borel_measurable M" ``` hoelzl@41981 ` 231` ``` shows "\f. incseq f \ (\i. \ \ range (f i) \ simple_function M (f i)) \ ``` hoelzl@41981 ` 232` ``` (\x. (SUP i. f i x) = max 0 (u x)) \ (\i x. 0 \ f i x)" ``` hoelzl@35582 ` 233` ```proof - ``` hoelzl@41981 ` 234` ``` def f \ "\x i. if real i \ u x then i * 2 ^ i else natfloor (real (u x) * 2 ^ i)" ``` hoelzl@41981 ` 235` ``` { fix x j have "f x j \ j * 2 ^ j" unfolding f_def ``` hoelzl@41981 ` 236` ``` proof (split split_if, intro conjI impI) ``` hoelzl@41981 ` 237` ``` assume "\ real j \ u x" ``` hoelzl@41981 ` 238` ``` then have "natfloor (real (u x) * 2 ^ j) \ natfloor (j * 2 ^ j)" ``` hoelzl@41981 ` 239` ``` by (cases "u x") (auto intro!: natfloor_mono simp: mult_nonneg_nonneg) ``` hoelzl@41981 ` 240` ``` moreover have "real (natfloor (j * 2 ^ j)) \ j * 2^j" ``` hoelzl@41981 ` 241` ``` by (intro real_natfloor_le) (auto simp: mult_nonneg_nonneg) ``` hoelzl@41981 ` 242` ``` ultimately show "natfloor (real (u x) * 2 ^ j) \ j * 2 ^ j" ``` hoelzl@41981 ` 243` ``` unfolding real_of_nat_le_iff by auto ``` hoelzl@41981 ` 244` ``` qed auto } ``` hoelzl@38656 ` 245` ``` note f_upper = this ``` hoelzl@35582 ` 246` hoelzl@41981 ` 247` ``` have real_f: ``` hoelzl@41981 ` 248` ``` "\i x. real (f x i) = (if real i \ u x then i * 2 ^ i else real (natfloor (real (u x) * 2 ^ i)))" ``` hoelzl@41981 ` 249` ``` unfolding f_def by auto ``` hoelzl@35582 ` 250` wenzelm@46731 ` 251` ``` let ?g = "\j x. real (f x j) / 2^j :: ereal" ``` hoelzl@41981 ` 252` ``` show ?thesis ``` hoelzl@41981 ` 253` ``` proof (intro exI[of _ ?g] conjI allI ballI) ``` hoelzl@41981 ` 254` ``` fix i ``` hoelzl@41981 ` 255` ``` have "simple_function M (\x. real (f x i))" ``` hoelzl@41981 ` 256` ``` proof (intro simple_function_borel_measurable) ``` hoelzl@41981 ` 257` ``` show "(\x. real (f x i)) \ borel_measurable M" ``` hoelzl@50021 ` 258` ``` using u by (auto simp: real_f) ``` hoelzl@41981 ` 259` ``` have "(\x. real (f x i))`space M \ real`{..i*2^i}" ``` hoelzl@41981 ` 260` ``` using f_upper[of _ i] by auto ``` hoelzl@41981 ` 261` ``` then show "finite ((\x. real (f x i))`space M)" ``` hoelzl@41981 ` 262` ``` by (rule finite_subset) auto ``` hoelzl@41981 ` 263` ``` qed ``` hoelzl@41981 ` 264` ``` then show "simple_function M (?g i)" ``` hoelzl@43920 ` 265` ``` by (auto intro: simple_function_ereal simple_function_div) ``` hoelzl@41981 ` 266` ``` next ``` hoelzl@41981 ` 267` ``` show "incseq ?g" ``` hoelzl@43920 ` 268` ``` proof (intro incseq_ereal incseq_SucI le_funI) ``` hoelzl@41981 ` 269` ``` fix x and i :: nat ``` hoelzl@41981 ` 270` ``` have "f x i * 2 \ f x (Suc i)" unfolding f_def ``` hoelzl@41981 ` 271` ``` proof ((split split_if)+, intro conjI impI) ``` hoelzl@43920 ` 272` ``` assume "ereal (real i) \ u x" "\ ereal (real (Suc i)) \ u x" ``` hoelzl@41981 ` 273` ``` then show "i * 2 ^ i * 2 \ natfloor (real (u x) * 2 ^ Suc i)" ``` hoelzl@41981 ` 274` ``` by (cases "u x") (auto intro!: le_natfloor) ``` hoelzl@38656 ` 275` ``` next ``` hoelzl@43920 ` 276` ``` assume "\ ereal (real i) \ u x" "ereal (real (Suc i)) \ u x" ``` hoelzl@41981 ` 277` ``` then show "natfloor (real (u x) * 2 ^ i) * 2 \ Suc i * 2 ^ Suc i" ``` hoelzl@41981 ` 278` ``` by (cases "u x") auto ``` hoelzl@41981 ` 279` ``` next ``` hoelzl@43920 ` 280` ``` assume "\ ereal (real i) \ u x" "\ ereal (real (Suc i)) \ u x" ``` hoelzl@41981 ` 281` ``` have "natfloor (real (u x) * 2 ^ i) * 2 = natfloor (real (u x) * 2 ^ i) * natfloor 2" ``` hoelzl@41981 ` 282` ``` by simp ``` hoelzl@41981 ` 283` ``` also have "\ \ natfloor (real (u x) * 2 ^ i * 2)" ``` hoelzl@41981 ` 284` ``` proof cases ``` hoelzl@41981 ` 285` ``` assume "0 \ u x" then show ?thesis ``` bulwahn@46671 ` 286` ``` by (intro le_mult_natfloor) ``` hoelzl@41981 ` 287` ``` next ``` hoelzl@41981 ` 288` ``` assume "\ 0 \ u x" then show ?thesis ``` hoelzl@41981 ` 289` ``` by (cases "u x") (auto simp: natfloor_neg mult_nonpos_nonneg) ``` hoelzl@38656 ` 290` ``` qed ``` hoelzl@41981 ` 291` ``` also have "\ = natfloor (real (u x) * 2 ^ Suc i)" ``` hoelzl@41981 ` 292` ``` by (simp add: ac_simps) ``` hoelzl@41981 ` 293` ``` finally show "natfloor (real (u x) * 2 ^ i) * 2 \ natfloor (real (u x) * 2 ^ Suc i)" . ``` hoelzl@41981 ` 294` ``` qed simp ``` hoelzl@41981 ` 295` ``` then show "?g i x \ ?g (Suc i) x" ``` hoelzl@41981 ` 296` ``` by (auto simp: field_simps) ``` hoelzl@35582 ` 297` ``` qed ``` hoelzl@38656 ` 298` ``` next ``` hoelzl@41981 ` 299` ``` fix x show "(SUP i. ?g i x) = max 0 (u x)" ``` hoelzl@51000 ` 300` ``` proof (rule SUP_eqI) ``` hoelzl@41981 ` 301` ``` fix i show "?g i x \ max 0 (u x)" unfolding max_def f_def ``` hoelzl@41981 ` 302` ``` by (cases "u x") (auto simp: field_simps real_natfloor_le natfloor_neg ``` hoelzl@41981 ` 303` ``` mult_nonpos_nonneg mult_nonneg_nonneg) ``` hoelzl@41981 ` 304` ``` next ``` hoelzl@41981 ` 305` ``` fix y assume *: "\i. i \ UNIV \ ?g i x \ y" ``` hoelzl@41981 ` 306` ``` have "\i. 0 \ ?g i x" by (auto simp: divide_nonneg_pos) ``` hoelzl@41981 ` 307` ``` from order_trans[OF this *] have "0 \ y" by simp ``` hoelzl@41981 ` 308` ``` show "max 0 (u x) \ y" ``` hoelzl@41981 ` 309` ``` proof (cases y) ``` hoelzl@41981 ` 310` ``` case (real r) ``` hoelzl@41981 ` 311` ``` with * have *: "\i. f x i \ r * 2^i" by (auto simp: divide_le_eq) ``` huffman@44666 ` 312` ``` from reals_Archimedean2[of r] * have "u x \ \" by (auto simp: f_def) (metis less_le_not_le) ``` hoelzl@43920 ` 313` ``` then have "\p. max 0 (u x) = ereal p \ 0 \ p" by (cases "u x") (auto simp: max_def) ``` hoelzl@41981 ` 314` ``` then guess p .. note ux = this ``` huffman@44666 ` 315` ``` obtain m :: nat where m: "p < real m" using reals_Archimedean2 .. ``` hoelzl@41981 ` 316` ``` have "p \ r" ``` hoelzl@41981 ` 317` ``` proof (rule ccontr) ``` hoelzl@41981 ` 318` ``` assume "\ p \ r" ``` hoelzl@41981 ` 319` ``` with LIMSEQ_inverse_realpow_zero[unfolded LIMSEQ_iff, rule_format, of 2 "p - r"] ``` hoelzl@41981 ` 320` ``` obtain N where "\n\N. r * 2^n < p * 2^n - 1" by (auto simp: inverse_eq_divide field_simps) ``` hoelzl@41981 ` 321` ``` then have "r * 2^max N m < p * 2^max N m - 1" by simp ``` hoelzl@41981 ` 322` ``` moreover ``` hoelzl@41981 ` 323` ``` have "real (natfloor (p * 2 ^ max N m)) \ r * 2 ^ max N m" ``` hoelzl@41981 ` 324` ``` using *[of "max N m"] m unfolding real_f using ux ``` hoelzl@41981 ` 325` ``` by (cases "0 \ u x") (simp_all add: max_def mult_nonneg_nonneg split: split_if_asm) ``` hoelzl@41981 ` 326` ``` then have "p * 2 ^ max N m - 1 < r * 2 ^ max N m" ``` hoelzl@41981 ` 327` ``` by (metis real_natfloor_gt_diff_one less_le_trans) ``` hoelzl@41981 ` 328` ``` ultimately show False by auto ``` hoelzl@38656 ` 329` ``` qed ``` hoelzl@41981 ` 330` ``` then show "max 0 (u x) \ y" using real ux by simp ``` hoelzl@41981 ` 331` ``` qed (insert `0 \ y`, auto) ``` hoelzl@41981 ` 332` ``` qed ``` hoelzl@41981 ` 333` ``` qed (auto simp: divide_nonneg_pos) ``` hoelzl@41981 ` 334` ```qed ``` hoelzl@35582 ` 335` hoelzl@47694 ` 336` ```lemma borel_measurable_implies_simple_function_sequence': ``` hoelzl@43920 ` 337` ``` fixes u :: "'a \ ereal" ``` hoelzl@41981 ` 338` ``` assumes u: "u \ borel_measurable M" ``` hoelzl@41981 ` 339` ``` obtains f where "\i. simple_function M (f i)" "incseq f" "\i. \ \ range (f i)" ``` hoelzl@41981 ` 340` ``` "\x. (SUP i. f i x) = max 0 (u x)" "\i x. 0 \ f i x" ``` hoelzl@41981 ` 341` ``` using borel_measurable_implies_simple_function_sequence[OF u] by auto ``` hoelzl@41981 ` 342` hoelzl@49796 ` 343` ```lemma simple_function_induct[consumes 1, case_names cong set mult add, induct set: simple_function]: ``` hoelzl@49796 ` 344` ``` fixes u :: "'a \ ereal" ``` hoelzl@49796 ` 345` ``` assumes u: "simple_function M u" ``` hoelzl@49796 ` 346` ``` assumes cong: "\f g. simple_function M f \ simple_function M g \ (AE x in M. f x = g x) \ P f \ P g" ``` hoelzl@49796 ` 347` ``` assumes set: "\A. A \ sets M \ P (indicator A)" ``` hoelzl@49796 ` 348` ``` assumes mult: "\u c. P u \ P (\x. c * u x)" ``` hoelzl@49796 ` 349` ``` assumes add: "\u v. P u \ P v \ P (\x. v x + u x)" ``` hoelzl@49796 ` 350` ``` shows "P u" ``` hoelzl@49796 ` 351` ```proof (rule cong) ``` hoelzl@49796 ` 352` ``` from AE_space show "AE x in M. (\y\u ` space M. y * indicator (u -` {y} \ space M) x) = u x" ``` hoelzl@49796 ` 353` ``` proof eventually_elim ``` hoelzl@49796 ` 354` ``` fix x assume x: "x \ space M" ``` hoelzl@49796 ` 355` ``` from simple_function_indicator_representation[OF u x] ``` hoelzl@49796 ` 356` ``` show "(\y\u ` space M. y * indicator (u -` {y} \ space M) x) = u x" .. ``` hoelzl@49796 ` 357` ``` qed ``` hoelzl@49796 ` 358` ```next ``` hoelzl@49796 ` 359` ``` from u have "finite (u ` space M)" ``` hoelzl@49796 ` 360` ``` unfolding simple_function_def by auto ``` hoelzl@49796 ` 361` ``` then show "P (\x. \y\u ` space M. y * indicator (u -` {y} \ space M) x)" ``` hoelzl@49796 ` 362` ``` proof induct ``` hoelzl@49796 ` 363` ``` case empty show ?case ``` hoelzl@49796 ` 364` ``` using set[of "{}"] by (simp add: indicator_def[abs_def]) ``` hoelzl@49796 ` 365` ``` qed (auto intro!: add mult set simple_functionD u) ``` hoelzl@49796 ` 366` ```next ``` hoelzl@49796 ` 367` ``` show "simple_function M (\x. (\y\u ` space M. y * indicator (u -` {y} \ space M) x))" ``` hoelzl@49796 ` 368` ``` apply (subst simple_function_cong) ``` hoelzl@49796 ` 369` ``` apply (rule simple_function_indicator_representation[symmetric]) ``` hoelzl@49796 ` 370` ``` apply (auto intro: u) ``` hoelzl@49796 ` 371` ``` done ``` hoelzl@49796 ` 372` ```qed fact ``` hoelzl@49796 ` 373` hoelzl@49796 ` 374` ```lemma simple_function_induct_nn[consumes 2, case_names cong set mult add]: ``` hoelzl@49796 ` 375` ``` fixes u :: "'a \ ereal" ``` hoelzl@49799 ` 376` ``` assumes u: "simple_function M u" and nn: "\x. 0 \ u x" ``` hoelzl@49799 ` 377` ``` assumes cong: "\f g. simple_function M f \ simple_function M g \ (\x. x \ space M \ f x = g x) \ P f \ P g" ``` hoelzl@49796 ` 378` ``` assumes set: "\A. A \ sets M \ P (indicator A)" ``` hoelzl@49797 ` 379` ``` assumes mult: "\u c. 0 \ c \ simple_function M u \ (\x. 0 \ u x) \ P u \ P (\x. c * u x)" ``` hoelzl@49797 ` 380` ``` assumes add: "\u v. simple_function M u \ (\x. 0 \ u x) \ P u \ simple_function M v \ (\x. 0 \ v x) \ P v \ P (\x. v x + u x)" ``` hoelzl@49796 ` 381` ``` shows "P u" ``` hoelzl@49796 ` 382` ```proof - ``` hoelzl@49796 ` 383` ``` show ?thesis ``` hoelzl@49796 ` 384` ``` proof (rule cong) ``` hoelzl@49799 ` 385` ``` fix x assume x: "x \ space M" ``` hoelzl@49799 ` 386` ``` from simple_function_indicator_representation[OF u x] ``` hoelzl@49799 ` 387` ``` show "(\y\u ` space M. y * indicator (u -` {y} \ space M) x) = u x" .. ``` hoelzl@49796 ` 388` ``` next ``` hoelzl@49799 ` 389` ``` show "simple_function M (\x. (\y\u ` space M. y * indicator (u -` {y} \ space M) x))" ``` hoelzl@49796 ` 390` ``` apply (subst simple_function_cong) ``` hoelzl@49796 ` 391` ``` apply (rule simple_function_indicator_representation[symmetric]) ``` hoelzl@49799 ` 392` ``` apply (auto intro: u) ``` hoelzl@49796 ` 393` ``` done ``` hoelzl@49796 ` 394` ``` next ``` hoelzl@49799 ` 395` ``` from u nn have "finite (u ` space M)" "\x. x \ u ` space M \ 0 \ x" ``` hoelzl@49796 ` 396` ``` unfolding simple_function_def by auto ``` hoelzl@49799 ` 397` ``` then show "P (\x. \y\u ` space M. y * indicator (u -` {y} \ space M) x)" ``` hoelzl@49796 ` 398` ``` proof induct ``` hoelzl@49796 ` 399` ``` case empty show ?case ``` hoelzl@49796 ` 400` ``` using set[of "{}"] by (simp add: indicator_def[abs_def]) ``` hoelzl@49799 ` 401` ``` qed (auto intro!: add mult set simple_functionD u setsum_nonneg ``` hoelzl@49797 ` 402` ``` simple_function_setsum) ``` hoelzl@49796 ` 403` ``` qed fact ``` hoelzl@49796 ` 404` ```qed ``` hoelzl@49796 ` 405` hoelzl@49796 ` 406` ```lemma borel_measurable_induct[consumes 2, case_names cong set mult add seq, induct set: borel_measurable]: ``` hoelzl@49796 ` 407` ``` fixes u :: "'a \ ereal" ``` hoelzl@49799 ` 408` ``` assumes u: "u \ borel_measurable M" "\x. 0 \ u x" ``` hoelzl@49799 ` 409` ``` assumes cong: "\f g. f \ borel_measurable M \ g \ borel_measurable M \ (\x. x \ space M \ f x = g x) \ P g \ P f" ``` hoelzl@49796 ` 410` ``` assumes set: "\A. A \ sets M \ P (indicator A)" ``` hoelzl@49797 ` 411` ``` assumes mult: "\u c. 0 \ c \ u \ borel_measurable M \ (\x. 0 \ u x) \ P u \ P (\x. c * u x)" ``` hoelzl@49797 ` 412` ``` assumes add: "\u v. u \ borel_measurable M \ (\x. 0 \ u x) \ P u \ v \ borel_measurable M \ (\x. 0 \ v x) \ P v \ P (\x. v x + u x)" ``` hoelzl@49797 ` 413` ``` assumes seq: "\U. (\i. U i \ borel_measurable M) \ (\i x. 0 \ U i x) \ (\i. P (U i)) \ incseq U \ P (SUP i. U i)" ``` hoelzl@49796 ` 414` ``` shows "P u" ``` hoelzl@49796 ` 415` ``` using u ``` hoelzl@49796 ` 416` ```proof (induct rule: borel_measurable_implies_simple_function_sequence') ``` hoelzl@49797 ` 417` ``` fix U assume U: "\i. simple_function M (U i)" "incseq U" "\i. \ \ range (U i)" and ``` hoelzl@49796 ` 418` ``` sup: "\x. (SUP i. U i x) = max 0 (u x)" and nn: "\i x. 0 \ U i x" ``` hoelzl@49799 ` 419` ``` have u_eq: "u = (SUP i. U i)" ``` hoelzl@49796 ` 420` ``` using nn u sup by (auto simp: max_def) ``` hoelzl@49796 ` 421` ``` ``` hoelzl@49797 ` 422` ``` from U have "\i. U i \ borel_measurable M" ``` hoelzl@49797 ` 423` ``` by (simp add: borel_measurable_simple_function) ``` hoelzl@49797 ` 424` hoelzl@49799 ` 425` ``` show "P u" ``` hoelzl@49796 ` 426` ``` unfolding u_eq ``` hoelzl@49796 ` 427` ``` proof (rule seq) ``` hoelzl@49796 ` 428` ``` fix i show "P (U i)" ``` hoelzl@49799 ` 429` ``` using `simple_function M (U i)` nn ``` hoelzl@49796 ` 430` ``` by (induct rule: simple_function_induct_nn) ``` hoelzl@49796 ` 431` ``` (auto intro: set mult add cong dest!: borel_measurable_simple_function) ``` hoelzl@49797 ` 432` ``` qed fact+ ``` hoelzl@49796 ` 433` ```qed ``` hoelzl@49796 ` 434` hoelzl@47694 ` 435` ```lemma simple_function_If_set: ``` hoelzl@41981 ` 436` ``` assumes sf: "simple_function M f" "simple_function M g" and A: "A \ space M \ sets M" ``` hoelzl@41981 ` 437` ``` shows "simple_function M (\x. if x \ A then f x else g x)" (is "simple_function M ?IF") ``` hoelzl@41981 ` 438` ```proof - ``` hoelzl@41981 ` 439` ``` def F \ "\x. f -` {x} \ space M" and G \ "\x. g -` {x} \ space M" ``` hoelzl@41981 ` 440` ``` show ?thesis unfolding simple_function_def ``` hoelzl@41981 ` 441` ``` proof safe ``` hoelzl@41981 ` 442` ``` have "?IF ` space M \ f ` space M \ g ` space M" by auto ``` hoelzl@41981 ` 443` ``` from finite_subset[OF this] assms ``` hoelzl@41981 ` 444` ``` show "finite (?IF ` space M)" unfolding simple_function_def by auto ``` hoelzl@41981 ` 445` ``` next ``` hoelzl@41981 ` 446` ``` fix x assume "x \ space M" ``` hoelzl@41981 ` 447` ``` then have *: "?IF -` {?IF x} \ space M = (if x \ A ``` hoelzl@41981 ` 448` ``` then ((F (f x) \ (A \ space M)) \ (G (f x) - (G (f x) \ (A \ space M)))) ``` hoelzl@41981 ` 449` ``` else ((F (g x) \ (A \ space M)) \ (G (g x) - (G (g x) \ (A \ space M)))))" ``` immler@50244 ` 450` ``` using sets.sets_into_space[OF A] by (auto split: split_if_asm simp: G_def F_def) ``` hoelzl@41981 ` 451` ``` have [intro]: "\x. F x \ sets M" "\x. G x \ sets M" ``` hoelzl@41981 ` 452` ``` unfolding F_def G_def using sf[THEN simple_functionD(2)] by auto ``` hoelzl@41981 ` 453` ``` show "?IF -` {?IF x} \ space M \ sets M" unfolding * using A by auto ``` hoelzl@35582 ` 454` ``` qed ``` hoelzl@35582 ` 455` ```qed ``` hoelzl@35582 ` 456` hoelzl@47694 ` 457` ```lemma simple_function_If: ``` hoelzl@41981 ` 458` ``` assumes sf: "simple_function M f" "simple_function M g" and P: "{x\space M. P x} \ sets M" ``` hoelzl@41981 ` 459` ``` shows "simple_function M (\x. if P x then f x else g x)" ``` hoelzl@35582 ` 460` ```proof - ``` hoelzl@41981 ` 461` ``` have "{x\space M. P x} = {x. P x} \ space M" by auto ``` hoelzl@41981 ` 462` ``` with simple_function_If_set[OF sf, of "{x. P x}"] P show ?thesis by simp ``` hoelzl@38656 ` 463` ```qed ``` hoelzl@38656 ` 464` hoelzl@47694 ` 465` ```lemma simple_function_subalgebra: ``` hoelzl@41689 ` 466` ``` assumes "simple_function N f" ``` hoelzl@41689 ` 467` ``` and N_subalgebra: "sets N \ sets M" "space N = space M" ``` hoelzl@41689 ` 468` ``` shows "simple_function M f" ``` hoelzl@41689 ` 469` ``` using assms unfolding simple_function_def by auto ``` hoelzl@39092 ` 470` hoelzl@47694 ` 471` ```lemma simple_function_comp: ``` hoelzl@47694 ` 472` ``` assumes T: "T \ measurable M M'" ``` hoelzl@41689 ` 473` ``` and f: "simple_function M' f" ``` hoelzl@41689 ` 474` ``` shows "simple_function M (\x. f (T x))" ``` hoelzl@41661 ` 475` ```proof (intro simple_function_def[THEN iffD2] conjI ballI) ``` hoelzl@41661 ` 476` ``` have "(\x. f (T x)) ` space M \ f ` space M'" ``` hoelzl@41661 ` 477` ``` using T unfolding measurable_def by auto ``` hoelzl@41661 ` 478` ``` then show "finite ((\x. f (T x)) ` space M)" ``` hoelzl@41689 ` 479` ``` using f unfolding simple_function_def by (auto intro: finite_subset) ``` hoelzl@41661 ` 480` ``` fix i assume i: "i \ (\x. f (T x)) ` space M" ``` hoelzl@41661 ` 481` ``` then have "i \ f ` space M'" ``` hoelzl@41661 ` 482` ``` using T unfolding measurable_def by auto ``` hoelzl@41661 ` 483` ``` then have "f -` {i} \ space M' \ sets M'" ``` hoelzl@41689 ` 484` ``` using f unfolding simple_function_def by auto ``` hoelzl@41661 ` 485` ``` then have "T -` (f -` {i} \ space M') \ space M \ sets M" ``` hoelzl@41661 ` 486` ``` using T unfolding measurable_def by auto ``` hoelzl@41661 ` 487` ``` also have "T -` (f -` {i} \ space M') \ space M = (\x. f (T x)) -` {i} \ space M" ``` hoelzl@41661 ` 488` ``` using T unfolding measurable_def by auto ``` hoelzl@41661 ` 489` ``` finally show "(\x. f (T x)) -` {i} \ space M \ sets M" . ``` hoelzl@40859 ` 490` ```qed ``` hoelzl@40859 ` 491` hoelzl@38656 ` 492` ```section "Simple integral" ``` hoelzl@38656 ` 493` wenzelm@53015 ` 494` ```definition simple_integral :: "'a measure \ ('a \ ereal) \ ereal" ("integral\<^sup>S") where ``` wenzelm@53015 ` 495` ``` "integral\<^sup>S M f = (\x \ f ` space M. x * emeasure M (f -` {x} \ space M))" ``` hoelzl@41689 ` 496` hoelzl@41689 ` 497` ```syntax ``` wenzelm@53015 ` 498` ``` "_simple_integral" :: "pttrn \ ereal \ 'a measure \ ereal" ("\\<^sup>S _. _ \_" [60,61] 110) ``` hoelzl@41689 ` 499` hoelzl@41689 ` 500` ```translations ``` wenzelm@53015 ` 501` ``` "\\<^sup>S x. f \M" == "CONST simple_integral M (%x. f)" ``` hoelzl@35582 ` 502` hoelzl@47694 ` 503` ```lemma simple_integral_cong: ``` hoelzl@38656 ` 504` ``` assumes "\t. t \ space M \ f t = g t" ``` wenzelm@53015 ` 505` ``` shows "integral\<^sup>S M f = integral\<^sup>S M g" ``` hoelzl@38656 ` 506` ```proof - ``` hoelzl@38656 ` 507` ``` have "f ` space M = g ` space M" ``` hoelzl@38656 ` 508` ``` "\x. f -` {x} \ space M = g -` {x} \ space M" ``` hoelzl@38656 ` 509` ``` using assms by (auto intro!: image_eqI) ``` hoelzl@38656 ` 510` ``` thus ?thesis unfolding simple_integral_def by simp ``` hoelzl@38656 ` 511` ```qed ``` hoelzl@38656 ` 512` hoelzl@47694 ` 513` ```lemma simple_integral_const[simp]: ``` wenzelm@53015 ` 514` ``` "(\\<^sup>Sx. c \M) = c * (emeasure M) (space M)" ``` hoelzl@38656 ` 515` ```proof (cases "space M = {}") ``` hoelzl@38656 ` 516` ``` case True thus ?thesis unfolding simple_integral_def by simp ``` hoelzl@38656 ` 517` ```next ``` hoelzl@38656 ` 518` ``` case False hence "(\x. c) ` space M = {c}" by auto ``` hoelzl@38656 ` 519` ``` thus ?thesis unfolding simple_integral_def by simp ``` hoelzl@35582 ` 520` ```qed ``` hoelzl@35582 ` 521` hoelzl@47694 ` 522` ```lemma simple_function_partition: ``` hoelzl@41981 ` 523` ``` assumes f: "simple_function M f" and g: "simple_function M g" ``` wenzelm@53015 ` 524` ``` shows "integral\<^sup>S M f = (\A\(\x. f -` {f x} \ g -` {g x} \ space M) ` space M. the_elem (f`A) * (emeasure M) A)" ``` hoelzl@38656 ` 525` ``` (is "_ = setsum _ (?p ` space M)") ``` hoelzl@38656 ` 526` ```proof- ``` wenzelm@46731 ` 527` ``` let ?sub = "\x. ?p ` (f -` {x} \ space M)" ``` hoelzl@38656 ` 528` ``` let ?SIGMA = "Sigma (f`space M) ?sub" ``` hoelzl@35582 ` 529` hoelzl@38656 ` 530` ``` have [intro]: ``` hoelzl@38656 ` 531` ``` "finite (f ` space M)" ``` hoelzl@38656 ` 532` ``` "finite (g ` space M)" ``` hoelzl@38656 ` 533` ``` using assms unfolding simple_function_def by simp_all ``` hoelzl@38656 ` 534` hoelzl@38656 ` 535` ``` { fix A ``` hoelzl@38656 ` 536` ``` have "?p ` (A \ space M) \ ``` hoelzl@38656 ` 537` ``` (\(x,y). f -` {x} \ g -` {y} \ space M) ` (f`space M \ g`space M)" ``` hoelzl@38656 ` 538` ``` by auto ``` hoelzl@38656 ` 539` ``` hence "finite (?p ` (A \ space M))" ``` nipkow@40786 ` 540` ``` by (rule finite_subset) auto } ``` hoelzl@38656 ` 541` ``` note this[intro, simp] ``` hoelzl@41981 ` 542` ``` note sets = simple_function_measurable2[OF f g] ``` hoelzl@35582 ` 543` hoelzl@38656 ` 544` ``` { fix x assume "x \ space M" ``` hoelzl@38656 ` 545` ``` have "\(?sub (f x)) = (f -` {f x} \ space M)" by auto ``` hoelzl@47694 ` 546` ``` with sets have "(emeasure M) (f -` {f x} \ space M) = setsum (emeasure M) (?sub (f x))" ``` hoelzl@47761 ` 547` ``` by (subst setsum_emeasure) (auto simp: disjoint_family_on_def) } ``` wenzelm@53015 ` 548` ``` hence "integral\<^sup>S M f = (\(x,A)\?SIGMA. x * (emeasure M) A)" ``` hoelzl@41981 ` 549` ``` unfolding simple_integral_def using f sets ``` hoelzl@41981 ` 550` ``` by (subst setsum_Sigma[symmetric]) ``` hoelzl@43920 ` 551` ``` (auto intro!: setsum_cong setsum_ereal_right_distrib) ``` hoelzl@47694 ` 552` ``` also have "\ = (\A\?p ` space M. the_elem (f`A) * (emeasure M) A)" ``` hoelzl@38656 ` 553` ``` proof - ``` hoelzl@38656 ` 554` ``` have [simp]: "\x. x \ space M \ f ` ?p x = {f x}" by (auto intro!: imageI) ``` haftmann@39910 ` 555` ``` have "(\A. (the_elem (f ` A), A)) ` ?p ` space M ``` hoelzl@38656 ` 556` ``` = (\x. (f x, ?p x)) ` space M" ``` hoelzl@38656 ` 557` ``` proof safe ``` hoelzl@38656 ` 558` ``` fix x assume "x \ space M" ``` haftmann@39910 ` 559` ``` thus "(f x, ?p x) \ (\A. (the_elem (f`A), A)) ` ?p ` space M" ``` hoelzl@38656 ` 560` ``` by (auto intro!: image_eqI[of _ _ "?p x"]) ``` hoelzl@38656 ` 561` ``` qed auto ``` hoelzl@38656 ` 562` ``` thus ?thesis ``` haftmann@39910 ` 563` ``` apply (auto intro!: setsum_reindex_cong[of "\A. (the_elem (f`A), A)"] inj_onI) ``` hoelzl@38656 ` 564` ``` apply (rule_tac x="xa" in image_eqI) ``` hoelzl@38656 ` 565` ``` by simp_all ``` hoelzl@38656 ` 566` ``` qed ``` hoelzl@38656 ` 567` ``` finally show ?thesis . ``` hoelzl@35582 ` 568` ```qed ``` hoelzl@35582 ` 569` hoelzl@47694 ` 570` ```lemma simple_integral_add[simp]: ``` hoelzl@41981 ` 571` ``` assumes f: "simple_function M f" and "\x. 0 \ f x" and g: "simple_function M g" and "\x. 0 \ g x" ``` wenzelm@53015 ` 572` ``` shows "(\\<^sup>Sx. f x + g x \M) = integral\<^sup>S M f + integral\<^sup>S M g" ``` hoelzl@35582 ` 573` ```proof - ``` hoelzl@38656 ` 574` ``` { fix x let ?S = "g -` {g x} \ f -` {f x} \ space M" ``` hoelzl@38656 ` 575` ``` assume "x \ space M" ``` hoelzl@38656 ` 576` ``` hence "(\a. f a + g a) ` ?S = {f x + g x}" "f ` ?S = {f x}" "g ` ?S = {g x}" ``` hoelzl@38656 ` 577` ``` "(\x. (f x, g x)) -` {(f x, g x)} \ space M = ?S" ``` hoelzl@38656 ` 578` ``` by auto } ``` hoelzl@41981 ` 579` ``` with assms show ?thesis ``` hoelzl@38656 ` 580` ``` unfolding ``` hoelzl@41981 ` 581` ``` simple_function_partition[OF simple_function_add[OF f g] simple_function_Pair[OF f g]] ``` hoelzl@41981 ` 582` ``` simple_function_partition[OF f g] ``` hoelzl@41981 ` 583` ``` simple_function_partition[OF g f] ``` hoelzl@41981 ` 584` ``` by (subst (3) Int_commute) ``` hoelzl@43920 ` 585` ``` (auto simp add: ereal_left_distrib setsum_addf[symmetric] intro!: setsum_cong) ``` hoelzl@35582 ` 586` ```qed ``` hoelzl@35582 ` 587` hoelzl@47694 ` 588` ```lemma simple_integral_setsum[simp]: ``` hoelzl@41981 ` 589` ``` assumes "\i x. i \ P \ 0 \ f i x" ``` hoelzl@41689 ` 590` ``` assumes "\i. i \ P \ simple_function M (f i)" ``` wenzelm@53015 ` 591` ``` shows "(\\<^sup>Sx. (\i\P. f i x) \M) = (\i\P. integral\<^sup>S M (f i))" ``` hoelzl@38656 ` 592` ```proof cases ``` hoelzl@38656 ` 593` ``` assume "finite P" ``` hoelzl@38656 ` 594` ``` from this assms show ?thesis ``` hoelzl@41981 ` 595` ``` by induct (auto simp: simple_function_setsum simple_integral_add setsum_nonneg) ``` hoelzl@38656 ` 596` ```qed auto ``` hoelzl@38656 ` 597` hoelzl@47694 ` 598` ```lemma simple_integral_mult[simp]: ``` hoelzl@41981 ` 599` ``` assumes f: "simple_function M f" "\x. 0 \ f x" ``` wenzelm@53015 ` 600` ``` shows "(\\<^sup>Sx. c * f x \M) = c * integral\<^sup>S M f" ``` hoelzl@38656 ` 601` ```proof - ``` hoelzl@47694 ` 602` ``` note mult = simple_function_mult[OF simple_function_const[of _ c] f(1)] ``` hoelzl@38656 ` 603` ``` { fix x let ?S = "f -` {f x} \ (\x. c * f x) -` {c * f x} \ space M" ``` hoelzl@38656 ` 604` ``` assume "x \ space M" ``` hoelzl@38656 ` 605` ``` hence "(\x. c * f x) ` ?S = {c * f x}" "f ` ?S = {f x}" ``` hoelzl@38656 ` 606` ``` by auto } ``` hoelzl@41981 ` 607` ``` with assms show ?thesis ``` hoelzl@41981 ` 608` ``` unfolding simple_function_partition[OF mult f(1)] ``` hoelzl@41981 ` 609` ``` simple_function_partition[OF f(1) mult] ``` hoelzl@43920 ` 610` ``` by (subst setsum_ereal_right_distrib) ``` hoelzl@43920 ` 611` ``` (auto intro!: ereal_0_le_mult setsum_cong simp: mult_assoc) ``` hoelzl@40871 ` 612` ```qed ``` hoelzl@40871 ` 613` hoelzl@47694 ` 614` ```lemma simple_integral_mono_AE: ``` hoelzl@41981 ` 615` ``` assumes f: "simple_function M f" and g: "simple_function M g" ``` hoelzl@47694 ` 616` ``` and mono: "AE x in M. f x \ g x" ``` wenzelm@53015 ` 617` ``` shows "integral\<^sup>S M f \ integral\<^sup>S M g" ``` hoelzl@40859 ` 618` ```proof - ``` wenzelm@46731 ` 619` ``` let ?S = "\x. (g -` {g x} \ space M) \ (f -` {f x} \ space M)" ``` hoelzl@40859 ` 620` ``` have *: "\x. g -` {g x} \ f -` {f x} \ space M = ?S x" ``` hoelzl@40859 ` 621` ``` "\x. f -` {f x} \ g -` {g x} \ space M = ?S x" by auto ``` hoelzl@40859 ` 622` ``` show ?thesis ``` hoelzl@40859 ` 623` ``` unfolding * ``` hoelzl@41981 ` 624` ``` simple_function_partition[OF f g] ``` hoelzl@41981 ` 625` ``` simple_function_partition[OF g f] ``` hoelzl@40859 ` 626` ``` proof (safe intro!: setsum_mono) ``` hoelzl@40859 ` 627` ``` fix x assume "x \ space M" ``` hoelzl@40859 ` 628` ``` then have *: "f ` ?S x = {f x}" "g ` ?S x = {g x}" by auto ``` hoelzl@47694 ` 629` ``` show "the_elem (f`?S x) * (emeasure M) (?S x) \ the_elem (g`?S x) * (emeasure M) (?S x)" ``` hoelzl@40859 ` 630` ``` proof (cases "f x \ g x") ``` hoelzl@41981 ` 631` ``` case True then show ?thesis ``` hoelzl@41981 ` 632` ``` using * assms(1,2)[THEN simple_functionD(2)] ``` hoelzl@43920 ` 633` ``` by (auto intro!: ereal_mult_right_mono) ``` hoelzl@40859 ` 634` ``` next ``` hoelzl@40859 ` 635` ``` case False ``` hoelzl@47694 ` 636` ``` obtain N where N: "{x\space M. \ f x \ g x} \ N" "N \ sets M" "(emeasure M) N = 0" ``` hoelzl@40859 ` 637` ``` using mono by (auto elim!: AE_E) ``` hoelzl@40859 ` 638` ``` have "?S x \ N" using N `x \ space M` False by auto ``` hoelzl@40871 ` 639` ``` moreover have "?S x \ sets M" using assms ``` immler@50244 ` 640` ``` by (rule_tac sets.Int) (auto intro!: simple_functionD) ``` hoelzl@47694 ` 641` ``` ultimately have "(emeasure M) (?S x) \ (emeasure M) N" ``` hoelzl@47694 ` 642` ``` using `N \ sets M` by (auto intro!: emeasure_mono) ``` hoelzl@47694 ` 643` ``` moreover have "0 \ (emeasure M) (?S x)" ``` hoelzl@41981 ` 644` ``` using assms(1,2)[THEN simple_functionD(2)] by auto ``` hoelzl@47694 ` 645` ``` ultimately have "(emeasure M) (?S x) = 0" using `(emeasure M) N = 0` by auto ``` hoelzl@41981 ` 646` ``` then show ?thesis by simp ``` hoelzl@40859 ` 647` ``` qed ``` hoelzl@40859 ` 648` ``` qed ``` hoelzl@40859 ` 649` ```qed ``` hoelzl@40859 ` 650` hoelzl@47694 ` 651` ```lemma simple_integral_mono: ``` hoelzl@41689 ` 652` ``` assumes "simple_function M f" and "simple_function M g" ``` hoelzl@38656 ` 653` ``` and mono: "\ x. x \ space M \ f x \ g x" ``` wenzelm@53015 ` 654` ``` shows "integral\<^sup>S M f \ integral\<^sup>S M g" ``` hoelzl@41705 ` 655` ``` using assms by (intro simple_integral_mono_AE) auto ``` hoelzl@35582 ` 656` hoelzl@47694 ` 657` ```lemma simple_integral_cong_AE: ``` hoelzl@41981 ` 658` ``` assumes "simple_function M f" and "simple_function M g" ``` hoelzl@47694 ` 659` ``` and "AE x in M. f x = g x" ``` wenzelm@53015 ` 660` ``` shows "integral\<^sup>S M f = integral\<^sup>S M g" ``` hoelzl@40859 ` 661` ``` using assms by (auto simp: eq_iff intro!: simple_integral_mono_AE) ``` hoelzl@40859 ` 662` hoelzl@47694 ` 663` ```lemma simple_integral_cong': ``` hoelzl@41689 ` 664` ``` assumes sf: "simple_function M f" "simple_function M g" ``` hoelzl@47694 ` 665` ``` and mea: "(emeasure M) {x\space M. f x \ g x} = 0" ``` wenzelm@53015 ` 666` ``` shows "integral\<^sup>S M f = integral\<^sup>S M g" ``` hoelzl@40859 ` 667` ```proof (intro simple_integral_cong_AE sf AE_I) ``` hoelzl@47694 ` 668` ``` show "(emeasure M) {x\space M. f x \ g x} = 0" by fact ``` hoelzl@40859 ` 669` ``` show "{x \ space M. f x \ g x} \ sets M" ``` hoelzl@40859 ` 670` ``` using sf[THEN borel_measurable_simple_function] by auto ``` hoelzl@40859 ` 671` ```qed simp ``` hoelzl@40859 ` 672` hoelzl@47694 ` 673` ```lemma simple_integral_indicator: ``` hoelzl@38656 ` 674` ``` assumes "A \ sets M" ``` hoelzl@49796 ` 675` ``` assumes f: "simple_function M f" ``` wenzelm@53015 ` 676` ``` shows "(\\<^sup>Sx. f x * indicator A x \M) = ``` hoelzl@47694 ` 677` ``` (\x \ f ` space M. x * (emeasure M) (f -` {x} \ space M \ A))" ``` wenzelm@53374 ` 678` ```proof (cases "A = space M") ``` wenzelm@53374 ` 679` ``` case True ``` wenzelm@53374 ` 680` ``` then have "(\\<^sup>Sx. f x * indicator A x \M) = integral\<^sup>S M f" ``` hoelzl@38656 ` 681` ``` by (auto intro!: simple_integral_cong) ``` wenzelm@53374 ` 682` ``` with True show ?thesis by (simp add: simple_integral_def) ``` hoelzl@38656 ` 683` ```next ``` hoelzl@38656 ` 684` ``` assume "A \ space M" ``` immler@50244 ` 685` ``` then obtain x where x: "x \ space M" "x \ A" using sets.sets_into_space[OF assms(1)] by auto ``` hoelzl@38656 ` 686` ``` have I: "(\x. f x * indicator A x) ` space M = f ` A \ {0}" (is "?I ` _ = _") ``` hoelzl@35582 ` 687` ``` proof safe ``` hoelzl@38656 ` 688` ``` fix y assume "?I y \ f ` A" hence "y \ A" by auto thus "?I y = 0" by auto ``` hoelzl@38656 ` 689` ``` next ``` hoelzl@38656 ` 690` ``` fix y assume "y \ A" thus "f y \ ?I ` space M" ``` immler@50244 ` 691` ``` using sets.sets_into_space[OF assms(1)] by (auto intro!: image_eqI[of _ _ y]) ``` hoelzl@38656 ` 692` ``` next ``` hoelzl@38656 ` 693` ``` show "0 \ ?I ` space M" using x by (auto intro!: image_eqI[of _ _ x]) ``` hoelzl@35582 ` 694` ``` qed ``` wenzelm@53015 ` 695` ``` have *: "(\\<^sup>Sx. f x * indicator A x \M) = ``` hoelzl@47694 ` 696` ``` (\x \ f ` space M \ {0}. x * (emeasure M) (f -` {x} \ space M \ A))" ``` hoelzl@38656 ` 697` ``` unfolding simple_integral_def I ``` hoelzl@38656 ` 698` ``` proof (rule setsum_mono_zero_cong_left) ``` hoelzl@38656 ` 699` ``` show "finite (f ` space M \ {0})" ``` hoelzl@38656 ` 700` ``` using assms(2) unfolding simple_function_def by auto ``` hoelzl@38656 ` 701` ``` show "f ` A \ {0} \ f`space M \ {0}" ``` immler@50244 ` 702` ``` using sets.sets_into_space[OF assms(1)] by auto ``` hoelzl@40859 ` 703` ``` have "\x. f x \ f ` A \ f -` {f x} \ space M \ A = {}" ``` hoelzl@40859 ` 704` ``` by (auto simp: image_iff) ``` hoelzl@38656 ` 705` ``` thus "\i\f ` space M \ {0} - (f ` A \ {0}). ``` hoelzl@47694 ` 706` ``` i * (emeasure M) (f -` {i} \ space M \ A) = 0" by auto ``` hoelzl@38656 ` 707` ``` next ``` hoelzl@38656 ` 708` ``` fix x assume "x \ f`A \ {0}" ``` hoelzl@38656 ` 709` ``` hence "x \ 0 \ ?I -` {x} \ space M = f -` {x} \ space M \ A" ``` hoelzl@38656 ` 710` ``` by (auto simp: indicator_def split: split_if_asm) ``` hoelzl@47694 ` 711` ``` thus "x * (emeasure M) (?I -` {x} \ space M) = ``` hoelzl@47694 ` 712` ``` x * (emeasure M) (f -` {x} \ space M \ A)" by (cases "x = 0") simp_all ``` hoelzl@38656 ` 713` ``` qed ``` hoelzl@38656 ` 714` ``` show ?thesis unfolding * ``` hoelzl@38656 ` 715` ``` using assms(2) unfolding simple_function_def ``` hoelzl@38656 ` 716` ``` by (auto intro!: setsum_mono_zero_cong_right) ``` hoelzl@38656 ` 717` ```qed ``` hoelzl@35582 ` 718` hoelzl@47694 ` 719` ```lemma simple_integral_indicator_only[simp]: ``` hoelzl@38656 ` 720` ``` assumes "A \ sets M" ``` wenzelm@53015 ` 721` ``` shows "integral\<^sup>S M (indicator A) = emeasure M A" ``` hoelzl@38656 ` 722` ```proof cases ``` immler@50244 ` 723` ``` assume "space M = {}" hence "A = {}" using sets.sets_into_space[OF assms] by auto ``` hoelzl@38656 ` 724` ``` thus ?thesis unfolding simple_integral_def using `space M = {}` by auto ``` hoelzl@38656 ` 725` ```next ``` hoelzl@43920 ` 726` ``` assume "space M \ {}" hence "(\x. 1) ` space M = {1::ereal}" by auto ``` hoelzl@38656 ` 727` ``` thus ?thesis ``` hoelzl@47694 ` 728` ``` using simple_integral_indicator[OF assms simple_function_const[of _ 1]] ``` immler@50244 ` 729` ``` using sets.sets_into_space[OF assms] ``` hoelzl@47694 ` 730` ``` by (auto intro!: arg_cong[where f="(emeasure M)"]) ``` hoelzl@38656 ` 731` ```qed ``` hoelzl@35582 ` 732` hoelzl@47694 ` 733` ```lemma simple_integral_null_set: ``` hoelzl@47694 ` 734` ``` assumes "simple_function M u" "\x. 0 \ u x" and "N \ null_sets M" ``` wenzelm@53015 ` 735` ``` shows "(\\<^sup>Sx. u x * indicator N x \M) = 0" ``` hoelzl@38656 ` 736` ```proof - ``` hoelzl@47694 ` 737` ``` have "AE x in M. indicator N x = (0 :: ereal)" ``` hoelzl@47694 ` 738` ``` using `N \ null_sets M` by (auto simp: indicator_def intro!: AE_I[of _ _ N]) ``` wenzelm@53015 ` 739` ``` then have "(\\<^sup>Sx. u x * indicator N x \M) = (\\<^sup>Sx. 0 \M)" ``` hoelzl@41981 ` 740` ``` using assms apply (intro simple_integral_cong_AE) by auto ``` hoelzl@40859 ` 741` ``` then show ?thesis by simp ``` hoelzl@38656 ` 742` ```qed ``` hoelzl@35582 ` 743` hoelzl@47694 ` 744` ```lemma simple_integral_cong_AE_mult_indicator: ``` hoelzl@47694 ` 745` ``` assumes sf: "simple_function M f" and eq: "AE x in M. x \ S" and "S \ sets M" ``` wenzelm@53015 ` 746` ``` shows "integral\<^sup>S M f = (\\<^sup>Sx. f x * indicator S x \M)" ``` hoelzl@41705 ` 747` ``` using assms by (intro simple_integral_cong_AE) auto ``` hoelzl@35582 ` 748` hoelzl@47694 ` 749` ```lemma simple_integral_cmult_indicator: ``` hoelzl@41981 ` 750` ``` assumes A: "A \ sets M" ``` wenzelm@53015 ` 751` ``` shows "(\\<^sup>Sx. c * indicator A x \M) = c * (emeasure M) A" ``` hoelzl@41981 ` 752` ``` using simple_integral_mult[OF simple_function_indicator[OF A]] ``` hoelzl@41981 ` 753` ``` unfolding simple_integral_indicator_only[OF A] by simp ``` hoelzl@41981 ` 754` hoelzl@47694 ` 755` ```lemma simple_integral_positive: ``` hoelzl@47694 ` 756` ``` assumes f: "simple_function M f" and ae: "AE x in M. 0 \ f x" ``` wenzelm@53015 ` 757` ``` shows "0 \ integral\<^sup>S M f" ``` hoelzl@41981 ` 758` ```proof - ``` wenzelm@53015 ` 759` ``` have "integral\<^sup>S M (\x. 0) \ integral\<^sup>S M f" ``` hoelzl@41981 ` 760` ``` using simple_integral_mono_AE[OF _ f ae] by auto ``` hoelzl@41981 ` 761` ``` then show ?thesis by simp ``` hoelzl@41981 ` 762` ```qed ``` hoelzl@41981 ` 763` hoelzl@41689 ` 764` ```section "Continuous positive integration" ``` hoelzl@41689 ` 765` wenzelm@53015 ` 766` ```definition positive_integral :: "'a measure \ ('a \ ereal) \ ereal" ("integral\<^sup>P") where ``` wenzelm@53015 ` 767` ``` "integral\<^sup>P M f = (SUP g : {g. simple_function M g \ g \ max 0 \ f}. integral\<^sup>S M g)" ``` hoelzl@35692 ` 768` hoelzl@41689 ` 769` ```syntax ``` wenzelm@53015 ` 770` ``` "_positive_integral" :: "pttrn \ ereal \ 'a measure \ ereal" ("\\<^sup>+ _. _ \_" [60,61] 110) ``` hoelzl@41689 ` 771` hoelzl@41689 ` 772` ```translations ``` wenzelm@53015 ` 773` ``` "\\<^sup>+ x. f \M" == "CONST positive_integral M (%x. f)" ``` hoelzl@40872 ` 774` hoelzl@47694 ` 775` ```lemma positive_integral_positive: ``` wenzelm@53015 ` 776` ``` "0 \ integral\<^sup>P M f" ``` hoelzl@44928 ` 777` ``` by (auto intro!: SUP_upper2[of "\x. 0"] simp: positive_integral_def le_fun_def) ``` hoelzl@40873 ` 778` wenzelm@53015 ` 779` ```lemma positive_integral_not_MInfty[simp]: "integral\<^sup>P M f \ -\" ``` hoelzl@47694 ` 780` ``` using positive_integral_positive[of M f] by auto ``` hoelzl@47694 ` 781` hoelzl@47694 ` 782` ```lemma positive_integral_def_finite: ``` wenzelm@53015 ` 783` ``` "integral\<^sup>P M f = (SUP g : {g. simple_function M g \ g \ max 0 \ f \ range g \ {0 ..< \}}. integral\<^sup>S M g)" ``` hoelzl@41981 ` 784` ``` (is "_ = SUPR ?A ?f") ``` hoelzl@41981 ` 785` ``` unfolding positive_integral_def ``` hoelzl@44928 ` 786` ```proof (safe intro!: antisym SUP_least) ``` hoelzl@41981 ` 787` ``` fix g assume g: "simple_function M g" "g \ max 0 \ f" ``` hoelzl@41981 ` 788` ``` let ?G = "{x \ space M. \ g x \ \}" ``` hoelzl@41981 ` 789` ``` note gM = g(1)[THEN borel_measurable_simple_function] ``` wenzelm@50252 ` 790` ``` have \_G_pos: "0 \ (emeasure M) ?G" using gM by auto ``` wenzelm@46731 ` 791` ``` let ?g = "\y x. if g x = \ then y else max 0 (g x)" ``` hoelzl@41981 ` 792` ``` from g gM have g_in_A: "\y. 0 \ y \ y \ \ \ ?g y \ ?A" ``` hoelzl@41981 ` 793` ``` apply (safe intro!: simple_function_max simple_function_If) ``` hoelzl@41981 ` 794` ``` apply (force simp: max_def le_fun_def split: split_if_asm)+ ``` hoelzl@41981 ` 795` ``` done ``` wenzelm@53015 ` 796` ``` show "integral\<^sup>S M g \ SUPR ?A ?f" ``` hoelzl@41981 ` 797` ``` proof cases ``` hoelzl@41981 ` 798` ``` have g0: "?g 0 \ ?A" by (intro g_in_A) auto ``` hoelzl@47694 ` 799` ``` assume "(emeasure M) ?G = 0" ``` hoelzl@47694 ` 800` ``` with gM have "AE x in M. x \ ?G" ``` hoelzl@47694 ` 801` ``` by (auto simp add: AE_iff_null intro!: null_setsI) ``` hoelzl@41981 ` 802` ``` with gM g show ?thesis ``` hoelzl@44928 ` 803` ``` by (intro SUP_upper2[OF g0] simple_integral_mono_AE) ``` hoelzl@41981 ` 804` ``` (auto simp: max_def intro!: simple_function_If) ``` hoelzl@41981 ` 805` ``` next ``` wenzelm@50252 ` 806` ``` assume \_G: "(emeasure M) ?G \ 0" ``` wenzelm@53015 ` 807` ``` have "SUPR ?A (integral\<^sup>S M) = \" ``` hoelzl@41981 ` 808` ``` proof (intro SUP_PInfty) ``` hoelzl@41981 ` 809` ``` fix n :: nat ``` hoelzl@47694 ` 810` ``` let ?y = "ereal (real n) / (if (emeasure M) ?G = \ then 1 else (emeasure M) ?G)" ``` wenzelm@50252 ` 811` ``` have "0 \ ?y" "?y \ \" using \_G \_G_pos by (auto simp: ereal_divide_eq) ``` hoelzl@41981 ` 812` ``` then have "?g ?y \ ?A" by (rule g_in_A) ``` hoelzl@47694 ` 813` ``` have "real n \ ?y * (emeasure M) ?G" ``` wenzelm@50252 ` 814` ``` using \_G \_G_pos by (cases "(emeasure M) ?G") (auto simp: field_simps) ``` wenzelm@53015 ` 815` ``` also have "\ = (\\<^sup>Sx. ?y * indicator ?G x \M)" ``` hoelzl@41981 ` 816` ``` using `0 \ ?y` `?g ?y \ ?A` gM ``` hoelzl@41981 ` 817` ``` by (subst simple_integral_cmult_indicator) auto ``` wenzelm@53015 ` 818` ``` also have "\ \ integral\<^sup>S M (?g ?y)" using `?g ?y \ ?A` gM ``` hoelzl@41981 ` 819` ``` by (intro simple_integral_mono) auto ``` wenzelm@53015 ` 820` ``` finally show "\i\?A. real n \ integral\<^sup>S M i" ``` hoelzl@41981 ` 821` ``` using `?g ?y \ ?A` by blast ``` hoelzl@41981 ` 822` ``` qed ``` hoelzl@41981 ` 823` ``` then show ?thesis by simp ``` hoelzl@41981 ` 824` ``` qed ``` hoelzl@44928 ` 825` ```qed (auto intro: SUP_upper) ``` hoelzl@40873 ` 826` hoelzl@47694 ` 827` ```lemma positive_integral_mono_AE: ``` wenzelm@53015 ` 828` ``` assumes ae: "AE x in M. u x \ v x" shows "integral\<^sup>P M u \ integral\<^sup>P M v" ``` hoelzl@41981 ` 829` ``` unfolding positive_integral_def ``` hoelzl@41981 ` 830` ```proof (safe intro!: SUP_mono) ``` hoelzl@41981 ` 831` ``` fix n assume n: "simple_function M n" "n \ max 0 \ u" ``` hoelzl@41981 ` 832` ``` from ae[THEN AE_E] guess N . note N = this ``` hoelzl@47694 ` 833` ``` then have ae_N: "AE x in M. x \ N" by (auto intro: AE_not_in) ``` wenzelm@46731 ` 834` ``` let ?n = "\x. n x * indicator (space M - N) x" ``` hoelzl@47694 ` 835` ``` have "AE x in M. n x \ ?n x" "simple_function M ?n" ``` hoelzl@41981 ` 836` ``` using n N ae_N by auto ``` hoelzl@41981 ` 837` ``` moreover ``` hoelzl@41981 ` 838` ``` { fix x have "?n x \ max 0 (v x)" ``` hoelzl@41981 ` 839` ``` proof cases ``` hoelzl@41981 ` 840` ``` assume x: "x \ space M - N" ``` hoelzl@41981 ` 841` ``` with N have "u x \ v x" by auto ``` hoelzl@41981 ` 842` ``` with n(2)[THEN le_funD, of x] x show ?thesis ``` hoelzl@41981 ` 843` ``` by (auto simp: max_def split: split_if_asm) ``` hoelzl@41981 ` 844` ``` qed simp } ``` hoelzl@41981 ` 845` ``` then have "?n \ max 0 \ v" by (auto simp: le_funI) ``` wenzelm@53015 ` 846` ``` moreover have "integral\<^sup>S M n \ integral\<^sup>S M ?n" ``` hoelzl@41981 ` 847` ``` using ae_N N n by (auto intro!: simple_integral_mono_AE) ``` wenzelm@53015 ` 848` ``` ultimately show "\m\{g. simple_function M g \ g \ max 0 \ v}. integral\<^sup>S M n \ integral\<^sup>S M m" ``` hoelzl@41981 ` 849` ``` by force ``` hoelzl@38656 ` 850` ```qed ``` hoelzl@38656 ` 851` hoelzl@47694 ` 852` ```lemma positive_integral_mono: ``` wenzelm@53015 ` 853` ``` "(\x. x \ space M \ u x \ v x) \ integral\<^sup>P M u \ integral\<^sup>P M v" ``` hoelzl@41981 ` 854` ``` by (auto intro: positive_integral_mono_AE) ``` hoelzl@40859 ` 855` hoelzl@47694 ` 856` ```lemma positive_integral_cong_AE: ``` wenzelm@53015 ` 857` ``` "AE x in M. u x = v x \ integral\<^sup>P M u = integral\<^sup>P M v" ``` hoelzl@40859 ` 858` ``` by (auto simp: eq_iff intro!: positive_integral_mono_AE) ``` hoelzl@40859 ` 859` hoelzl@47694 ` 860` ```lemma positive_integral_cong: ``` wenzelm@53015 ` 861` ``` "(\x. x \ space M \ u x = v x) \ integral\<^sup>P M u = integral\<^sup>P M v" ``` hoelzl@41981 ` 862` ``` by (auto intro: positive_integral_cong_AE) ``` hoelzl@40859 ` 863` hoelzl@47694 ` 864` ```lemma positive_integral_eq_simple_integral: ``` wenzelm@53015 ` 865` ``` assumes f: "simple_function M f" "\x. 0 \ f x" shows "integral\<^sup>P M f = integral\<^sup>S M f" ``` hoelzl@41981 ` 866` ```proof - ``` wenzelm@46731 ` 867` ``` let ?f = "\x. f x * indicator (space M) x" ``` hoelzl@41981 ` 868` ``` have f': "simple_function M ?f" using f by auto ``` hoelzl@41981 ` 869` ``` with f(2) have [simp]: "max 0 \ ?f = ?f" ``` hoelzl@41981 ` 870` ``` by (auto simp: fun_eq_iff max_def split: split_indicator) ``` wenzelm@53015 ` 871` ``` have "integral\<^sup>P M ?f \ integral\<^sup>S M ?f" using f' ``` hoelzl@44928 ` 872` ``` by (force intro!: SUP_least simple_integral_mono simp: le_fun_def positive_integral_def) ``` wenzelm@53015 ` 873` ``` moreover have "integral\<^sup>S M ?f \ integral\<^sup>P M ?f" ``` hoelzl@41981 ` 874` ``` unfolding positive_integral_def ``` hoelzl@44928 ` 875` ``` using f' by (auto intro!: SUP_upper) ``` hoelzl@41981 ` 876` ``` ultimately show ?thesis ``` hoelzl@41981 ` 877` ``` by (simp cong: positive_integral_cong simple_integral_cong) ``` hoelzl@41981 ` 878` ```qed ``` hoelzl@41981 ` 879` hoelzl@47694 ` 880` ```lemma positive_integral_eq_simple_integral_AE: ``` wenzelm@53015 ` 881` ``` assumes f: "simple_function M f" "AE x in M. 0 \ f x" shows "integral\<^sup>P M f = integral\<^sup>S M f" ``` hoelzl@41981 ` 882` ```proof - ``` hoelzl@47694 ` 883` ``` have "AE x in M. f x = max 0 (f x)" using f by (auto split: split_max) ``` wenzelm@53015 ` 884` ``` with f have "integral\<^sup>P M f = integral\<^sup>S M (\x. max 0 (f x))" ``` hoelzl@41981 ` 885` ``` by (simp cong: positive_integral_cong_AE simple_integral_cong_AE ``` hoelzl@41981 ` 886` ``` add: positive_integral_eq_simple_integral) ``` hoelzl@41981 ` 887` ``` with assms show ?thesis ``` hoelzl@41981 ` 888` ``` by (auto intro!: simple_integral_cong_AE split: split_max) ``` hoelzl@41981 ` 889` ```qed ``` hoelzl@40873 ` 890` hoelzl@47694 ` 891` ```lemma positive_integral_SUP_approx: ``` hoelzl@41981 ` 892` ``` assumes f: "incseq f" "\i. f i \ borel_measurable M" "\i x. 0 \ f i x" ``` hoelzl@41981 ` 893` ``` and u: "simple_function M u" "u \ (SUP i. f i)" "u`space M \ {0..<\}" ``` wenzelm@53015 ` 894` ``` shows "integral\<^sup>S M u \ (SUP i. integral\<^sup>P M (f i))" (is "_ \ ?S") ``` hoelzl@43920 ` 895` ```proof (rule ereal_le_mult_one_interval) ``` wenzelm@53015 ` 896` ``` have "0 \ (SUP i. integral\<^sup>P M (f i))" ``` hoelzl@44928 ` 897` ``` using f(3) by (auto intro!: SUP_upper2 positive_integral_positive) ``` wenzelm@53015 ` 898` ``` then show "(SUP i. integral\<^sup>P M (f i)) \ -\" by auto ``` hoelzl@41981 ` 899` ``` have u_range: "\x. x \ space M \ 0 \ u x \ u x \ \" ``` hoelzl@41981 ` 900` ``` using u(3) by auto ``` hoelzl@43920 ` 901` ``` fix a :: ereal assume "0 < a" "a < 1" ``` hoelzl@38656 ` 902` ``` hence "a \ 0" by auto ``` wenzelm@46731 ` 903` ``` let ?B = "\i. {x \ space M. a * u x \ f i x}" ``` hoelzl@38656 ` 904` ``` have B: "\i. ?B i \ sets M" ``` hoelzl@50003 ` 905` ``` using f `simple_function M u` by auto ``` hoelzl@38656 ` 906` wenzelm@46731 ` 907` ``` let ?uB = "\i x. u x * indicator (?B i) x" ``` hoelzl@38656 ` 908` hoelzl@38656 ` 909` ``` { fix i have "?B i \ ?B (Suc i)" ``` hoelzl@38656 ` 910` ``` proof safe ``` hoelzl@38656 ` 911` ``` fix i x assume "a * u x \ f i x" ``` hoelzl@38656 ` 912` ``` also have "\ \ f (Suc i) x" ``` hoelzl@41981 ` 913` ``` using `incseq f`[THEN incseq_SucD] unfolding le_fun_def by auto ``` hoelzl@38656 ` 914` ``` finally show "a * u x \ f (Suc i) x" . ``` hoelzl@38656 ` 915` ``` qed } ``` hoelzl@38656 ` 916` ``` note B_mono = this ``` hoelzl@35582 ` 917` immler@50244 ` 918` ``` note B_u = sets.Int[OF u(1)[THEN simple_functionD(2)] B] ``` hoelzl@38656 ` 919` wenzelm@46731 ` 920` ``` let ?B' = "\i n. (u -` {i} \ space M) \ ?B n" ``` hoelzl@47694 ` 921` ``` have measure_conv: "\i. (emeasure M) (u -` {i} \ space M) = (SUP n. (emeasure M) (?B' i n))" ``` hoelzl@41981 ` 922` ``` proof - ``` hoelzl@41981 ` 923` ``` fix i ``` hoelzl@41981 ` 924` ``` have 1: "range (?B' i) \ sets M" using B_u by auto ``` hoelzl@41981 ` 925` ``` have 2: "incseq (?B' i)" using B_mono by (auto intro!: incseq_SucI) ``` hoelzl@41981 ` 926` ``` have "(\n. ?B' i n) = u -` {i} \ space M" ``` hoelzl@41981 ` 927` ``` proof safe ``` hoelzl@41981 ` 928` ``` fix x i assume x: "x \ space M" ``` hoelzl@41981 ` 929` ``` show "x \ (\i. ?B' (u x) i)" ``` hoelzl@41981 ` 930` ``` proof cases ``` hoelzl@41981 ` 931` ``` assume "u x = 0" thus ?thesis using `x \ space M` f(3) by simp ``` hoelzl@41981 ` 932` ``` next ``` hoelzl@41981 ` 933` ``` assume "u x \ 0" ``` hoelzl@41981 ` 934` ``` with `a < 1` u_range[OF `x \ space M`] ``` hoelzl@41981 ` 935` ``` have "a * u x < 1 * u x" ``` hoelzl@43920 ` 936` ``` by (intro ereal_mult_strict_right_mono) (auto simp: image_iff) ``` noschinl@46884 ` 937` ``` also have "\ \ (SUP i. f i x)" using u(2) by (auto simp: le_fun_def) ``` hoelzl@44928 ` 938` ``` finally obtain i where "a * u x < f i x" unfolding SUP_def ``` haftmann@56166 ` 939` ``` by (auto simp add: less_SUP_iff) ``` hoelzl@41981 ` 940` ``` hence "a * u x \ f i x" by auto ``` hoelzl@41981 ` 941` ``` thus ?thesis using `x \ space M` by auto ``` hoelzl@41981 ` 942` ``` qed ``` hoelzl@40859 ` 943` ``` qed ``` hoelzl@47694 ` 944` ``` then show "?thesis i" using SUP_emeasure_incseq[OF 1 2] by simp ``` hoelzl@41981 ` 945` ``` qed ``` hoelzl@38656 ` 946` wenzelm@53015 ` 947` ``` have "integral\<^sup>S M u = (SUP i. integral\<^sup>S M (?uB i))" ``` hoelzl@41689 ` 948` ``` unfolding simple_integral_indicator[OF B `simple_function M u`] ``` haftmann@56212 ` 949` ``` proof (subst SUP_ereal_setsum, safe) ``` hoelzl@38656 ` 950` ``` fix x n assume "x \ space M" ``` hoelzl@47694 ` 951` ``` with u_range show "incseq (\i. u x * (emeasure M) (?B' (u x) i))" "\i. 0 \ u x * (emeasure M) (?B' (u x) i)" ``` hoelzl@47694 ` 952` ``` using B_mono B_u by (auto intro!: emeasure_mono ereal_mult_left_mono incseq_SucI simp: ereal_zero_le_0_iff) ``` hoelzl@38656 ` 953` ``` next ``` wenzelm@53015 ` 954` ``` show "integral\<^sup>S M u = (\i\u ` space M. SUP n. i * (emeasure M) (?B' i n))" ``` hoelzl@41981 ` 955` ``` using measure_conv u_range B_u unfolding simple_integral_def ``` haftmann@56212 ` 956` ``` by (auto intro!: setsum_cong SUP_ereal_cmult [symmetric]) ``` hoelzl@38656 ` 957` ``` qed ``` hoelzl@38656 ` 958` ``` moreover ``` wenzelm@53015 ` 959` ``` have "a * (SUP i. integral\<^sup>S M (?uB i)) \ ?S" ``` haftmann@56212 ` 960` ``` apply (subst SUP_ereal_cmult [symmetric]) ``` hoelzl@38705 ` 961` ``` proof (safe intro!: SUP_mono bexI) ``` hoelzl@38656 ` 962` ``` fix i ``` wenzelm@53015 ` 963` ``` have "a * integral\<^sup>S M (?uB i) = (\\<^sup>Sx. a * ?uB i x \M)" ``` hoelzl@41981 ` 964` ``` using B `simple_function M u` u_range ``` hoelzl@41981 ` 965` ``` by (subst simple_integral_mult) (auto split: split_indicator) ``` wenzelm@53015 ` 966` ``` also have "\ \ integral\<^sup>P M (f i)" ``` hoelzl@38656 ` 967` ``` proof - ``` hoelzl@41981 ` 968` ``` have *: "simple_function M (\x. a * ?uB i x)" using B `0 < a` u(1) by auto ``` hoelzl@41981 ` 969` ``` show ?thesis using f(3) * u_range `0 < a` ``` hoelzl@41981 ` 970` ``` by (subst positive_integral_eq_simple_integral[symmetric]) ``` hoelzl@41981 ` 971` ``` (auto intro!: positive_integral_mono split: split_indicator) ``` hoelzl@38656 ` 972` ``` qed ``` wenzelm@53015 ` 973` ``` finally show "a * integral\<^sup>S M (?uB i) \ integral\<^sup>P M (f i)" ``` hoelzl@38656 ` 974` ``` by auto ``` hoelzl@41981 ` 975` ``` next ``` wenzelm@53015 ` 976` ``` fix i show "0 \ \\<^sup>S x. ?uB i x \M" using B `0 < a` u(1) u_range ``` hoelzl@41981 ` 977` ``` by (intro simple_integral_positive) (auto split: split_indicator) ``` hoelzl@41981 ` 978` ``` qed (insert `0 < a`, auto) ``` wenzelm@53015 ` 979` ``` ultimately show "a * integral\<^sup>S M u \ ?S" by simp ``` hoelzl@35582 ` 980` ```qed ``` hoelzl@35582 ` 981` hoelzl@47694 ` 982` ```lemma incseq_positive_integral: ``` wenzelm@53015 ` 983` ``` assumes "incseq f" shows "incseq (\i. integral\<^sup>P M (f i))" ``` hoelzl@41981 ` 984` ```proof - ``` hoelzl@41981 ` 985` ``` have "\i x. f i x \ f (Suc i) x" ``` hoelzl@41981 ` 986` ``` using assms by (auto dest!: incseq_SucD simp: le_fun_def) ``` hoelzl@41981 ` 987` ``` then show ?thesis ``` hoelzl@41981 ` 988` ``` by (auto intro!: incseq_SucI positive_integral_mono) ``` hoelzl@41981 ` 989` ```qed ``` hoelzl@41981 ` 990` hoelzl@35582 ` 991` ```text {* Beppo-Levi monotone convergence theorem *} ``` hoelzl@47694 ` 992` ```lemma positive_integral_monotone_convergence_SUP: ``` hoelzl@41981 ` 993` ``` assumes f: "incseq f" "\i. f i \ borel_measurable M" "\i x. 0 \ f i x" ``` wenzelm@53015 ` 994` ``` shows "(\\<^sup>+ x. (SUP i. f i x) \M) = (SUP i. integral\<^sup>P M (f i))" ``` hoelzl@41981 ` 995` ```proof (rule antisym) ``` wenzelm@53015 ` 996` ``` show "(SUP j. integral\<^sup>P M (f j)) \ (\\<^sup>+ x. (SUP i. f i x) \M)" ``` hoelzl@44928 ` 997` ``` by (auto intro!: SUP_least SUP_upper positive_integral_mono) ``` hoelzl@38656 ` 998` ```next ``` wenzelm@53015 ` 999` ``` show "(\\<^sup>+ x. (SUP i. f i x) \M) \ (SUP j. integral\<^sup>P M (f j))" ``` hoelzl@47694 ` 1000` ``` unfolding positive_integral_def_finite[of _ "\x. SUP i. f i x"] ``` hoelzl@44928 ` 1001` ``` proof (safe intro!: SUP_least) ``` hoelzl@41981 ` 1002` ``` fix g assume g: "simple_function M g" ``` wenzelm@53374 ` 1003` ``` and *: "g \ max 0 \ (\x. SUP i. f i x)" "range g \ {0..<\}" ``` wenzelm@53374 ` 1004` ``` then have "\x. 0 \ (SUP i. f i x)" and g': "g`space M \ {0..<\}" ``` hoelzl@44928 ` 1005` ``` using f by (auto intro!: SUP_upper2) ``` wenzelm@53374 ` 1006` ``` with * show "integral\<^sup>S M g \ (SUP j. integral\<^sup>P M (f j))" ``` hoelzl@41981 ` 1007` ``` by (intro positive_integral_SUP_approx[OF f g _ g']) ``` noschinl@46884 ` 1008` ``` (auto simp: le_fun_def max_def) ``` hoelzl@35582 ` 1009` ``` qed ``` hoelzl@35582 ` 1010` ```qed ``` hoelzl@35582 ` 1011` hoelzl@47694 ` 1012` ```lemma positive_integral_monotone_convergence_SUP_AE: ``` hoelzl@47694 ` 1013` ``` assumes f: "\i. AE x in M. f i x \ f (Suc i) x \ 0 \ f i x" "\i. f i \ borel_measurable M" ``` wenzelm@53015 ` 1014` ``` shows "(\\<^sup>+ x. (SUP i. f i x) \M) = (SUP i. integral\<^sup>P M (f i))" ``` hoelzl@40859 ` 1015` ```proof - ``` hoelzl@47694 ` 1016` ``` from f have "AE x in M. \i. f i x \ f (Suc i) x \ 0 \ f i x" ``` hoelzl@41981 ` 1017` ``` by (simp add: AE_all_countable) ``` hoelzl@41981 ` 1018` ``` from this[THEN AE_E] guess N . note N = this ``` wenzelm@46731 ` 1019` ``` let ?f = "\i x. if x \ space M - N then f i x else 0" ``` hoelzl@47694 ` 1020` ``` have f_eq: "AE x in M. \i. ?f i x = f i x" using N by (auto intro!: AE_I[of _ _ N]) ``` wenzelm@53015 ` 1021` ``` then have "(\\<^sup>+ x. (SUP i. f i x) \M) = (\\<^sup>+ x. (SUP i. ?f i x) \M)" ``` hoelzl@41981 ` 1022` ``` by (auto intro!: positive_integral_cong_AE) ``` wenzelm@53015 ` 1023` ``` also have "\ = (SUP i. (\\<^sup>+ x. ?f i x \M))" ``` hoelzl@41981 ` 1024` ``` proof (rule positive_integral_monotone_convergence_SUP) ``` hoelzl@41981 ` 1025` ``` show "incseq ?f" using N(1) by (force intro!: incseq_SucI le_funI) ``` hoelzl@41981 ` 1026` ``` { fix i show "(\x. if x \ space M - N then f i x else 0) \ borel_measurable M" ``` hoelzl@41981 ` 1027` ``` using f N(3) by (intro measurable_If_set) auto ``` hoelzl@41981 ` 1028` ``` fix x show "0 \ ?f i x" ``` hoelzl@41981 ` 1029` ``` using N(1) by auto } ``` hoelzl@40859 ` 1030` ``` qed ``` wenzelm@53015 ` 1031` ``` also have "\ = (SUP i. (\\<^sup>+ x. f i x \M))" ``` hoelzl@41981 ` 1032` ``` using f_eq by (force intro!: arg_cong[where f="SUPR UNIV"] positive_integral_cong_AE ext) ``` hoelzl@41981 ` 1033` ``` finally show ?thesis . ``` hoelzl@41981 ` 1034` ```qed ``` hoelzl@41981 ` 1035` hoelzl@47694 ` 1036` ```lemma positive_integral_monotone_convergence_SUP_AE_incseq: ``` hoelzl@47694 ` 1037` ``` assumes f: "incseq f" "\i. AE x in M. 0 \ f i x" and borel: "\i. f i \ borel_measurable M" ``` wenzelm@53015 ` 1038` ``` shows "(\\<^sup>+ x. (SUP i. f i x) \M) = (SUP i. integral\<^sup>P M (f i))" ``` hoelzl@41981 ` 1039` ``` using f[unfolded incseq_Suc_iff le_fun_def] ``` hoelzl@41981 ` 1040` ``` by (intro positive_integral_monotone_convergence_SUP_AE[OF _ borel]) ``` hoelzl@41981 ` 1041` ``` auto ``` hoelzl@41981 ` 1042` hoelzl@47694 ` 1043` ```lemma positive_integral_monotone_convergence_simple: ``` hoelzl@41981 ` 1044` ``` assumes f: "incseq f" "\i x. 0 \ f i x" "\i. simple_function M (f i)" ``` wenzelm@53015 ` 1045` ``` shows "(SUP i. integral\<^sup>S M (f i)) = (\\<^sup>+x. (SUP i. f i x) \M)" ``` hoelzl@41981 ` 1046` ``` using assms unfolding positive_integral_monotone_convergence_SUP[OF f(1) ``` hoelzl@41981 ` 1047` ``` f(3)[THEN borel_measurable_simple_function] f(2)] ``` hoelzl@41981 ` 1048` ``` by (auto intro!: positive_integral_eq_simple_integral[symmetric] arg_cong[where f="SUPR UNIV"] ext) ``` hoelzl@41981 ` 1049` hoelzl@41981 ` 1050` ```lemma positive_integral_max_0: ``` wenzelm@53015 ` 1051` ``` "(\\<^sup>+x. max 0 (f x) \M) = integral\<^sup>P M f" ``` hoelzl@41981 ` 1052` ``` by (simp add: le_fun_def positive_integral_def) ``` hoelzl@41981 ` 1053` hoelzl@47694 ` 1054` ```lemma positive_integral_cong_pos: ``` hoelzl@41981 ` 1055` ``` assumes "\x. x \ space M \ f x \ 0 \ g x \ 0 \ f x = g x" ``` wenzelm@53015 ` 1056` ``` shows "integral\<^sup>P M f = integral\<^sup>P M g" ``` hoelzl@41981 ` 1057` ```proof - ``` wenzelm@53015 ` 1058` ``` have "integral\<^sup>P M (\x. max 0 (f x)) = integral\<^sup>P M (\x. max 0 (g x))" ``` hoelzl@41981 ` 1059` ``` proof (intro positive_integral_cong) ``` hoelzl@41981 ` 1060` ``` fix x assume "x \ space M" ``` hoelzl@41981 ` 1061` ``` from assms[OF this] show "max 0 (f x) = max 0 (g x)" ``` hoelzl@41981 ` 1062` ``` by (auto split: split_max) ``` hoelzl@41981 ` 1063` ``` qed ``` hoelzl@41981 ` 1064` ``` then show ?thesis by (simp add: positive_integral_max_0) ``` hoelzl@40859 ` 1065` ```qed ``` hoelzl@40859 ` 1066` hoelzl@47694 ` 1067` ```lemma SUP_simple_integral_sequences: ``` hoelzl@41981 ` 1068` ``` assumes f: "incseq f" "\i x. 0 \ f i x" "\i. simple_function M (f i)" ``` hoelzl@41981 ` 1069` ``` and g: "incseq g" "\i x. 0 \ g i x" "\i. simple_function M (g i)" ``` hoelzl@47694 ` 1070` ``` and eq: "AE x in M. (SUP i. f i x) = (SUP i. g i x)" ``` wenzelm@53015 ` 1071` ``` shows "(SUP i. integral\<^sup>S M (f i)) = (SUP i. integral\<^sup>S M (g i))" ``` hoelzl@38656 ` 1072` ``` (is "SUPR _ ?F = SUPR _ ?G") ``` hoelzl@38656 ` 1073` ```proof - ``` wenzelm@53015 ` 1074` ``` have "(SUP i. integral\<^sup>S M (f i)) = (\\<^sup>+x. (SUP i. f i x) \M)" ``` hoelzl@41981 ` 1075` ``` using f by (rule positive_integral_monotone_convergence_simple) ``` wenzelm@53015 ` 1076` ``` also have "\ = (\\<^sup>+x. (SUP i. g i x) \M)" ``` hoelzl@41981 ` 1077` ``` unfolding eq[THEN positive_integral_cong_AE] .. ``` hoelzl@38656 ` 1078` ``` also have "\ = (SUP i. ?G i)" ``` hoelzl@41981 ` 1079` ``` using g by (rule positive_integral_monotone_convergence_simple[symmetric]) ``` hoelzl@41981 ` 1080` ``` finally show ?thesis by simp ``` hoelzl@38656 ` 1081` ```qed ``` hoelzl@38656 ` 1082` hoelzl@47694 ` 1083` ```lemma positive_integral_const[simp]: ``` wenzelm@53015 ` 1084` ``` "0 \ c \ (\\<^sup>+ x. c \M) = c * (emeasure M) (space M)" ``` hoelzl@38656 ` 1085` ``` by (subst positive_integral_eq_simple_integral) auto ``` hoelzl@38656 ` 1086` hoelzl@47694 ` 1087` ```lemma positive_integral_linear: ``` hoelzl@41981 ` 1088` ``` assumes f: "f \ borel_measurable M" "\x. 0 \ f x" and "0 \ a" ``` hoelzl@41981 ` 1089` ``` and g: "g \ borel_measurable M" "\x. 0 \ g x" ``` wenzelm@53015 ` 1090` ``` shows "(\\<^sup>+ x. a * f x + g x \M) = a * integral\<^sup>P M f + integral\<^sup>P M g" ``` wenzelm@53015 ` 1091` ``` (is "integral\<^sup>P M ?L = _") ``` hoelzl@35582 ` 1092` ```proof - ``` hoelzl@41981 ` 1093` ``` from borel_measurable_implies_simple_function_sequence'[OF f(1)] guess u . ``` hoelzl@41981 ` 1094` ``` note u = positive_integral_monotone_convergence_simple[OF this(2,5,1)] this ``` hoelzl@41981 ` 1095` ``` from borel_measurable_implies_simple_function_sequence'[OF g(1)] guess v . ``` hoelzl@41981 ` 1096` ``` note v = positive_integral_monotone_convergence_simple[OF this(2,5,1)] this ``` wenzelm@46731 ` 1097` ``` let ?L' = "\i x. a * u i x + v i x" ``` hoelzl@38656 ` 1098` hoelzl@41981 ` 1099` ``` have "?L \ borel_measurable M" using assms by auto ``` hoelzl@38656 ` 1100` ``` from borel_measurable_implies_simple_function_sequence'[OF this] guess l . ``` hoelzl@41981 ` 1101` ``` note l = positive_integral_monotone_convergence_simple[OF this(2,5,1)] this ``` hoelzl@41981 ` 1102` wenzelm@53015 ` 1103` ``` have inc: "incseq (\i. a * integral\<^sup>S M (u i))" "incseq (\i. integral\<^sup>S M (v i))" ``` hoelzl@41981 ` 1104` ``` using u v `0 \ a` ``` hoelzl@41981 ` 1105` ``` by (auto simp: incseq_Suc_iff le_fun_def ``` hoelzl@43920 ` 1106` ``` intro!: add_mono ereal_mult_left_mono simple_integral_mono) ``` wenzelm@53015 ` 1107` ``` have pos: "\i. 0 \ integral\<^sup>S M (u i)" "\i. 0 \ integral\<^sup>S M (v i)" "\i. 0 \ a * integral\<^sup>S M (u i)" ``` hoelzl@41981 ` 1108` ``` using u v `0 \ a` by (auto simp: simple_integral_positive) ``` wenzelm@53015 ` 1109` ``` { fix i from pos[of i] have "a * integral\<^sup>S M (u i) \ -\" "integral\<^sup>S M (v i) \ -\" ``` hoelzl@41981 ` 1110` ``` by (auto split: split_if_asm) } ``` hoelzl@41981 ` 1111` ``` note not_MInf = this ``` hoelzl@41981 ` 1112` wenzelm@53015 ` 1113` ``` have l': "(SUP i. integral\<^sup>S M (l i)) = (SUP i. integral\<^sup>S M (?L' i))" ``` hoelzl@41981 ` 1114` ``` proof (rule SUP_simple_integral_sequences[OF l(3,6,2)]) ``` hoelzl@41981 ` 1115` ``` show "incseq ?L'" "\i x. 0 \ ?L' i x" "\i. simple_function M (?L' i)" ``` hoelzl@41981 ` 1116` ``` using u v `0 \ a` unfolding incseq_Suc_iff le_fun_def ``` hoelzl@43920 ` 1117` ``` by (auto intro!: add_mono ereal_mult_left_mono ereal_add_nonneg_nonneg) ``` hoelzl@41981 ` 1118` ``` { fix x ``` hoelzl@41981 ` 1119` ``` { fix i have "a * u i x \ -\" "v i x \ -\" "u i x \ -\" using `0 \ a` u(6)[of i x] v(6)[of i x] ``` hoelzl@41981 ` 1120` ``` by auto } ``` hoelzl@41981 ` 1121` ``` then have "(SUP i. a * u i x + v i x) = a * (SUP i. u i x) + (SUP i. v i x)" ``` hoelzl@41981 ` 1122` ``` using `0 \ a` u(3) v(3) u(6)[of _ x] v(6)[of _ x] ``` haftmann@56212 ` 1123` ``` by (subst SUP_ereal_cmult [symmetric, OF u(6) `0 \ a`]) ``` haftmann@56212 ` 1124` ``` (auto intro!: SUP_ereal_add ``` hoelzl@43920 ` 1125` ``` simp: incseq_Suc_iff le_fun_def add_mono ereal_mult_left_mono ereal_add_nonneg_nonneg) } ``` hoelzl@47694 ` 1126` ``` then show "AE x in M. (SUP i. l i x) = (SUP i. ?L' i x)" ``` hoelzl@41981 ` 1127` ``` unfolding l(5) using `0 \ a` u(5) v(5) l(5) f(2) g(2) ``` hoelzl@43920 ` 1128` ``` by (intro AE_I2) (auto split: split_max simp add: ereal_add_nonneg_nonneg) ``` hoelzl@38656 ` 1129` ``` qed ``` wenzelm@53015 ` 1130` ``` also have "\ = (SUP i. a * integral\<^sup>S M (u i) + integral\<^sup>S M (v i))" ``` hoelzl@41981 ` 1131` ``` using u(2, 6) v(2, 6) `0 \ a` by (auto intro!: arg_cong[where f="SUPR UNIV"] ext) ``` wenzelm@53015 ` 1132` ``` finally have "(\\<^sup>+ x. max 0 (a * f x + g x) \M) = a * (\\<^sup>+x. max 0 (f x) \M) + (\\<^sup>+x. max 0 (g x) \M)" ``` hoelzl@41981 ` 1133` ``` unfolding l(5)[symmetric] u(5)[symmetric] v(5)[symmetric] ``` hoelzl@41981 ` 1134` ``` unfolding l(1)[symmetric] u(1)[symmetric] v(1)[symmetric] ``` haftmann@56212 ` 1135` ``` apply (subst SUP_ereal_cmult [symmetric, OF pos(1) `0 \ a`]) ``` haftmann@56212 ` 1136` ``` apply (subst SUP_ereal_add [symmetric, OF inc not_MInf]) . ``` hoelzl@41981 ` 1137` ``` then show ?thesis by (simp add: positive_integral_max_0) ``` hoelzl@38656 ` 1138` ```qed ``` hoelzl@38656 ` 1139` hoelzl@47694 ` 1140` ```lemma positive_integral_cmult: ``` hoelzl@49775 ` 1141` ``` assumes f: "f \ borel_measurable M" "0 \ c" ``` wenzelm@53015 ` 1142` ``` shows "(\\<^sup>+ x. c * f x \M) = c * integral\<^sup>P M f" ``` hoelzl@41981 ` 1143` ```proof - ``` hoelzl@41981 ` 1144` ``` have [simp]: "\x. c * max 0 (f x) = max 0 (c * f x)" using `0 \ c` ``` hoelzl@43920 ` 1145` ``` by (auto split: split_max simp: ereal_zero_le_0_iff) ``` wenzelm@53015 ` 1146` ``` have "(\\<^sup>+ x. c * f x \M) = (\\<^sup>+ x. c * max 0 (f x) \M)" ``` hoelzl@41981 ` 1147` ``` by (simp add: positive_integral_max_0) ``` hoelzl@41981 ` 1148` ``` then show ?thesis ``` hoelzl@47694 ` 1149` ``` using positive_integral_linear[OF _ _ `0 \ c`, of "\x. max 0 (f x)" _ "\x. 0"] f ``` hoelzl@41981 ` 1150` ``` by (auto simp: positive_integral_max_0) ``` hoelzl@41981 ` 1151` ```qed ``` hoelzl@38656 ` 1152` hoelzl@47694 ` 1153` ```lemma positive_integral_multc: ``` hoelzl@49775 ` 1154` ``` assumes "f \ borel_measurable M" "0 \ c" ``` wenzelm@53015 ` 1155` ``` shows "(\\<^sup>+ x. f x * c \M) = integral\<^sup>P M f * c" ``` hoelzl@41096 ` 1156` ``` unfolding mult_commute[of _ c] positive_integral_cmult[OF assms] by simp ``` hoelzl@41096 ` 1157` hoelzl@47694 ` 1158` ```lemma positive_integral_indicator[simp]: ``` wenzelm@53015 ` 1159` ``` "A \ sets M \ (\\<^sup>+ x. indicator A x\M) = (emeasure M) A" ``` hoelzl@41544 ` 1160` ``` by (subst positive_integral_eq_simple_integral) ``` hoelzl@49775 ` 1161` ``` (auto simp: simple_integral_indicator) ``` hoelzl@38656 ` 1162` hoelzl@47694 ` 1163` ```lemma positive_integral_cmult_indicator: ``` wenzelm@53015 ` 1164` ``` "0 \ c \ A \ sets M \ (\\<^sup>+ x. c * indicator A x \M) = c * (emeasure M) A" ``` hoelzl@41544 ` 1165` ``` by (subst positive_integral_eq_simple_integral) ``` hoelzl@41544 ` 1166` ``` (auto simp: simple_function_indicator simple_integral_indicator) ``` hoelzl@38656 ` 1167` hoelzl@50097 ` 1168` ```lemma positive_integral_indicator': ``` hoelzl@50097 ` 1169` ``` assumes [measurable]: "A \ space M \ sets M" ``` wenzelm@53015 ` 1170` ``` shows "(\\<^sup>+ x. indicator A x \M) = emeasure M (A \ space M)" ``` hoelzl@50097 ` 1171` ```proof - ``` wenzelm@53015 ` 1172` ``` have "(\\<^sup>+ x. indicator A x \M) = (\\<^sup>+ x. indicator (A \ space M) x \M)" ``` hoelzl@50097 ` 1173` ``` by (intro positive_integral_cong) (simp split: split_indicator) ``` hoelzl@50097 ` 1174` ``` also have "\ = emeasure M (A \ space M)" ``` hoelzl@50097 ` 1175` ``` by simp ``` hoelzl@50097 ` 1176` ``` finally show ?thesis . ``` hoelzl@50097 ` 1177` ```qed ``` hoelzl@50097 ` 1178` hoelzl@47694 ` 1179` ```lemma positive_integral_add: ``` hoelzl@47694 ` 1180` ``` assumes f: "f \ borel_measurable M" "AE x in M. 0 \ f x" ``` hoelzl@47694 ` 1181` ``` and g: "g \ borel_measurable M" "AE x in M. 0 \ g x" ``` wenzelm@53015 ` 1182` ``` shows "(\\<^sup>+ x. f x + g x \M) = integral\<^sup>P M f + integral\<^sup>P M g" ``` hoelzl@41981 ` 1183` ```proof - ``` hoelzl@47694 ` 1184` ``` have ae: "AE x in M. max 0 (f x) + max 0 (g x) = max 0 (f x + g x)" ``` hoelzl@43920 ` 1185` ``` using assms by (auto split: split_max simp: ereal_add_nonneg_nonneg) ``` wenzelm@53015 ` 1186` ``` have "(\\<^sup>+ x. f x + g x \M) = (\\<^sup>+ x. max 0 (f x + g x) \M)" ``` hoelzl@41981 ` 1187` ``` by (simp add: positive_integral_max_0) ``` wenzelm@53015 ` 1188` ``` also have "\ = (\\<^sup>+ x. max 0 (f x) + max 0 (g x) \M)" ``` hoelzl@41981 ` 1189` ``` unfolding ae[THEN positive_integral_cong_AE] .. ``` wenzelm@53015 ` 1190` ``` also have "\ = (\\<^sup>+ x. max 0 (f x) \M) + (\\<^sup>+ x. max 0 (g x) \M)" ``` hoelzl@47694 ` 1191` ``` using positive_integral_linear[of "\x. max 0 (f x)" _ 1 "\x. max 0 (g x)"] f g ``` hoelzl@41981 ` 1192` ``` by auto ``` hoelzl@41981 ` 1193` ``` finally show ?thesis ``` hoelzl@41981 ` 1194` ``` by (simp add: positive_integral_max_0) ``` hoelzl@41981 ` 1195` ```qed ``` hoelzl@38656 ` 1196` hoelzl@47694 ` 1197` ```lemma positive_integral_setsum: ``` hoelzl@47694 ` 1198` ``` assumes "\i. i\P \ f i \ borel_measurable M" "\i. i\P \ AE x in M. 0 \ f i x" ``` wenzelm@53015 ` 1199` ``` shows "(\\<^sup>+ x. (\i\P. f i x) \M) = (\i\P. integral\<^sup>P M (f i))" ``` hoelzl@38656 ` 1200` ```proof cases ``` hoelzl@41981 ` 1201` ``` assume f: "finite P" ``` hoelzl@47694 ` 1202` ``` from assms have "AE x in M. \i\P. 0 \ f i x" unfolding AE_finite_all[OF f] by auto ``` hoelzl@41981 ` 1203` ``` from f this assms(1) show ?thesis ``` hoelzl@38656 ` 1204` ``` proof induct ``` hoelzl@38656 ` 1205` ``` case (insert i P) ``` hoelzl@47694 ` 1206` ``` then have "f i \ borel_measurable M" "AE x in M. 0 \ f i x" ``` hoelzl@47694 ` 1207` ``` "(\x. \i\P. f i x) \ borel_measurable M" "AE x in M. 0 \ (\i\P. f i x)" ``` hoelzl@50002 ` 1208` ``` by (auto intro!: setsum_nonneg) ``` hoelzl@38656 ` 1209` ``` from positive_integral_add[OF this] ``` hoelzl@38656 ` 1210` ``` show ?case using insert by auto ``` hoelzl@38656 ` 1211` ``` qed simp ``` hoelzl@38656 ` 1212` ```qed simp ``` hoelzl@38656 ` 1213` hoelzl@47694 ` 1214` ```lemma positive_integral_Markov_inequality: ``` hoelzl@49775 ` 1215` ``` assumes u: "u \ borel_measurable M" "AE x in M. 0 \ u x" and "A \ sets M" and c: "0 \ c" ``` wenzelm@53015 ` 1216` ``` shows "(emeasure M) ({x\space M. 1 \ c * u x} \ A) \ c * (\\<^sup>+ x. u x * indicator A x \M)" ``` hoelzl@47694 ` 1217` ``` (is "(emeasure M) ?A \ _ * ?PI") ``` hoelzl@41981 ` 1218` ```proof - ``` hoelzl@41981 ` 1219` ``` have "?A \ sets M" ``` hoelzl@41981 ` 1220` ``` using `A \ sets M` u by auto ``` wenzelm@53015 ` 1221` ``` hence "(emeasure M) ?A = (\\<^sup>+ x. indicator ?A x \M)" ``` hoelzl@41981 ` 1222` ``` using positive_integral_indicator by simp ``` wenzelm@53015 ` 1223` ``` also have "\ \ (\\<^sup>+ x. c * (u x * indicator A x) \M)" using u c ``` hoelzl@41981 ` 1224` ``` by (auto intro!: positive_integral_mono_AE ``` hoelzl@43920 ` 1225` ``` simp: indicator_def ereal_zero_le_0_iff) ``` wenzelm@53015 ` 1226` ``` also have "\ = c * (\\<^sup>+ x. u x * indicator A x \M)" ``` hoelzl@41981 ` 1227` ``` using assms ``` hoelzl@50002 ` 1228` ``` by (auto intro!: positive_integral_cmult simp: ereal_zero_le_0_iff) ``` hoelzl@41981 ` 1229` ``` finally show ?thesis . ``` hoelzl@41981 ` 1230` ```qed ``` hoelzl@41981 ` 1231` hoelzl@47694 ` 1232` ```lemma positive_integral_noteq_infinite: ``` hoelzl@47694 ` 1233` ``` assumes g: "g \ borel_measurable M" "AE x in M. 0 \ g x" ``` wenzelm@53015 ` 1234` ``` and "integral\<^sup>P M g \ \" ``` hoelzl@47694 ` 1235` ``` shows "AE x in M. g x \ \" ``` hoelzl@41981 ` 1236` ```proof (rule ccontr) ``` hoelzl@47694 ` 1237` ``` assume c: "\ (AE x in M. g x \ \)" ``` hoelzl@47694 ` 1238` ``` have "(emeasure M) {x\space M. g x = \} \ 0" ``` hoelzl@47694 ` 1239` ``` using c g by (auto simp add: AE_iff_null) ``` hoelzl@47694 ` 1240` ``` moreover have "0 \ (emeasure M) {x\space M. g x = \}" using g by (auto intro: measurable_sets) ``` hoelzl@47694 ` 1241` ``` ultimately have "0 < (emeasure M) {x\space M. g x = \}" by auto ``` hoelzl@47694 ` 1242` ``` then have "\ = \ * (emeasure M) {x\space M. g x = \}" by auto ``` wenzelm@53015 ` 1243` ``` also have "\ \ (\\<^sup>+x. \ * indicator {x\space M. g x = \} x \M)" ``` hoelzl@41981 ` 1244` ``` using g by (subst positive_integral_cmult_indicator) auto ``` wenzelm@53015 ` 1245` ``` also have "\ \ integral\<^sup>P M g" ``` hoelzl@41981 ` 1246` ``` using assms by (auto intro!: positive_integral_mono_AE simp: indicator_def) ``` wenzelm@53015 ` 1247` ``` finally show False using `integral\<^sup>P M g \ \` by auto ``` hoelzl@41981 ` 1248` ```qed ``` hoelzl@41981 ` 1249` hoelzl@47694 ` 1250` ```lemma positive_integral_diff: ``` hoelzl@41981 ` 1251` ``` assumes f: "f \ borel_measurable M" ``` hoelzl@47694 ` 1252` ``` and g: "g \ borel_measurable M" "AE x in M. 0 \ g x" ``` wenzelm@53015 ` 1253` ``` and fin: "integral\<^sup>P M g \ \" ``` hoelzl@47694 ` 1254` ``` and mono: "AE x in M. g x \ f x" ``` wenzelm@53015 ` 1255` ``` shows "(\\<^sup>+ x. f x - g x \M) = integral\<^sup>P M f - integral\<^sup>P M g" ``` hoelzl@38656 ` 1256` ```proof - ``` hoelzl@47694 ` 1257` ``` have diff: "(\x. f x - g x) \ borel_measurable M" "AE x in M. 0 \ f x - g x" ``` hoelzl@43920 ` 1258` ``` using assms by (auto intro: ereal_diff_positive) ``` hoelzl@47694 ` 1259` ``` have pos_f: "AE x in M. 0 \ f x" using mono g by auto ``` hoelzl@43920 ` 1260` ``` { fix a b :: ereal assume "0 \ a" "a \ \" "0 \ b" "a \ b" then have "b - a + a = b" ``` hoelzl@43920 ` 1261` ``` by (cases rule: ereal2_cases[of a b]) auto } ``` hoelzl@41981 ` 1262` ``` note * = this ``` hoelzl@47694 ` 1263` ``` then have "AE x in M. f x = f x - g x + g x" ``` hoelzl@41981 ` 1264` ``` using mono positive_integral_noteq_infinite[OF g fin] assms by auto ``` wenzelm@53015 ` 1265` ``` then have **: "integral\<^sup>P M f = (\\<^sup>+x. f x - g x \M) + integral\<^sup>P M g" ``` hoelzl@41981 ` 1266` ``` unfolding positive_integral_add[OF diff g, symmetric] ``` hoelzl@41981 ` 1267` ``` by (rule positive_integral_cong_AE) ``` hoelzl@41981 ` 1268` ``` show ?thesis unfolding ** ``` hoelzl@47694 ` 1269` ``` using fin positive_integral_positive[of M g] ``` wenzelm@53015 ` 1270` ``` by (cases rule: ereal2_cases[of "\\<^sup>+ x. f x - g x \M" "integral\<^sup>P M g"]) auto ``` hoelzl@38656 ` 1271` ```qed ``` hoelzl@38656 ` 1272` hoelzl@47694 ` 1273` ```lemma positive_integral_suminf: ``` hoelzl@47694 ` 1274` ``` assumes f: "\i. f i \ borel_measurable M" "\i. AE x in M. 0 \ f i x" ``` wenzelm@53015 ` 1275` ``` shows "(\\<^sup>+ x. (\i. f i x) \M) = (\i. integral\<^sup>P M (f i))" ``` hoelzl@38656 ` 1276` ```proof - ``` hoelzl@47694 ` 1277` ``` have all_pos: "AE x in M. \i. 0 \ f i x" ``` hoelzl@41981 ` 1278` ``` using assms by (auto simp: AE_all_countable) ``` wenzelm@53015 ` 1279` ``` have "(\i. integral\<^sup>P M (f i)) = (SUP n. \iP M (f i))" ``` haftmann@56212 ` 1280` ``` using positive_integral_positive by (rule suminf_ereal_eq_SUP) ``` wenzelm@53015 ` 1281` ``` also have "\ = (SUP n. \\<^sup>+x. (\iM)" ``` hoelzl@41981 ` 1282` ``` unfolding positive_integral_setsum[OF f] .. ``` wenzelm@53015 ` 1283` ``` also have "\ = \\<^sup>+x. (SUP n. \iM" using f all_pos ``` hoelzl@41981 ` 1284` ``` by (intro positive_integral_monotone_convergence_SUP_AE[symmetric]) ``` hoelzl@41981 ` 1285` ``` (elim AE_mp, auto simp: setsum_nonneg simp del: setsum_lessThan_Suc intro!: AE_I2 setsum_mono3) ``` wenzelm@53015 ` 1286` ``` also have "\ = \\<^sup>+x. (\i. f i x) \M" using all_pos ``` haftmann@56212 ` 1287` ``` by (intro positive_integral_cong_AE) (auto simp: suminf_ereal_eq_SUP) ``` hoelzl@41981 ` 1288` ``` finally show ?thesis by simp ``` hoelzl@38656 ` 1289` ```qed ``` hoelzl@38656 ` 1290` hoelzl@38656 ` 1291` ```text {* Fatou's lemma: convergence theorem on limes inferior *} ``` hoelzl@47694 ` 1292` ```lemma positive_integral_lim_INF: ``` hoelzl@43920 ` 1293` ``` fixes u :: "nat \ 'a \ ereal" ``` hoelzl@47694 ` 1294` ``` assumes u: "\i. u i \ borel_measurable M" "\i. AE x in M. 0 \ u i x" ``` wenzelm@53015 ` 1295` ``` shows "(\\<^sup>+ x. liminf (\n. u n x) \M) \ liminf (\n. integral\<^sup>P M (u n))" ``` hoelzl@38656 ` 1296` ```proof - ``` hoelzl@47694 ` 1297` ``` have pos: "AE x in M. \i. 0 \ u i x" using u by (auto simp: AE_all_countable) ``` wenzelm@53015 ` 1298` ``` have "(\\<^sup>+ x. liminf (\n. u n x) \M) = ``` wenzelm@53015 ` 1299` ``` (SUP n. \\<^sup>+ x. (INF i:{n..}. u i x) \M)" ``` haftmann@56212 ` 1300` ``` unfolding liminf_SUP_INF using pos u ``` hoelzl@41981 ` 1301` ``` by (intro positive_integral_monotone_convergence_SUP_AE) ``` hoelzl@44937 ` 1302` ``` (elim AE_mp, auto intro!: AE_I2 intro: INF_greatest INF_superset_mono) ``` wenzelm@53015 ` 1303` ``` also have "\ \ liminf (\n. integral\<^sup>P M (u n))" ``` haftmann@56212 ` 1304` ``` unfolding liminf_SUP_INF ``` hoelzl@44928 ` 1305` ``` by (auto intro!: SUP_mono exI INF_greatest positive_integral_mono INF_lower) ``` hoelzl@38656 ` 1306` ``` finally show ?thesis . ``` hoelzl@35582 ` 1307` ```qed ``` hoelzl@35582 ` 1308` hoelzl@47694 ` 1309` ```lemma positive_integral_null_set: ``` wenzelm@53015 ` 1310` ``` assumes "N \ null_sets M" shows "(\\<^sup>+ x. u x * indicator N x \M) = 0" ``` hoelzl@38656 ` 1311` ```proof - ``` wenzelm@53015 ` 1312` ``` have "(\\<^sup>+ x. u x * indicator N x \M) = (\\<^sup>+ x. 0 \M)" ``` hoelzl@40859 ` 1313` ``` proof (intro positive_integral_cong_AE AE_I) ``` hoelzl@40859 ` 1314` ``` show "{x \ space M. u x * indicator N x \ 0} \ N" ``` hoelzl@40859 ` 1315` ``` by (auto simp: indicator_def) ``` hoelzl@47694 ` 1316` ``` show "(emeasure M) N = 0" "N \ sets M" ``` hoelzl@40859 ` 1317` ``` using assms by auto ``` hoelzl@35582 ` 1318` ``` qed ``` hoelzl@40859 ` 1319` ``` then show ?thesis by simp ``` hoelzl@38656 ` 1320` ```qed ``` hoelzl@35582 ` 1321` hoelzl@47694 ` 1322` ```lemma positive_integral_0_iff: ``` hoelzl@47694 ` 1323` ``` assumes u: "u \ borel_measurable M" and pos: "AE x in M. 0 \ u x" ``` wenzelm@53015 ` 1324` ``` shows "integral\<^sup>P M u = 0 \ emeasure M {x\space M. u x \ 0} = 0" ``` hoelzl@47694 ` 1325` ``` (is "_ \ (emeasure M) ?A = 0") ``` hoelzl@35582 ` 1326` ```proof - ``` wenzelm@53015 ` 1327` ``` have u_eq: "(\\<^sup>+ x. u x * indicator ?A x \M) = integral\<^sup>P M u" ``` hoelzl@38656 ` 1328` ``` by (auto intro!: positive_integral_cong simp: indicator_def) ``` hoelzl@38656 ` 1329` ``` show ?thesis ``` hoelzl@38656 ` 1330` ``` proof ``` hoelzl@47694 ` 1331` ``` assume "(emeasure M) ?A = 0" ``` hoelzl@47694 ` 1332` ``` with positive_integral_null_set[of ?A M u] u ``` wenzelm@53015 ` 1333` ``` show "integral\<^sup>P M u = 0" by (simp add: u_eq null_sets_def) ``` hoelzl@38656 ` 1334` ``` next ``` hoelzl@43920 ` 1335` ``` { fix r :: ereal and n :: nat assume gt_1: "1 \ real n * r" ``` hoelzl@43920 ` 1336` ``` then have "0 < real n * r" by (cases r) (auto split: split_if_asm simp: one_ereal_def) ``` hoelzl@43920 ` 1337` ``` then have "0 \ r" by (auto simp add: ereal_zero_less_0_iff) } ``` hoelzl@41981 ` 1338` ``` note gt_1 = this ``` wenzelm@53015 ` 1339` ``` assume *: "integral\<^sup>P M u = 0" ``` wenzelm@46731 ` 1340` ``` let ?M = "\n. {x \ space M. 1 \ real (n::nat) * u x}" ``` hoelzl@47694 ` 1341` ``` have "0 = (SUP n. (emeasure M) (?M n \ ?A))" ``` hoelzl@38656 ` 1342` ``` proof - ``` hoelzl@41981 ` 1343` ``` { fix n :: nat ``` hoelzl@43920 ` 1344` ``` from positive_integral_Markov_inequality[OF u pos, of ?A "ereal (real n)"] ``` hoelzl@47694 ` 1345` ``` have "(emeasure M) (?M n \ ?A) \ 0" unfolding u_eq * using u by simp ``` hoelzl@47694 ` 1346` ``` moreover have "0 \ (emeasure M) (?M n \ ?A)" using u by auto ``` hoelzl@47694 ` 1347` ``` ultimately have "(emeasure M) (?M n \ ?A) = 0" by auto } ``` hoelzl@38656 ` 1348` ``` thus ?thesis by simp ``` hoelzl@35582 ` 1349` ``` qed ``` hoelzl@47694 ` 1350` ``` also have "\ = (emeasure M) (\n. ?M n \ ?A)" ``` hoelzl@47694 ` 1351` ``` proof (safe intro!: SUP_emeasure_incseq) ``` hoelzl@38656 ` 1352` ``` fix n show "?M n \ ?A \ sets M" ``` immler@50244 ` 1353` ``` using u by (auto intro!: sets.Int) ``` hoelzl@38656 ` 1354` ``` next ``` hoelzl@41981 ` 1355` ``` show "incseq (\n. {x \ space M. 1 \ real n * u x} \ {x \ space M. u x \ 0})" ``` hoelzl@41981 ` 1356` ``` proof (safe intro!: incseq_SucI) ``` hoelzl@41981 ` 1357` ``` fix n :: nat and x ``` hoelzl@41981 ` 1358` ``` assume *: "1 \ real n * u x" ``` wenzelm@53374 ` 1359` ``` also from gt_1[OF *] have "real n * u x \ real (Suc n) * u x" ``` hoelzl@43920 ` 1360` ``` using `0 \ u x` by (auto intro!: ereal_mult_right_mono) ``` hoelzl@41981 ` 1361` ``` finally show "1 \ real (Suc n) * u x" by auto ``` hoelzl@41981 ` 1362` ``` qed ``` hoelzl@38656 ` 1363` ``` qed ``` hoelzl@47694 ` 1364` ``` also have "\ = (emeasure M) {x\space M. 0 < u x}" ``` hoelzl@47694 ` 1365` ``` proof (safe intro!: arg_cong[where f="(emeasure M)"] dest!: gt_1) ``` hoelzl@41981 ` 1366` ``` fix x assume "0 < u x" and [simp, intro]: "x \ space M" ``` hoelzl@38656 ` 1367` ``` show "x \ (\n. ?M n \ ?A)" ``` hoelzl@38656 ` 1368` ``` proof (cases "u x") ``` hoelzl@41981 ` 1369` ``` case (real r) with `0 < u x` have "0 < r" by auto ``` hoelzl@41981 ` 1370` ``` obtain j :: nat where "1 / r \ real j" using real_arch_simple .. ``` hoelzl@41981 ` 1371` ``` hence "1 / r * r \ real j * r" unfolding mult_le_cancel_right using `0 < r` by auto ``` hoelzl@41981 ` 1372` ``` hence "1 \ real j * r" using real `0 < r` by auto ``` hoelzl@43920 ` 1373` ``` thus ?thesis using `0 < r` real by (auto simp: one_ereal_def) ``` hoelzl@41981 ` 1374` ``` qed (insert `0 < u x`, auto) ``` hoelzl@41981 ` 1375` ``` qed auto ``` hoelzl@47694 ` 1376` ``` finally have "(emeasure M) {x\space M. 0 < u x} = 0" by simp ``` hoelzl@41981 ` 1377` ``` moreover ``` hoelzl@47694 ` 1378` ``` from pos have "AE x in M. \ (u x < 0)" by auto ``` hoelzl@47694 ` 1379` ``` then have "(emeasure M) {x\space M. u x < 0} = 0" ``` hoelzl@47694 ` 1380` ``` using AE_iff_null[of M] u by auto ``` hoelzl@47694 ` 1381` ``` moreover have "(emeasure M) {x\space M. u x \ 0} = (emeasure M) {x\space M. u x < 0} + (emeasure M) {x\space M. 0 < u x}" ``` hoelzl@47694 ` 1382` ``` using u by (subst plus_emeasure) (auto intro!: arg_cong[where f="emeasure M"]) ``` hoelzl@47694 ` 1383` ``` ultimately show "(emeasure M) ?A = 0" by simp ``` hoelzl@35582 ` 1384` ``` qed ``` hoelzl@35582 ` 1385` ```qed ``` hoelzl@35582 ` 1386` hoelzl@47694 ` 1387` ```lemma positive_integral_0_iff_AE: ``` hoelzl@41705 ` 1388` ``` assumes u: "u \ borel_measurable M" ``` wenzelm@53015 ` 1389` ``` shows "integral\<^sup>P M u = 0 \ (AE x in M. u x \ 0)" ``` hoelzl@41705 ` 1390` ```proof - ``` hoelzl@41981 ` 1391` ``` have sets: "{x\space M. max 0 (u x) \ 0} \ sets M" ``` hoelzl@41705 ` 1392` ``` using u by auto ``` hoelzl@41981 ` 1393` ``` from positive_integral_0_iff[of "\x. max 0 (u x)"] ``` wenzelm@53015 ` 1394` ``` have "integral\<^sup>P M u = 0 \ (AE x in M. max 0 (u x) = 0)" ``` hoelzl@41981 ` 1395` ``` unfolding positive_integral_max_0 ``` hoelzl@47694 ` 1396` ``` using AE_iff_null[OF sets] u by auto ``` hoelzl@47694 ` 1397` ``` also have "\ \ (AE x in M. u x \ 0)" by (auto split: split_max) ``` hoelzl@41981 ` 1398` ``` finally show ?thesis . ``` hoelzl@41705 ` 1399` ```qed ``` hoelzl@41705 ` 1400` hoelzl@50001 ` 1401` ```lemma AE_iff_positive_integral: ``` wenzelm@53015 ` 1402` ``` "{x\space M. P x} \ sets M \ (AE x in M. P x) \ integral\<^sup>P M (indicator {x. \ P x}) = 0" ``` immler@50244 ` 1403` ``` by (subst positive_integral_0_iff_AE) (auto simp: one_ereal_def zero_ereal_def ``` immler@50244 ` 1404` ``` sets.sets_Collect_neg indicator_def[abs_def] measurable_If) ``` hoelzl@50001 ` 1405` hoelzl@47694 ` 1406` ```lemma positive_integral_const_If: ``` wenzelm@53015 ` 1407` ``` "(\\<^sup>+x. a \M) = (if 0 \ a then a * (emeasure M) (space M) else 0)" ``` hoelzl@42991 ` 1408` ``` by (auto intro!: positive_integral_0_iff_AE[THEN iffD2]) ``` hoelzl@42991 ` 1409` hoelzl@47694 ` 1410` ```lemma positive_integral_subalgebra: ``` hoelzl@49799 ` 1411` ``` assumes f: "f \ borel_measurable N" "\x. 0 \ f x" ``` hoelzl@47694 ` 1412` ``` and N: "sets N \ sets M" "space N = space M" "\A. A \ sets N \ emeasure N A = emeasure M A" ``` wenzelm@53015 ` 1413` ``` shows "integral\<^sup>P N f = integral\<^sup>P M f" ``` hoelzl@39092 ` 1414` ```proof - ``` hoelzl@49799 ` 1415` ``` have [simp]: "\f :: 'a \ ereal. f \ borel_measurable N \ f \ borel_measurable M" ``` hoelzl@49799 ` 1416` ``` using N by (auto simp: measurable_def) ``` hoelzl@49799 ` 1417` ``` have [simp]: "\P. (AE x in N. P x) \ (AE x in M. P x)" ``` hoelzl@49799 ` 1418` ``` using N by (auto simp add: eventually_ae_filter null_sets_def) ``` hoelzl@49799 ` 1419` ``` have [simp]: "\A. A \ sets N \ A \ sets M" ``` hoelzl@49799 ` 1420` ``` using N by auto ``` hoelzl@49799 ` 1421` ``` from f show ?thesis ``` hoelzl@49799 ` 1422` ``` apply induct ``` hoelzl@49799 ` 1423` ``` apply (simp_all add: positive_integral_add positive_integral_cmult positive_integral_monotone_convergence_SUP N) ``` hoelzl@49799 ` 1424` ``` apply (auto intro!: positive_integral_cong cong: positive_integral_cong simp: N(2)[symmetric]) ``` hoelzl@49799 ` 1425` ``` done ``` hoelzl@39092 ` 1426` ```qed ``` hoelzl@39092 ` 1427` hoelzl@50097 ` 1428` ```lemma positive_integral_nat_function: ``` hoelzl@50097 ` 1429` ``` fixes f :: "'a \ nat" ``` hoelzl@50097 ` 1430` ``` assumes "f \ measurable M (count_space UNIV)" ``` wenzelm@53015 ` 1431` ``` shows "(\\<^sup>+x. ereal (of_nat (f x)) \M) = (\t. emeasure M {x\space M. t < f x})" ``` hoelzl@50097 ` 1432` ```proof - ``` hoelzl@50097 ` 1433` ``` def F \ "\i. {x\space M. i < f x}" ``` hoelzl@50097 ` 1434` ``` with assms have [measurable]: "\i. F i \ sets M" ``` hoelzl@50097 ` 1435` ``` by auto ``` hoelzl@50097 ` 1436` hoelzl@50097 ` 1437` ``` { fix x assume "x \ space M" ``` hoelzl@50097 ` 1438` ``` have "(\i. if i < f x then 1 else 0) sums (of_nat (f x)::real)" ``` hoelzl@50097 ` 1439` ``` using sums_If_finite[of "\i. i < f x" "\_. 1::real"] by simp ``` hoelzl@50097 ` 1440` ``` then have "(\i. ereal(if i < f x then 1 else 0)) sums (ereal(of_nat(f x)))" ``` hoelzl@50097 ` 1441` ``` unfolding sums_ereal . ``` hoelzl@50097 ` 1442` ``` moreover have "\i. ereal (if i < f x then 1 else 0) = indicator (F i) x" ``` hoelzl@50097 ` 1443` ``` using `x \ space M` by (simp add: one_ereal_def F_def) ``` hoelzl@50097 ` 1444` ``` ultimately have "ereal(of_nat(f x)) = (\i. indicator (F i) x)" ``` hoelzl@50097 ` 1445` ``` by (simp add: sums_iff) } ``` wenzelm@53015 ` 1446` ``` then have "(\\<^sup>+x. ereal (of_nat (f x)) \M) = (\\<^sup>+x. (\i. indicator (F i) x) \M)" ``` hoelzl@50097 ` 1447` ``` by (simp cong: positive_integral_cong) ``` hoelzl@50097 ` 1448` ``` also have "\ = (\i. emeasure M (F i))" ``` hoelzl@50097 ` 1449` ``` by (simp add: positive_integral_suminf) ``` hoelzl@50097 ` 1450` ``` finally show ?thesis ``` hoelzl@50097 ` 1451` ``` by (simp add: F_def) ``` hoelzl@50097 ` 1452` ```qed ``` hoelzl@50097 ` 1453` hoelzl@35692 ` 1454` ```section "Lebesgue Integral" ``` hoelzl@35692 ` 1455` hoelzl@47694 ` 1456` ```definition integrable :: "'a measure \ ('a \ real) \ bool" where ``` hoelzl@41689 ` 1457` ``` "integrable M f \ f \ borel_measurable M \ ``` wenzelm@53015 ` 1458` ``` (\\<^sup>+ x. ereal (f x) \M) \ \ \ (\\<^sup>+ x. ereal (- f x) \M) \ \" ``` hoelzl@35692 ` 1459` hoelzl@50003 ` 1460` ```lemma borel_measurable_integrable[measurable_dest]: ``` hoelzl@50003 ` 1461` ``` "integrable M f \ f \ borel_measurable M" ``` hoelzl@50003 ` 1462` ``` by (auto simp: integrable_def) ``` hoelzl@50003 ` 1463` hoelzl@41689 ` 1464` ```lemma integrableD[dest]: ``` hoelzl@41689 ` 1465` ``` assumes "integrable M f" ``` wenzelm@53015 ` 1466` ``` shows "f \ borel_measurable M" "(\\<^sup>+ x. ereal (f x) \M) \ \" "(\\<^sup>+ x. ereal (- f x) \M) \ \" ``` hoelzl@38656 ` 1467` ``` using assms unfolding integrable_def by auto ``` hoelzl@35692 ` 1468` wenzelm@53015 ` 1469` ```definition lebesgue_integral :: "'a measure \ ('a \ real) \ real" ("integral\<^sup>L") where ``` wenzelm@53015 ` 1470` ``` "integral\<^sup>L M f = real ((\\<^sup>+ x. ereal (f x) \M)) - real ((\\<^sup>+ x. ereal (- f x) \M))" ``` hoelzl@41689 ` 1471` hoelzl@41689 ` 1472` ```syntax ``` hoelzl@47694 ` 1473` ``` "_lebesgue_integral" :: "pttrn \ real \ 'a measure \ real" ("\ _. _ \_" [60,61] 110) ``` hoelzl@41689 ` 1474` hoelzl@41689 ` 1475` ```translations ``` hoelzl@47694 ` 1476` ``` "\ x. f \M" == "CONST lebesgue_integral M (%x. f)" ``` hoelzl@38656 ` 1477` hoelzl@47694 ` 1478` ```lemma integrableE: ``` hoelzl@41981 ` 1479` ``` assumes "integrable M f" ``` hoelzl@41981 ` 1480` ``` obtains r q where ``` wenzelm@53015 ` 1481` ``` "(\\<^sup>+x. ereal (f x)\M) = ereal r" ``` wenzelm@53015 ` 1482` ``` "(\\<^sup>+x. ereal (-f x)\M) = ereal q" ``` wenzelm@53015 ` 1483` ``` "f \ borel_measurable M" "integral\<^sup>L M f = r - q" ``` hoelzl@41981 ` 1484` ``` using assms unfolding integrable_def lebesgue_integral_def ``` hoelzl@47694 ` 1485` ``` using positive_integral_positive[of M "\x. ereal (f x)"] ``` hoelzl@47694 ` 1486` ``` using positive_integral_positive[of M "\x. ereal (-f x)"] ``` wenzelm@53015 ` 1487` ``` by (cases rule: ereal2_cases[of "(\\<^sup>+x. ereal (-f x)\M)" "(\\<^sup>+x. ereal (f x)\M)"]) auto ``` hoelzl@41981 ` 1488` hoelzl@47694 ` 1489` ```lemma integral_cong: ``` hoelzl@41689 ` 1490` ``` assumes "\x. x \ space M \ f x = g x" ``` wenzelm@53015 ` 1491` ``` shows "integral\<^sup>L M f = integral\<^sup>L M g" ``` hoelzl@41689 ` 1492` ``` using assms by (simp cong: positive_integral_cong add: lebesgue_integral_def) ``` hoelzl@35582 ` 1493` hoelzl@47694 ` 1494` ```lemma integral_cong_AE: ``` hoelzl@47694 ` 1495` ``` assumes cong: "AE x in M. f x = g x" ``` wenzelm@53015 ` 1496` ``` shows "integral\<^sup>L M f = integral\<^sup>L M g" ``` hoelzl@40859 ` 1497` ```proof - ``` hoelzl@47694 ` 1498` ``` have *: "AE x in M. ereal (f x) = ereal (g x)" ``` hoelzl@47694 ` 1499` ``` "AE x in M. ereal (- f x) = ereal (- g x)" using cong by auto ``` hoelzl@41981 ` 1500` ``` show ?thesis ``` hoelzl@41981 ` 1501` ``` unfolding *[THEN positive_integral_cong_AE] lebesgue_integral_def .. ``` hoelzl@40859 ` 1502` ```qed ``` hoelzl@40859 ` 1503` hoelzl@47694 ` 1504` ```lemma integrable_cong_AE: ``` hoelzl@43339 ` 1505` ``` assumes borel: "f \ borel_measurable M" "g \ borel_measurable M" ``` hoelzl@47694 ` 1506` ``` assumes "AE x in M. f x = g x" ``` hoelzl@43339 ` 1507` ``` shows "integrable M f = integrable M g" ``` hoelzl@43339 ` 1508` ```proof - ``` wenzelm@53015 ` 1509` ``` have "(\\<^sup>+ x. ereal (f x) \M) = (\\<^sup>+ x. ereal (g x) \M)" ``` wenzelm@53015 ` 1510` ``` "(\\<^sup>+ x. ereal (- f x) \M) = (\\<^sup>+ x. ereal (- g x) \M)" ``` hoelzl@43339 ` 1511` ``` using assms by (auto intro!: positive_integral_cong_AE) ``` hoelzl@43339 ` 1512` ``` with assms show ?thesis ``` hoelzl@43339 ` 1513` ``` by (auto simp: integrable_def) ``` hoelzl@43339 ` 1514` ```qed ``` hoelzl@43339 ` 1515` hoelzl@47694 ` 1516` ```lemma integrable_cong: ``` hoelzl@41689 ` 1517` ``` "(\x. x \ space M \ f x = g x) \ integrable M f \ integrable M g" ``` hoelzl@38656 ` 1518` ``` by (simp cong: positive_integral_cong measurable_cong add: integrable_def) ``` hoelzl@38656 ` 1519` hoelzl@49775 ` 1520` ```lemma integral_mono_AE: ``` hoelzl@49775 ` 1521` ``` assumes fg: "integrable M f" "integrable M g" ``` hoelzl@49775 ` 1522` ``` and mono: "AE t in M. f t \ g t" ``` wenzelm@53015 ` 1523` ``` shows "integral\<^sup>L M f \ integral\<^sup>L M g" ``` hoelzl@49775 ` 1524` ```proof - ``` hoelzl@49775 ` 1525` ``` have "AE x in M. ereal (f x) \ ereal (g x)" ``` hoelzl@49775 ` 1526` ``` using mono by auto ``` hoelzl@49775 ` 1527` ``` moreover have "AE x in M. ereal (- g x) \ ereal (- f x)" ``` hoelzl@49775 ` 1528` ``` using mono by auto ``` hoelzl@49775 ` 1529` ``` ultimately show ?thesis using fg ``` hoelzl@49775 ` 1530` ``` by (auto intro!: add_mono positive_integral_mono_AE real_of_ereal_positive_mono ``` haftmann@54230 ` 1531` ``` simp: positive_integral_positive lebesgue_integral_def algebra_simps) ``` hoelzl@49775 ` 1532` ```qed ``` hoelzl@49775 ` 1533` hoelzl@49775 ` 1534` ```lemma integral_mono: ``` hoelzl@49775 ` 1535` ``` assumes "integrable M f" "integrable M g" "\t. t \ space M \ f t \ g t" ``` wenzelm@53015 ` 1536` ``` shows "integral\<^sup>L M f \ integral\<^sup>L M g" ``` hoelzl@49775 ` 1537` ``` using assms by (auto intro: integral_mono_AE) ``` hoelzl@49775 ` 1538` hoelzl@47694 ` 1539` ```lemma positive_integral_eq_integral: ``` hoelzl@47694 ` 1540` ``` assumes f: "integrable M f" ``` hoelzl@47694 ` 1541` ``` assumes nonneg: "AE x in M. 0 \ f x" ``` wenzelm@53015 ` 1542` ``` shows "(\\<^sup>+ x. ereal (f x) \M) = integral\<^sup>L M f" ``` hoelzl@47694 ` 1543` ```proof - ``` wenzelm@53015 ` 1544` ``` have "(\\<^sup>+ x. max 0 (ereal (- f x)) \M) = (\\<^sup>+ x. 0 \M)" ``` hoelzl@47694 ` 1545` ``` using nonneg by (intro positive_integral_cong_AE) (auto split: split_max) ``` hoelzl@47694 ` 1546` ``` with f positive_integral_positive show ?thesis ``` wenzelm@53015 ` 1547` ``` by (cases "\\<^sup>+ x. ereal (f x) \M") ``` hoelzl@47694 ` 1548` ``` (auto simp add: lebesgue_integral_def positive_integral_max_0 integrable_def) ``` hoelzl@47694 ` 1549` ```qed ``` hoelzl@47694 ` 1550` ``` ``` hoelzl@47694 ` 1551` ```lemma integral_eq_positive_integral: ``` hoelzl@41981 ` 1552` ``` assumes f: "\x. 0 \ f x" ``` wenzelm@53015 ` 1553` ``` shows "integral\<^sup>L M f = real (\\<^sup>+ x. ereal (f x) \M)" ``` hoelzl@35582 ` 1554` ```proof - ``` hoelzl@43920 ` 1555` ``` { fix x have "max 0 (ereal (- f x)) = 0" using f[of x] by (simp split: split_max) } ``` wenzelm@53015 ` 1556` ``` then have "0 = (\\<^sup>+ x. max 0 (ereal (- f x)) \M)" by simp ``` wenzelm@53015 ` 1557` ``` also have "\ = (\\<^sup>+ x. ereal (- f x) \M)" unfolding positive_integral_max_0 .. ``` hoelzl@41981 ` 1558` ``` finally show ?thesis ``` hoelzl@41981 ` 1559` ``` unfolding lebesgue_integral_def by simp ``` hoelzl@35582 ` 1560` ```qed ``` hoelzl@35582 ` 1561` hoelzl@47694 ` 1562` ```lemma integral_minus[intro, simp]: ``` hoelzl@41689 ` 1563` ``` assumes "integrable M f" ``` wenzelm@53015 ` 1564` ``` shows "integrable M (\x. - f x)" "(\x. - f x \M) = - integral\<^sup>L M f" ``` hoelzl@41689 ` 1565` ``` using assms by (auto simp: integrable_def lebesgue_integral_def) ``` hoelzl@38656 ` 1566` hoelzl@47694 ` 1567` ```lemma integral_minus_iff[simp]: ``` hoelzl@42991 ` 1568` ``` "integrable M (\x. - f x) \ integrable M f" ``` hoelzl@42991 ` 1569` ```proof ``` hoelzl@42991 ` 1570` ``` assume "integrable M (\x. - f x)" ``` hoelzl@42991 ` 1571` ``` then have "integrable M (\x. - (- f x))" ``` hoelzl@42991 ` 1572` ``` by (rule integral_minus) ``` hoelzl@42991 ` 1573` ``` then show "integrable M f" by simp ``` hoelzl@42991 ` 1574` ```qed (rule integral_minus) ``` hoelzl@42991 ` 1575` hoelzl@47694 ` 1576` ```lemma integral_of_positive_diff: ``` hoelzl@41689 ` 1577` ``` assumes integrable: "integrable M u" "integrable M v" ``` hoelzl@38656 ` 1578` ``` and f_def: "\x. f x = u x - v x" and pos: "\x. 0 \ u x" "\x. 0 \ v x" ``` wenzelm@53015 ` 1579` ``` shows "integrable M f" and "integral\<^sup>L M f = integral\<^sup>L M u - integral\<^sup>L M v" ``` hoelzl@35582 ` 1580` ```proof - ``` wenzelm@46731 ` 1581` ``` let ?f = "\x. max 0 (ereal (f x))" ``` wenzelm@46731 ` 1582` ``` let ?mf = "\x. max 0 (ereal (- f x))" ``` wenzelm@46731 ` 1583` ``` let ?u = "\x. max 0 (ereal (u x))" ``` wenzelm@46731 ` 1584` ``` let ?v = "\x. max 0 (ereal (v x))" ``` hoelzl@38656 ` 1585` hoelzl@47694 ` 1586` ``` from borel_measurable_diff[of u M v] integrable ``` hoelzl@38656 ` 1587` ``` have f_borel: "?f \ borel_measurable M" and ``` hoelzl@38656 ` 1588` ``` mf_borel: "?mf \ borel_measurable M" and ``` hoelzl@38656 ` 1589` ``` v_borel: "?v \ borel_measurable M" and ``` hoelzl@38656 ` 1590` ``` u_borel: "?u \ borel_measurable M" and ``` hoelzl@38656 ` 1591` ``` "f \ borel_measurable M" ``` hoelzl@38656 ` 1592` ``` by (auto simp: f_def[symmetric] integrable_def) ``` hoelzl@35582 ` 1593` wenzelm@53015 ` 1594` ``` have "(\\<^sup>+ x. ereal (u x - v x) \M) \ integral\<^sup>P M ?u" ``` hoelzl@41981 ` 1595` ``` using pos by (auto intro!: positive_integral_mono simp: positive_integral_max_0) ``` wenzelm@53015 ` 1596` ``` moreover have "(\\<^sup>+ x. ereal (v x - u x) \M) \ integral\<^sup>P M ?v" ``` hoelzl@41981 ` 1597` ``` using pos by (auto intro!: positive_integral_mono simp: positive_integral_max_0) ``` hoelzl@41689 ` 1598` ``` ultimately show f: "integrable M f" ``` hoelzl@41689 ` 1599` ``` using `integrable M u` `integrable M v` `f \ borel_measurable M` ``` hoelzl@41981 ` 1600` ``` by (auto simp: integrable_def f_def positive_integral_max_0) ``` hoelzl@35582 ` 1601` hoelzl@38656 ` 1602` ``` have "\x. ?u x + ?mf x = ?v x + ?f x" ``` hoelzl@41981 ` 1603` ``` unfolding f_def using pos by (simp split: split_max) ``` wenzelm@53015 ` 1604` ``` then have "(\\<^sup>+ x. ?u x + ?mf x \M) = (\\<^sup>+ x. ?v x + ?f x \M)" by simp ``` wenzelm@53015 ` 1605` ``` then have "real (integral\<^sup>P M ?u + integral\<^sup>P M ?mf) = ``` wenzelm@53015 ` 1606` ``` real (integral\<^sup>P M ?v + integral\<^sup>P M ?f)" ``` hoelzl@41981 ` 1607` ``` using positive_integral_add[OF u_borel _ mf_borel] ``` hoelzl@41981 ` 1608` ``` using positive_integral_add[OF v_borel _ f_borel] ``` hoelzl@38656 ` 1609` ``` by auto ``` wenzelm@53015 ` 1610` ``` then show "integral\<^sup>L M f = integral\<^sup>L M u - integral\<^sup>L M v" ``` hoelzl@41981 ` 1611` ``` unfolding positive_integral_max_0 ``` hoelzl@41981 ` 1612` ``` unfolding pos[THEN integral_eq_positive_integral] ``` hoelzl@41981 ` 1613` ``` using integrable f by (auto elim!: integrableE) ``` hoelzl@35582 ` 1614` ```qed ``` hoelzl@35582 ` 1615` hoelzl@47694 ` 1616` ```lemma integral_linear: ``` hoelzl@41689 ` 1617` ``` assumes "integrable M f" "integrable M g" and "0 \ a" ``` hoelzl@41689 ` 1618` ``` shows "integrable M (\t. a * f t + g t)" ``` wenzelm@53015 ` 1619` ``` and "(\ t. a * f t + g t \M) = a * integral\<^sup>L M f + integral\<^sup>L M g" (is ?EQ) ``` hoelzl@38656 ` 1620` ```proof - ``` wenzelm@46731 ` 1621` ``` let ?f = "\x. max 0 (ereal (f x))" ``` wenzelm@46731 ` 1622` ``` let ?g = "\x. max 0 (ereal (g x))" ``` wenzelm@46731 ` 1623` ``` let ?mf = "\x. max 0 (ereal (- f x))" ``` wenzelm@46731 ` 1624` ``` let ?mg = "\x. max 0 (ereal (- g x))" ``` wenzelm@46731 ` 1625` ``` let ?p = "\t. max 0 (a * f t) + max 0 (g t)" ``` wenzelm@46731 ` 1626` ``` let ?n = "\t. max 0 (- (a * f t)) + max 0 (- g t)" ``` hoelzl@38656 ` 1627` hoelzl@41981 ` 1628` ``` from assms have linear: ``` wenzelm@53015 ` 1629` ``` "(\\<^sup>+ x. ereal a * ?f x + ?g x \M) = ereal a * integral\<^sup>P M ?f + integral\<^sup>P M ?g" ``` wenzelm@53015 ` 1630` ``` "(\\<^sup>+ x. ereal a * ?mf x + ?mg x \M) = ereal a * integral\<^sup>P M ?mf + integral\<^sup>P M ?mg" ``` hoelzl@41981 ` 1631` ``` by (auto intro!: positive_integral_linear simp: integrable_def) ``` hoelzl@35582 ` 1632` wenzelm@53015 ` 1633` ``` have *: "(\\<^sup>+x. ereal (- ?p x) \M) = 0" "(\\<^sup>+x. ereal (- ?n x) \M) = 0" ``` hoelzl@41981 ` 1634` ``` using `0 \ a` assms by (auto simp: positive_integral_0_iff_AE integrable_def) ``` hoelzl@43920 ` 1635` ``` have **: "\x. ereal a * ?f x + ?g x = max 0 (ereal (?p x))" ``` hoelzl@43920 ` 1636` ``` "\x. ereal a * ?mf x + ?mg x = max 0 (ereal (?n x))" ``` hoelzl@41981 ` 1637` ``` using `0 \ a` by (auto split: split_max simp: zero_le_mult_iff mult_le_0_iff) ``` hoelzl@35582 ` 1638` hoelzl@41689 ` 1639` ``` have "integrable M ?p" "integrable M ?n" ``` hoelzl@38656 ` 1640` ``` "\t. a * f t + g t = ?p t - ?n t" "\t. 0 \ ?p t" "\t. 0 \ ?n t" ``` hoelzl@41981 ` 1641` ``` using linear assms unfolding integrable_def ** * ``` hoelzl@41981 ` 1642` ``` by (auto simp: positive_integral_max_0) ``` hoelzl@38656 ` 1643` ``` note diff = integral_of_positive_diff[OF this] ``` hoelzl@38656 ` 1644` hoelzl@41689 ` 1645` ``` show "integrable M (\t. a * f t + g t)" by (rule diff) ``` hoelzl@41981 ` 1646` ``` from assms linear show ?EQ ``` hoelzl@41981 ` 1647` ``` unfolding diff(2) ** positive_integral_max_0 ``` hoelzl@41981 ` 1648` ``` unfolding lebesgue_integral_def * ``` hoelzl@41981 ` 1649` ``` by (auto elim!: integrableE simp: field_simps) ``` hoelzl@38656 ` 1650` ```qed ``` hoelzl@38656 ` 1651` hoelzl@47694 ` 1652` ```lemma integral_add[simp, intro]: ``` hoelzl@41689 ` 1653` ``` assumes "integrable M f" "integrable M g" ``` hoelzl@41689 ` 1654` ``` shows "integrable M (\t. f t + g t)" ``` wenzelm@53015 ` 1655` ``` and "(\ t. f t + g t \M) = integral\<^sup>L M f + integral\<^sup>L M g" ``` hoelzl@38656 ` 1656` ``` using assms integral_linear[where a=1] by auto ``` hoelzl@38656 ` 1657` hoelzl@47694 ` 1658` ```lemma integral_zero[simp, intro]: ``` hoelzl@41689 ` 1659` ``` shows "integrable M (\x. 0)" "(\ x.0 \M) = 0" ``` hoelzl@41689 ` 1660` ``` unfolding integrable_def lebesgue_integral_def ``` hoelzl@50002 ` 1661` ``` by auto ``` hoelzl@35582 ` 1662` hoelzl@50097 ` 1663` ```lemma lebesgue_integral_uminus: ``` wenzelm@53015 ` 1664` ``` "(\x. - f x \M) = - integral\<^sup>L M f" ``` hoelzl@50097 ` 1665` ``` unfolding lebesgue_integral_def by simp ``` hoelzl@35582 ` 1666` hoelzl@47694 ` 1667` ```lemma lebesgue_integral_cmult_nonneg: ``` hoelzl@47694 ` 1668` ``` assumes f: "f \ borel_measurable M" and "0 \ c" ``` wenzelm@53015 ` 1669` ``` shows "(\x. c * f x \M) = c * integral\<^sup>L M f" ``` hoelzl@47694 ` 1670` ```proof - ``` wenzelm@53015 ` 1671` ``` { have "real (ereal c * integral\<^sup>P M (\x. max 0 (ereal (f x)))) = ``` wenzelm@53015 ` 1672` ``` real (integral\<^sup>P M (\x. ereal c * max 0 (ereal (f x))))" ``` hoelzl@47694 ` 1673` ``` using f `0 \ c` by (subst positive_integral_cmult) auto ``` wenzelm@53015 ` 1674` ``` also have "\ = real (integral\<^sup>P M (\x. max 0 (ereal (c * f x))))" ``` hoelzl@47694 ` 1675` ``` using `0 \ c` by (auto intro!: arg_cong[where f=real] positive_integral_cong simp: max_def zero_le_mult_iff) ``` wenzelm@53015 ` 1676` ``` finally have "real (integral\<^sup>P M (\x. ereal (c * f x))) = c * real (integral\<^sup>P M (\x. ereal (f x)))" ``` hoelzl@47694 ` 1677` ``` by (simp add: positive_integral_max_0) } ``` hoelzl@47694 ` 1678` ``` moreover ``` wenzelm@53015 ` 1679` ``` { have "real (ereal c * integral\<^sup>P M (\x. max 0 (ereal (- f x)))) = ``` wenzelm@53015 ` 1680` ``` real (integral\<^sup>P M (\x. ereal c * max 0 (ereal (- f x))))" ``` hoelzl@47694 ` 1681` ``` using f `0 \ c` by (subst positive_integral_cmult) auto ``` wenzelm@53015 ` 1682` ``` also have "\ = real (integral\<^sup>P M (\x. max 0 (ereal (- c * f x))))" ``` hoelzl@47694 ` 1683` ``` using `0 \ c` by (auto intro!: arg_cong[where f=real] positive_integral_cong simp: max_def mult_le_0_iff) ``` wenzelm@53015 ` 1684` ``` finally have "real (integral\<^sup>P M (\x. ereal (- c * f x))) = c * real (integral\<^sup>P M (\x. ereal (- f x)))" ``` hoelzl@47694 ` 1685` ``` by (simp add: positive_integral_max_0) } ``` hoelzl@47694 ` 1686` ``` ultimately show ?thesis ``` hoelzl@47694 ` 1687` ``` by (simp add: lebesgue_integral_def field_simps) ``` hoelzl@47694 ` 1688` ```qed ``` hoelzl@47694 ` 1689` hoelzl@47694 ` 1690` ```lemma lebesgue_integral_cmult: ``` hoelzl@47694 ` 1691` ``` assumes f: "f \ borel_measurable M" ``` wenzelm@53015 ` 1692` ``` shows "(\x. c * f x \M) = c * integral\<^sup>L M f" ``` hoelzl@47694 ` 1693` ```proof (cases rule: linorder_le_cases) ``` hoelzl@47694 ` 1694` ``` assume "0 \ c" with f show ?thesis by (rule lebesgue_integral_cmult_nonneg) ``` hoelzl@47694 ` 1695` ```next ``` hoelzl@47694 ` 1696` ``` assume "c \ 0" ``` hoelzl@47694 ` 1697` ``` with lebesgue_integral_cmult_nonneg[OF f, of "-c"] ``` hoelzl@47694 ` 1698` ``` show ?thesis ``` hoelzl@47694 ` 1699` ``` by (simp add: lebesgue_integral_def) ``` hoelzl@47694 ` 1700` ```qed ``` hoelzl@47694 ` 1701` hoelzl@50097 ` 1702` ```lemma lebesgue_integral_multc: ``` wenzelm@53015 ` 1703` ``` "f \ borel_measurable M \ (\x. f x * c \M) = integral\<^sup>L M f * c" ``` hoelzl@50097 ` 1704` ``` using lebesgue_integral_cmult[of f M c] by (simp add: ac_simps) ``` hoelzl@50097 ` 1705` hoelzl@47694 ` 1706` ```lemma integral_multc: ``` wenzelm@53015 ` 1707` ``` "integrable M f \ (\ x. f x * c \M) = integral\<^sup>L M f * c" ``` hoelzl@50097 ` 1708` ``` by (simp add: lebesgue_integral_multc) ``` hoelzl@50097 ` 1709` hoelzl@50097 ` 1710` ```lemma integral_cmult[simp, intro]: ``` hoelzl@41689 ` 1711` ``` assumes "integrable M f" ``` hoelzl@50097 ` 1712` ``` shows "integrable M (\t. a * f t)" (is ?P) ``` wenzelm@53015 ` 1713` ``` and "(\ t. a * f t \M) = a * integral\<^sup>L M f" (is ?I) ``` hoelzl@50097 ` 1714` ```proof - ``` wenzelm@53015 ` 1715` ``` have "integrable M (\t. a * f t) \ (\ t. a * f t \M) = a * integral\<^sup>L M f" ``` hoelzl@50097 ` 1716` ``` proof (cases rule: le_cases) ``` hoelzl@50097 ` 1717` ``` assume "0 \ a" show ?thesis ``` hoelzl@50097 ` 1718` ``` using integral_linear[OF assms integral_zero(1) `0 \ a`] ``` hoelzl@50097 ` 1719` ``` by simp ``` hoelzl@50097 ` 1720` ``` next ``` hoelzl@50097 ` 1721` ``` assume "a \ 0" hence "0 \ - a" by auto ``` hoelzl@50097 ` 1722` ``` have *: "\t. - a * t + 0 = (-a) * t" by simp ``` hoelzl@50097 ` 1723` ``` show ?thesis using integral_linear[OF assms integral_zero(1) `0 \ - a`] ``` hoelzl@50097 ` 1724` ``` integral_minus(1)[of M "\t. - a * f t"] ``` hoelzl@50097 ` 1725` ``` unfolding * integral_zero by simp ``` hoelzl@50097 ` 1726` ``` qed ``` hoelzl@50097 ` 1727` ``` thus ?P ?I by auto ``` hoelzl@50097 ` 1728` ```qed ``` hoelzl@41096 ` 1729` hoelzl@47694 ` 1730` ```lemma integral_diff[simp, intro]: ``` hoelzl@41689 ` 1731` ``` assumes f: "integrable M f" and g: "integrable M g" ``` hoelzl@41689 ` 1732` ``` shows "integrable M (\t. f t - g t)" ``` wenzelm@53015 ` 1733` ``` and "(\ t. f t - g t \M) = integral\<^sup>L M f - integral\<^sup>L M g" ``` hoelzl@38656 ` 1734` ``` using integral_add[OF f integral_minus(1)[OF g]] ``` haftmann@54230 ` 1735` ``` unfolding integral_minus(2)[OF g] ``` hoelzl@38656 ` 1736` ``` by auto ``` hoelzl@38656 ` 1737` hoelzl@47694 ` 1738` ```lemma integral_indicator[simp, intro]: ``` hoelzl@47694 ` 1739` ``` assumes "A \ sets M" and "(emeasure M) A \ \" ``` wenzelm@53015 ` 1740` ``` shows "integral\<^sup>L M (indicator A) = real (emeasure M A)" (is ?int) ``` hoelzl@41981 ` 1741` ``` and "integrable M (indicator A)" (is ?able) ``` hoelzl@35582 ` 1742` ```proof - ``` hoelzl@41981 ` 1743` ``` from `A \ sets M` have *: ``` hoelzl@43920 ` 1744` ``` "\x. ereal (indicator A x) = indicator A x" ``` wenzelm@53015 ` 1745` ``` "(\\<^sup>+x. ereal (- indicator A x) \M) = 0" ``` hoelzl@43920 ` 1746` ``` by (auto split: split_indicator simp: positive_integral_0_iff_AE one_ereal_def) ``` hoelzl@38656 ` 1747` ``` show ?int ?able ``` hoelzl@41689 ` 1748` ``` using assms unfolding lebesgue_integral_def integrable_def ``` hoelzl@50002 ` 1749` ``` by (auto simp: *) ``` hoelzl@35582 ` 1750` ```qed ``` hoelzl@35582 ` 1751` hoelzl@47694 ` 1752` ```lemma integral_cmul_indicator: ``` hoelzl@47694 ` 1753` ``` assumes "A \ sets M" and "c \ 0 \ (emeasure M) A \ \" ``` hoelzl@41689 ` 1754` ``` shows "integrable M (\x. c * indicator A x)" (is ?P) ``` hoelzl@47694 ` 1755` ``` and "(\x. c * indicator A x \M) = c * real ((emeasure M) A)" (is ?I) ``` hoelzl@38656 ` 1756` ```proof - ``` hoelzl@38656 ` 1757` ``` show ?P ``` hoelzl@38656 ` 1758` ``` proof (cases "c = 0") ``` hoelzl@38656 ` 1759` ``` case False with assms show ?thesis by simp ``` hoelzl@38656 ` 1760` ``` qed simp ``` hoelzl@35582 ` 1761` hoelzl@38656 ` 1762` ``` show ?I ``` hoelzl@38656 ` 1763` ``` proof (cases "c = 0") ``` hoelzl@38656 ` 1764` ``` case False with assms show ?thesis by simp ``` hoelzl@38656 ` 1765` ``` qed simp ``` hoelzl@38656 ` 1766` ```qed ``` hoelzl@35582 ` 1767` hoelzl@47694 ` 1768` ```lemma integral_setsum[simp, intro]: ``` hoelzl@41689 ` 1769` ``` assumes "\n. n \ S \ integrable M (f n)" ``` wenzelm@53015 ` 1770` ``` shows "(\x. (\ i \ S. f i x) \M) = (\ i \ S. integral\<^sup>L M (f i))" (is "?int S") ``` hoelzl@41689 ` 1771` ``` and "integrable M (\x. \ i \ S. f i x)" (is "?I S") ``` hoelzl@35582 ` 1772` ```proof - ``` hoelzl@38656 ` 1773` ``` have "?int S \ ?I S" ``` hoelzl@38656 ` 1774` ``` proof (cases "finite S") ``` hoelzl@38656 ` 1775` ``` assume "finite S" ``` hoelzl@38656 ` 1776` ``` from this assms show ?thesis by (induct S) simp_all ``` hoelzl@38656 ` 1777` ``` qed simp ``` hoelzl@35582 ` 1778` ``` thus "?int S" and "?I S" by auto ``` hoelzl@35582 ` 1779` ```qed ``` hoelzl@35582 ` 1780` hoelzl@49775 ` 1781` ```lemma integrable_bound: ``` hoelzl@49775 ` 1782` ``` assumes "integrable M f" and f: "AE x in M. \g x\ \ f x" ``` hoelzl@49775 ` 1783` ``` assumes borel: "g \ borel_measurable M" ``` hoelzl@49775 ` 1784` ``` shows "integrable M g" ``` hoelzl@49775 ` 1785` ```proof - ``` wenzelm@53015 ` 1786` ``` have "(\\<^sup>+ x. ereal (g x) \M) \ (\\<^sup>+ x. ereal \g x\ \M)" ``` hoelzl@49775 ` 1787` ``` by (auto intro!: positive_integral_mono) ``` wenzelm@53015 ` 1788` ``` also have "\ \ (\\<^sup>+ x. ereal (f x) \M)" ``` hoelzl@49775 ` 1789` ``` using f by (auto intro!: positive_integral_mono_AE) ``` hoelzl@49775 ` 1790` ``` also have "\ < \" ``` hoelzl@49775 ` 1791` ``` using `integrable M f` unfolding integrable_def by auto ``` wenzelm@53015 ` 1792` ``` finally have pos: "(\\<^sup>+ x. ereal (g x) \M) < \" . ``` hoelzl@49775 ` 1793` wenzelm@53015 ` 1794` ``` have "(\\<^sup>+ x. ereal (- g x) \M) \ (\\<^sup>+ x. ereal (\g x\) \M)" ``` hoelzl@49775 ` 1795` ``` by (auto intro!: positive_integral_mono) ``` wenzelm@53015 ` 1796` ``` also have "\ \ (\\<^sup>+ x. ereal (f x) \M)" ``` hoelzl@49775 ` 1797` ``` using f by (auto intro!: positive_integral_mono_AE) ``` hoelzl@49775 ` 1798` ``` also have "\ < \" ``` hoelzl@49775 ` 1799` ``` using `integrable M f` unfolding integrable_def by auto ``` wenzelm@53015 ` 1800` ``` finally have neg: "(\\<^sup>+ x. ereal (- g x) \M) < \" . ``` hoelzl@49775 ` 1801` hoelzl@49775 ` 1802` ``` from neg pos borel show ?thesis ``` hoelzl@49775 ` 1803` ``` unfolding integrable_def by auto ``` hoelzl@49775 ` 1804` ```qed ``` hoelzl@49775 ` 1805` hoelzl@47694 ` 1806` ```lemma integrable_abs: ``` hoelzl@50003 ` 1807` ``` assumes f[measurable]: "integrable M f" ``` hoelzl@41689 ` 1808` ``` shows "integrable M (\ x. \f x\)" ``` hoelzl@36624 ` 1809` ```proof - ``` wenzelm@53015 ` 1810` ``` from assms have *: "(\\<^sup>+x. ereal (- \f x\)\M) = 0" ``` hoelzl@43920 ` 1811` ``` "\x. ereal \f x\ = max 0 (ereal (f x)) + max 0 (ereal (- f x))" ``` hoelzl@41981 ` 1812` ``` by (auto simp: integrable_def positive_integral_0_iff_AE split: split_max) ``` hoelzl@41981 ` 1813` ``` with assms show ?thesis ``` hoelzl@41981 ` 1814` ``` by (simp add: positive_integral_add positive_integral_max_0 integrable_def) ``` hoelzl@38656 ` 1815` ```qed ``` hoelzl@38656 ` 1816` hoelzl@47694 ` 1817` ```lemma integral_subalgebra: ``` hoelzl@41545 ` 1818` ``` assumes borel: "f \ borel_measurable N" ``` hoelzl@47694 ` 1819` ``` and N: "sets N \ sets M" "space N = space M" "\A. A \ sets N \ emeasure N A = emeasure M A" ``` hoelzl@41689 ` 1820` ``` shows "integrable N f \ integrable M f" (is ?P) ``` wenzelm@53015 ` 1821` ``` and "integral\<^sup>L N f = integral\<^sup>L M f" (is ?I) ``` hoelzl@41545 ` 1822` ```proof - ``` wenzelm@53015 ` 1823` ``` have "(\\<^sup>+ x. max 0 (ereal (f x)) \N) = (\\<^sup>+ x. max 0 (ereal (f x)) \M)" ``` wenzelm@53015 ` 1824` ``` "(\\<^sup>+ x. max 0 (ereal (- f x)) \N) = (\\<^sup>+ x. max 0 (ereal (- f x)) \M)" ``` hoelzl@47694 ` 1825` ``` using borel by (auto intro!: positive_integral_subalgebra N) ``` hoelzl@41981 ` 1826` ``` moreover have "f \ borel_measurable M \ f \ borel_measurable N" ``` hoelzl@41545 ` 1827` ``` using assms unfolding measurable_def by auto ``` hoelzl@41981 ` 1828` ``` ultimately show ?P ?I ``` hoelzl@41981 ` 1829` ``` by (auto simp: integrable_def lebesgue_integral_def positive_integral_max_0) ``` hoelzl@41545 ` 1830` ```qed ``` hoelzl@41545 ` 1831` hoelzl@47694 ` 1832` ```lemma lebesgue_integral_nonneg: ``` wenzelm@53015 ` 1833` ``` assumes ae: "(AE x in M. 0 \ f x)" shows "0 \ integral\<^sup>L M f" ``` hoelzl@47694 ` 1834` ```proof - ``` wenzelm@53015 ` 1835` ``` have "(\\<^sup>+x. max 0 (ereal (- f x)) \M) = (\\<^sup>+x. 0 \M)" ``` hoelzl@47694 ` 1836` ``` using ae by (intro positive_integral_cong_AE) (auto simp: max_def) ``` hoelzl@47694 ` 1837` ``` then show ?thesis ``` hoelzl@47694 ` 1838` ``` by (auto simp: lebesgue_integral_def positive_integral_max_0 ``` hoelzl@47694 ` 1839` ``` intro!: real_of_ereal_pos positive_integral_positive) ``` hoelzl@47694 ` 1840` ```qed ``` hoelzl@47694 ` 1841` hoelzl@47694 ` 1842` ```lemma integrable_abs_iff: ``` hoelzl@41689 ` 1843` ``` "f \ borel_measurable M \ integrable M (\ x. \f x\) \ integrable M f" ``` hoelzl@38656 ` 1844` ``` by (auto intro!: integrable_bound[where g=f] integrable_abs) ``` hoelzl@38656 ` 1845` hoelzl@47694 ` 1846` ```lemma integrable_max: ``` hoelzl@41689 ` 1847` ``` assumes int: "integrable M f" "integrable M g" ``` hoelzl@41689 ` 1848` ``` shows "integrable M (\ x. max (f x) (g x))" ``` hoelzl@38656 ` 1849` ```proof (rule integrable_bound) ``` hoelzl@41689 ` 1850` ``` show "integrable M (\x. \f x\ + \g x\)" ``` hoelzl@38656 ` 1851` ``` using int by (simp add: integrable_abs) ``` hoelzl@38656 ` 1852` ``` show "(\x. max (f x) (g x)) \ borel_measurable M" ``` hoelzl@38656 ` 1853` ``` using int unfolding integrable_def by auto ``` hoelzl@49775 ` 1854` ```qed auto ``` hoelzl@38656 ` 1855` hoelzl@47694 ` 1856` ```lemma integrable_min: ``` hoelzl@41689 ` 1857` ``` assumes int: "integrable M f" "integrable M g" ``` hoelzl@41689 ` 1858` ``` shows "integrable M (\ x. min (f x) (g x))" ``` hoelzl@38656 ` 1859` ```proof (rule integrable_bound) ``` hoelzl@41689 ` 1860` ``` show "integrable M (\x. \f x\ + \g x\)" ``` hoelzl@38656 ` 1861` ``` using int by (simp add: integrable_abs) ``` hoelzl@38656 ` 1862` ``` show "(\x. min (f x) (g x)) \ borel_measurable M" ``` hoelzl@38656 ` 1863` ``` using int unfolding integrable_def by auto ``` hoelzl@49775 ` 1864` ```qed auto ``` hoelzl@38656 ` 1865` hoelzl@47694 ` 1866` ```lemma integral_triangle_inequality: ``` hoelzl@41689 ` 1867` ``` assumes "integrable M f" ``` wenzelm@53015 ` 1868` ``` shows "\integral\<^sup>L M f\ \ (\x. \f x\ \M)" ``` hoelzl@38656 ` 1869` ```proof - ``` wenzelm@53015 ` 1870` ``` have "\integral\<^sup>L M f\ = max (integral\<^sup>L M f) (- integral\<^sup>L M f)" by auto ``` hoelzl@41689 ` 1871` ``` also have "\ \ (\x. \f x\ \M)" ``` hoelzl@47694 ` 1872` ``` using assms integral_minus(2)[of M f, symmetric] ``` hoelzl@38656 ` 1873` ``` by (auto intro!: integral_mono integrable_abs simp del: integral_minus) ``` hoelzl@38656 ` 1874` ``` finally show ?thesis . ``` hoelzl@36624 ` 1875` ```qed ``` hoelzl@36624 ` 1876` hoelzl@50097 ` 1877` ```lemma integrable_nonneg: ``` wenzelm@53015 ` 1878` ``` assumes f: "f \ borel_measurable M" "AE x in M. 0 \ f x" "(\\<^sup>+ x. f x \M) \ \" ``` hoelzl@50097 ` 1879` ``` shows "integrable M f" ``` hoelzl@50097 ` 1880` ``` unfolding integrable_def ``` hoelzl@50097 ` 1881` ```proof (intro conjI f) ``` wenzelm@53015 ` 1882` ``` have "(\\<^sup>+ x. ereal (- f x) \M) = 0" ``` hoelzl@50097 ` 1883` ``` using f by (subst positive_integral_0_iff_AE) auto ``` wenzelm@53015 ` 1884` ``` then show "(\\<^sup>+ x. ereal (- f x) \M) \ \" by simp ``` hoelzl@50097 ` 1885` ```qed ``` hoelzl@50097 ` 1886` hoelzl@47694 ` 1887` ```lemma integral_positive: ``` hoelzl@41689 ` 1888` ``` assumes "integrable M f" "\x. x \ space M \ 0 \ f x" ``` wenzelm@53015 ` 1889` ``` shows "0 \ integral\<^sup>L M f" ``` hoelzl@38656 ` 1890` ```proof - ``` hoelzl@50002 ` 1891` ``` have "0 = (\x. 0 \M)" by auto ``` wenzelm@53015 ` 1892` ``` also have "\ \ integral\<^sup>L M f" ``` hoelzl@38656 ` 1893` ``` using assms by (rule integral_mono[OF integral_zero(1)]) ``` hoelzl@38656 ` 1894` ``` finally show ?thesis . ``` hoelzl@38656 ` 1895` ```qed ``` hoelzl@38656 ` 1896` hoelzl@47694 ` 1897` ```lemma integral_monotone_convergence_pos: ``` hoelzl@49775 ` 1898` ``` assumes i: "\i. integrable M (f i)" and mono: "AE x in M. mono (\n. f n x)" ``` hoelzl@49775 ` 1899` ``` and pos: "\i. AE x in M. 0 \ f i x" ``` hoelzl@49775 ` 1900` ``` and lim: "AE x in M. (\i. f i x) ----> u x" ``` wenzelm@53015 ` 1901` ``` and ilim: "(\i. integral\<^sup>L M (f i)) ----> x" ``` hoelzl@49775 ` 1902` ``` and u: "u \ borel_measurable M" ``` hoelzl@41689 ` 1903` ``` shows "integrable M u" ``` wenzelm@53015 ` 1904` ``` and "integral\<^sup>L M u = x" ``` hoelzl@35582 ` 1905` ```proof - ``` wenzelm@53015 ` 1906` ``` have "(\\<^sup>+ x. ereal (u x) \M) = (SUP n. (\\<^sup>+ x. ereal (f n x) \M))" ``` hoelzl@49775 ` 1907` ``` proof (subst positive_integral_monotone_convergence_SUP_AE[symmetric]) ``` hoelzl@49775 ` 1908` ``` fix i ``` hoelzl@49775 ` 1909` ``` from mono pos show "AE x in M. ereal (f i x) \ ereal (f (Suc i) x) \ 0 \ ereal (f i x)" ``` hoelzl@49775 ` 1910` ``` by eventually_elim (auto simp: mono_def) ``` hoelzl@49775 ` 1911` ``` show "(\x. ereal (f i x)) \ borel_measurable M" ``` hoelzl@50003 ` 1912` ``` using i by auto ``` hoelzl@49775 ` 1913` ``` next ``` wenzelm@53015 ` 1914` ``` show "(\\<^sup>+ x. ereal (u x) \M) = \\<^sup>+ x. (SUP i. ereal (f i x)) \M" ``` hoelzl@49775 ` 1915` ``` apply (rule positive_integral_cong_AE) ``` hoelzl@49775 ` 1916` ``` using lim mono ``` hoelzl@49775 ` 1917` ``` by eventually_elim (simp add: SUP_eq_LIMSEQ[THEN iffD2]) ``` hoelzl@38656 ` 1918` ``` qed ``` hoelzl@49775 ` 1919` ``` also have "\ = ereal x" ``` hoelzl@49775 ` 1920` ``` using mono i unfolding positive_integral_eq_integral[OF i pos] ``` hoelzl@49775 ` 1921` ``` by (subst SUP_eq_LIMSEQ) (auto simp: mono_def intro!: integral_mono_AE ilim) ``` wenzelm@53015 ` 1922` ``` finally have "(\\<^sup>+ x. ereal (u x) \M) = ereal x" . ``` wenzelm@53015 ` 1923` ``` moreover have "(\\<^sup>+ x. ereal (- u x) \M) = 0" ``` hoelzl@49775 ` 1924` ``` proof (subst positive_integral_0_iff_AE) ``` hoelzl@49775 ` 1925` ``` show "(\x. ereal (- u x)) \ borel_measurable M" ``` hoelzl@49775 ` 1926` ``` using u by auto ``` hoelzl@49775 ` 1927` ``` from mono pos[of 0] lim show "AE x in M. ereal (- u x) \ 0" ``` hoelzl@49775 ` 1928` ``` proof eventually_elim ``` hoelzl@49775 ` 1929` ``` fix x assume "mono (\n. f n x)" "0 \ f 0 x" "(\i. f i x) ----> u x" ``` hoelzl@49775 ` 1930` ``` then show "ereal (- u x) \ 0" ``` hoelzl@49775 ` 1931` ``` using incseq_le[of "\n. f n x" "u x" 0] by (simp add: mono_def incseq_def) ``` hoelzl@49775 ` 1932` ``` qed ``` hoelzl@49775 ` 1933` ``` qed ``` wenzelm@53015 ` 1934` ``` ultimately show "integrable M u" "integral\<^sup>L M u = x" ``` hoelzl@49775 ` 1935` ``` by (auto simp: integrable_def lebesgue_integral_def u) ``` hoelzl@38656 ` 1936` ```qed ``` hoelzl@38656 ` 1937` hoelzl@47694 ` 1938` ```lemma integral_monotone_convergence: ``` hoelzl@49775 ` 1939` ``` assumes f: "\i. integrable M (f i)" and mono: "AE x in M. mono (\n. f n x)" ``` hoelzl@49775 ` 1940` ``` and lim: "AE x in M. (\i. f i x) ----> u x" ``` wenzelm@53015 ` 1941` ``` and ilim: "(\i. integral\<^sup>L M (f i)) ----> x" ``` hoelzl@49775 ` 1942` ``` and u: "u \ borel_measurable M" ``` hoelzl@41689 ` 1943` ``` shows "integrable M u" ``` wenzelm@53015 ` 1944` ``` and "integral\<^sup>L M u = x" ``` hoelzl@38656 ` 1945` ```proof - ``` hoelzl@41689 ` 1946` ``` have 1: "\i. integrable M (\x. f i x - f 0 x)" ``` hoelzl@49775 ` 1947` ``` using f by auto ``` hoelzl@49775 ` 1948` ``` have 2: "AE x in M. mono (\n. f n x - f 0 x)" ``` hoelzl@49775 ` 1949` ``` using mono by (auto simp: mono_def le_fun_def) ``` hoelzl@49775 ` 1950` ``` have 3: "\n. AE x in M. 0 \ f n x - f 0 x" ``` hoelzl@49775 ` 1951` ``` using mono by (auto simp: field_simps mono_def le_fun_def) ``` hoelzl@49775 ` 1952` ``` have 4: "AE x in M. (\i. f i x - f 0 x) ----> u x - f 0 x" ``` huffman@44568 ` 1953` ``` using lim by (auto intro!: tendsto_diff) ``` wenzelm@53015 ` 1954` ``` have 5: "(\i. (\x. f i x - f 0 x \M)) ----> x - integral\<^sup>L M (f 0)" ``` hoelzl@49775 ` 1955` ``` using f ilim by (auto intro!: tendsto_diff) ``` hoelzl@49775 ` 1956` ``` have 6: "(\x. u x - f 0 x) \ borel_measurable M" ``` hoelzl@49775 ` 1957` ``` using f[of 0] u by auto ``` hoelzl@49775 ` 1958` ``` note diff = integral_monotone_convergence_pos[OF 1 2 3 4 5 6] ``` hoelzl@41689 ` 1959` ``` have "integrable M (\x. (u x - f 0 x) + f 0 x)" ``` hoelzl@38656 ` 1960` ``` using diff(1) f by (rule integral_add(1)) ``` wenzelm@53015 ` 1961` ``` with diff(2) f show "integrable M u" "integral\<^sup>L M u = x" ``` hoelzl@49775 ` 1962` ``` by auto ``` hoelzl@38656 ` 1963` ```qed ``` hoelzl@38656 ` 1964` hoelzl@47694 ` 1965` ```lemma integral_0_iff: ``` hoelzl@41689 ` 1966` ``` assumes "integrable M f" ``` hoelzl@47694 ` 1967` ``` shows "(\x. \f x\ \M) = 0 \ (emeasure M) {x\space M. f x \ 0} = 0" ``` hoelzl@38656 ` 1968` ```proof - ``` wenzelm@53015 ` 1969` ``` have *: "(\\<^sup>+x. ereal (- \f x\) \M) = 0" ``` hoelzl@41981 ` 1970` ``` using assms by (auto simp: positive_integral_0_iff_AE integrable_def) ``` hoelzl@41689 ` 1971` ``` have "integrable M (\x. \f x\)" using assms by (rule integrable_abs) ``` hoelzl@43920 ` 1972` ``` hence "(\x. ereal (\f x\)) \ borel_measurable M" ``` wenzelm@53015 ` 1973` ``` "(\\<^sup>+ x. ereal \f x\ \M) \ \" unfolding integrable_def by auto ``` hoelzl@38656 ` 1974` ``` from positive_integral_0_iff[OF this(1)] this(2) ``` hoelzl@41689 ` 1975` ``` show ?thesis unfolding lebesgue_integral_def * ``` hoelzl@47694 ` 1976` ``` using positive_integral_positive[of M "\x. ereal \f x\"] ``` hoelzl@43920 ` 1977` ``` by (auto simp add: real_of_ereal_eq_0) ``` hoelzl@35582 ` 1978` ```qed ``` hoelzl@35582 ` 1979`</