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