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