(* Author: Armin Heller, Johannes Hoelzl, TU Muenchen *) header {*Lebesgue Integration*} theory Lebesgue_Integration imports Measure Borel_Space begin lemma sums_If_finite: assumes finite: "finite {r. P r}" shows "(\r. if P r then f r else 0) sums (\r\{r. P r}. f r)" (is "?F sums _") proof cases assume "{r. P r} = {}" hence "\r. \ P r" by auto thus ?thesis by (simp add: sums_zero) next assume not_empty: "{r. P r} \ {}" have "?F sums (\r = 0..< Suc (Max {r. P r}). ?F r)" by (rule series_zero) (auto simp add: Max_less_iff[OF finite not_empty] less_eq_Suc_le[symmetric]) also have "(\r = 0..< Suc (Max {r. P r}). ?F r) = (\r\{r. P r}. f r)" by (subst setsum_cases) (auto intro!: setsum_cong simp: Max_ge_iff[OF finite not_empty] less_Suc_eq_le) finally show ?thesis . qed lemma sums_single: "(\r. if r = i then f r else 0) sums f i" using sums_If_finite[of "\r. r = i" f] by simp section "Simple function" text {* Our simple functions are not restricted to positive real numbers. Instead they are just functions with a finite range and are measurable when singleton sets are measurable. *} definition (in sigma_algebra) "simple_function g \ finite (g ` space M) \ (\x \ g ` space M. g -` {x} \ space M \ sets M)" lemma (in sigma_algebra) simple_functionD: assumes "simple_function g" shows "finite (g ` space M)" and "g -` X \ space M \ sets M" proof - show "finite (g ` space M)" using assms unfolding simple_function_def by auto have "g -` X \ space M = g -` (X \ g`space M) \ space M" by auto also have "\ = (\x\X \ g`space M. g-`{x} \ space M)" by auto finally show "g -` X \ space M \ sets M" using assms by (auto intro!: finite_UN simp del: UN_simps simp: simple_function_def) qed lemma (in sigma_algebra) simple_function_indicator_representation: fixes f ::"'a \ pinfreal" assumes f: "simple_function f" and x: "x \ space M" shows "f x = (\y \ f ` space M. y * indicator (f -` {y} \ space M) x)" (is "?l = ?r") proof - have "?r = (\y \ f ` space M. (if y = f x then y * indicator (f -` {y} \ space M) x else 0))" by (auto intro!: setsum_cong2) also have "... = f x * indicator (f -` {f x} \ space M) x" using assms by (auto dest: simple_functionD simp: setsum_delta) also have "... = f x" using x by (auto simp: indicator_def) finally show ?thesis by auto qed lemma (in measure_space) simple_function_notspace: "simple_function (\x. h x * indicator (- space M) x::pinfreal)" (is "simple_function ?h") proof - have "?h ` space M \ {0}" unfolding indicator_def by auto hence [simp, intro]: "finite (?h ` space M)" by (auto intro: finite_subset) have "?h -` {0} \ space M = space M" by auto thus ?thesis unfolding simple_function_def by auto qed lemma (in sigma_algebra) simple_function_cong: assumes "\t. t \ space M \ f t = g t" shows "simple_function f \ simple_function g" proof - have "f ` space M = g ` space M" "\x. f -` {x} \ space M = g -` {x} \ space M" using assms by (auto intro!: image_eqI) thus ?thesis unfolding simple_function_def using assms by simp qed lemma (in sigma_algebra) borel_measurable_simple_function: assumes "simple_function f" shows "f \ borel_measurable M" proof (rule borel_measurableI) fix S let ?I = "f ` (f -` S \ space M)" have *: "(\x\?I. f -` {x} \ space M) = f -` S \ space M" (is "?U = _") by auto have "finite ?I" using assms unfolding simple_function_def by (auto intro: finite_subset) hence "?U \ sets M" apply (rule finite_UN) using assms unfolding simple_function_def by auto thus "f -` S \ space M \ sets M" unfolding * . qed lemma (in sigma_algebra) simple_function_borel_measurable: fixes f :: "'a \ 'x::t2_space" assumes "f \ borel_measurable M" and "finite (f ` space M)" shows "simple_function f" using assms unfolding simple_function_def by (auto intro: borel_measurable_vimage) lemma (in sigma_algebra) simple_function_const[intro, simp]: "simple_function (\x. c)" by (auto intro: finite_subset simp: simple_function_def) lemma (in sigma_algebra) simple_function_compose[intro, simp]: assumes "simple_function f" shows "simple_function (g \ f)" unfolding simple_function_def proof safe show "finite ((g \ f) ` space M)" using assms unfolding simple_function_def by (auto simp: image_compose) next fix x assume "x \ space M" let ?G = "g -` {g (f x)} \ (f`space M)" have *: "(g \ f) -` {(g \ f) x} \ space M = (\x\?G. f -` {x} \ space M)" by auto show "(g \ f) -` {(g \ f) x} \ space M \ sets M" using assms unfolding simple_function_def * by (rule_tac finite_UN) (auto intro!: finite_UN) qed lemma (in sigma_algebra) simple_function_indicator[intro, simp]: assumes "A \ sets M" shows "simple_function (indicator A)" proof - have "indicator A ` space M \ {0, 1}" (is "?S \ _") by (auto simp: indicator_def) hence "finite ?S" by (rule finite_subset) simp moreover have "- A \ space M = space M - A" by auto ultimately show ?thesis unfolding simple_function_def using assms by (auto simp: indicator_def_raw) qed lemma (in sigma_algebra) simple_function_Pair[intro, simp]: assumes "simple_function f" assumes "simple_function g" shows "simple_function (\x. (f x, g x))" (is "simple_function ?p") unfolding simple_function_def proof safe show "finite (?p ` space M)" using assms unfolding simple_function_def by (rule_tac finite_subset[of _ "f`space M \ g`space M"]) auto next fix x assume "x \ space M" have "(\x. (f x, g x)) -` {(f x, g x)} \ space M = (f -` {f x} \ space M) \ (g -` {g x} \ space M)" by auto with `x \ space M` show "(\x. (f x, g x)) -` {(f x, g x)} \ space M \ sets M" using assms unfolding simple_function_def by auto qed lemma (in sigma_algebra) simple_function_compose1: assumes "simple_function f" shows "simple_function (\x. g (f x))" using simple_function_compose[OF assms, of g] by (simp add: comp_def) lemma (in sigma_algebra) simple_function_compose2: assumes "simple_function f" and "simple_function g" shows "simple_function (\x. h (f x) (g x))" proof - have "simple_function ((\(x, y). h x y) \ (\x. (f x, g x)))" using assms by auto thus ?thesis by (simp_all add: comp_def) qed lemmas (in sigma_algebra) simple_function_add[intro, simp] = simple_function_compose2[where h="op +"] and simple_function_diff[intro, simp] = simple_function_compose2[where h="op -"] and simple_function_uminus[intro, simp] = simple_function_compose[where g="uminus"] and simple_function_mult[intro, simp] = simple_function_compose2[where h="op *"] and simple_function_div[intro, simp] = simple_function_compose2[where h="op /"] and simple_function_inverse[intro, simp] = simple_function_compose[where g="inverse"] lemma (in sigma_algebra) simple_function_setsum[intro, simp]: assumes "\i. i \ P \ simple_function (f i)" shows "simple_function (\x. \i\P. f i x)" proof cases assume "finite P" from this assms show ?thesis by induct auto qed auto lemma (in sigma_algebra) simple_function_le_measurable: assumes "simple_function f" "simple_function g" shows "{x \ space M. f x \ g x} \ sets M" proof - have *: "{x \ space M. f x \ g x} = (\(F, G)\f`space M \ g`space M. if F \ G then (f -` {F} \ space M) \ (g -` {G} \ space M) else {})" apply (auto split: split_if_asm) apply (rule_tac x=x in bexI) apply (rule_tac x=x in bexI) by simp_all have **: "\x y. x \ space M \ y \ space M \ (f -` {f x} \ space M) \ (g -` {g y} \ space M) \ sets M" using assms unfolding simple_function_def by auto have "finite (f`space M \ g`space M)" using assms unfolding simple_function_def by auto thus ?thesis unfolding * apply (rule finite_UN) using assms unfolding simple_function_def by (auto intro!: **) qed lemma (in sigma_algebra) borel_measurable_implies_simple_function_sequence: fixes u :: "'a \ pinfreal" assumes u: "u \ borel_measurable M" shows "\f. (\i. simple_function (f i) \ (\x\space M. f i x \ \)) \ f \ u" proof - have "\f. \x j. (of_nat j \ u x \ f x j = j*2^j) \ (u x < of_nat j \ of_nat (f x j) \ u x * 2^j \ u x * 2^j < of_nat (Suc (f x j)))" (is "\f. \x j. ?P x j (f x j)") proof(rule choice, rule, rule choice, rule) fix x j show "\n. ?P x j n" proof cases assume *: "u x < of_nat j" then obtain r where r: "u x = Real r" "0 \ r" by (cases "u x") auto from reals_Archimedean6a[of "r * 2^j"] obtain n :: nat where "real n \ r * 2 ^ j" "r * 2 ^ j < real (Suc n)" using `0 \ r` by (auto simp: zero_le_power zero_le_mult_iff) thus ?thesis using r * by (auto intro!: exI[of _ n]) qed auto qed then obtain f where top: "\j x. of_nat j \ u x \ f x j = j*2^j" and upper: "\j x. u x < of_nat j \ of_nat (f x j) \ u x * 2^j" and lower: "\j x. u x < of_nat j \ u x * 2^j < of_nat (Suc (f x j))" by blast { fix j x P assume 1: "of_nat j \ u x \ P (j * 2^j)" assume 2: "\k. \ u x < of_nat j ; of_nat k \ u x * 2^j ; u x * 2^j < of_nat (Suc k) \ \ P k" have "P (f x j)" proof cases assume "of_nat j \ u x" thus "P (f x j)" using top[of j x] 1 by auto next assume "\ of_nat j \ u x" hence "u x < of_nat j" "of_nat (f x j) \ u x * 2^j" "u x * 2^j < of_nat (Suc (f x j))" using upper lower by auto from 2[OF this] show "P (f x j)" . qed } note fI = this { fix j x have "f x j = j * 2 ^ j \ of_nat j \ u x" by (rule fI, simp, cases "u x") (auto split: split_if_asm) } note f_eq = this { fix j x have "f x j \ j * 2 ^ j" proof (rule fI) fix k assume *: "u x < of_nat j" assume "of_nat k \ u x * 2 ^ j" also have "\ \ of_nat (j * 2^j)" using * by (cases "u x") (auto simp: zero_le_mult_iff) finally show "k \ j*2^j" by (auto simp del: real_of_nat_mult) qed simp } note f_upper = this let "?g j x" = "of_nat (f x j) / 2^j :: pinfreal" show ?thesis unfolding simple_function_def isoton_fun_expand unfolding isoton_def proof (safe intro!: exI[of _ ?g]) fix j have *: "?g j ` space M \ (\x. of_nat x / 2^j) ` {..j * 2^j}" using f_upper by auto thus "finite (?g j ` space M)" by (rule finite_subset) auto next fix j t assume "t \ space M" have **: "?g j -` {?g j t} \ space M = {x \ space M. f t j = f x j}" by (auto simp: power_le_zero_eq Real_eq_Real mult_le_0_iff) show "?g j -` {?g j t} \ space M \ sets M" proof cases assume "of_nat j \ u t" hence "?g j -` {?g j t} \ space M = {x\space M. of_nat j \ u x}" unfolding ** f_eq[symmetric] by auto thus "?g j -` {?g j t} \ space M \ sets M" using u by auto next assume not_t: "\ of_nat j \ u t" hence less: "f t j < j*2^j" using f_eq[symmetric] `f t j \ j*2^j` by auto have split_vimage: "?g j -` {?g j t} \ space M = {x\space M. of_nat (f t j)/2^j \ u x} \ {x\space M. u x < of_nat (Suc (f t j))/2^j}" unfolding ** proof safe fix x assume [simp]: "f t j = f x j" have *: "\ of_nat j \ u x" using not_t f_eq[symmetric] by simp hence "of_nat (f t j) \ u x * 2^j \ u x * 2^j < of_nat (Suc (f t j))" using upper lower by auto hence "of_nat (f t j) / 2^j \ u x \ u x < of_nat (Suc (f t j))/2^j" using * by (cases "u x") (auto simp: zero_le_mult_iff power_le_zero_eq divide_real_def[symmetric] field_simps) thus "of_nat (f t j) / 2^j \ u x" "u x < of_nat (Suc (f t j))/2^j" by auto next fix x assume "of_nat (f t j) / 2^j \ u x" "u x < of_nat (Suc (f t j))/2^j" hence "of_nat (f t j) \ u x * 2 ^ j \ u x * 2 ^ j < of_nat (Suc (f t j))" by (cases "u x") (auto simp: zero_le_mult_iff power_le_zero_eq divide_real_def[symmetric] field_simps) hence 1: "of_nat (f t j) \ u x * 2 ^ j" and 2: "u x * 2 ^ j < of_nat (Suc (f t j))" by auto note 2 also have "\ \ of_nat (j*2^j)" using less by (auto simp: zero_le_mult_iff simp del: real_of_nat_mult) finally have bound_ux: "u x < of_nat j" by (cases "u x") (auto simp: zero_le_mult_iff power_le_zero_eq) show "f t j = f x j" proof (rule antisym) from 1 lower[OF bound_ux] show "f t j \ f x j" by (cases "u x") (auto split: split_if_asm) from upper[OF bound_ux] 2 show "f x j \ f t j" by (cases "u x") (auto split: split_if_asm) qed qed show ?thesis unfolding split_vimage using u by auto qed next fix j t assume "?g j t = \" thus False by (auto simp: power_le_zero_eq) next fix t { fix i have "f t i * 2 \ f t (Suc i)" proof (rule fI) assume "of_nat (Suc i) \ u t" hence "of_nat i \ u t" by (cases "u t") auto thus "f t i * 2 \ Suc i * 2 ^ Suc i" unfolding f_eq[symmetric] by simp next fix k assume *: "u t * 2 ^ Suc i < of_nat (Suc k)" show "f t i * 2 \ k" proof (rule fI) assume "of_nat i \ u t" hence "of_nat (i * 2^Suc i) \ u t * 2^Suc i" by (cases "u t") (auto simp: zero_le_mult_iff power_le_zero_eq) also have "\ < of_nat (Suc k)" using * by auto finally show "i * 2 ^ i * 2 \ k" by (auto simp del: real_of_nat_mult) next fix j assume "of_nat j \ u t * 2 ^ i" with * show "j * 2 \ k" by (cases "u t") (auto simp: zero_le_mult_iff power_le_zero_eq) qed qed thus "?g i t \ ?g (Suc i) t" by (auto simp: zero_le_mult_iff power_le_zero_eq divide_real_def[symmetric] field_simps) } hence mono: "mono (\i. ?g i t)" unfolding mono_iff_le_Suc by auto show "(SUP j. of_nat (f t j) / 2 ^ j) = u t" proof (rule pinfreal_SUPI) fix j show "of_nat (f t j) / 2 ^ j \ u t" proof (rule fI) assume "of_nat j \ u t" thus "of_nat (j * 2 ^ j) / 2 ^ j \ u t" by (cases "u t") (auto simp: power_le_zero_eq divide_real_def[symmetric] field_simps) next fix k assume "of_nat k \ u t * 2 ^ j" thus "of_nat k / 2 ^ j \ u t" by (cases "u t") (auto simp: power_le_zero_eq divide_real_def[symmetric] field_simps zero_le_mult_iff) qed next fix y :: pinfreal assume *: "\j. j \ UNIV \ of_nat (f t j) / 2 ^ j \ y" show "u t \ y" proof (cases "u t") case (preal r) show ?thesis proof (rule ccontr) assume "\ u t \ y" then obtain p where p: "y = Real p" "0 \ p" "p < r" using preal by (cases y) auto with LIMSEQ_inverse_realpow_zero[of 2, unfolded LIMSEQ_iff, rule_format, of "r - p"] obtain n where n: "\N. n \ N \ inverse (2^N) < r - p" by auto let ?N = "max n (natfloor r + 1)" have "u t < of_nat ?N" "n \ ?N" using ge_natfloor_plus_one_imp_gt[of r n] preal using real_natfloor_add_one_gt by (auto simp: max_def real_of_nat_Suc) from lower[OF this(1)] have "r < (real (f t ?N) + 1) / 2 ^ ?N" unfolding less_divide_eq using preal by (auto simp add: power_le_zero_eq zero_le_mult_iff real_of_nat_Suc split: split_if_asm) hence "u t < of_nat (f t ?N) / 2 ^ ?N + 1 / 2 ^ ?N" using preal by (auto simp: field_simps divide_real_def[symmetric]) with n[OF `n \ ?N`] p preal *[of ?N] show False by (cases "f t ?N") (auto simp: power_le_zero_eq split: split_if_asm) qed next case infinite { fix j have "f t j = j*2^j" using top[of j t] infinite by simp hence "of_nat j \ y" using *[of j] by (cases y) (auto simp: power_le_zero_eq zero_le_mult_iff field_simps) } note all_less_y = this show ?thesis unfolding infinite proof (rule ccontr) assume "\ \ \ y" then obtain r where r: "y = Real r" "0 \ r" by (cases y) auto moreover obtain n ::nat where "r < real n" using ex_less_of_nat by (auto simp: real_eq_of_nat) with all_less_y[of n] r show False by auto qed qed qed qed qed lemma (in sigma_algebra) borel_measurable_implies_simple_function_sequence': fixes u :: "'a \ pinfreal" assumes "u \ borel_measurable M" obtains (x) f where "f \ u" "\i. simple_function (f i)" "\i. \\f i`space M" proof - from borel_measurable_implies_simple_function_sequence[OF assms] obtain f where x: "\i. simple_function (f i)" "f \ u" and fin: "\i. \x. x\space M \ f i x \ \" by auto { fix i from fin[of _ i] have "\ \ f i`space M" by fastsimp } with x show thesis by (auto intro!: that[of f]) qed lemma (in sigma_algebra) simple_function_eq_borel_measurable: fixes f :: "'a \ pinfreal" shows "simple_function f \ finite (f`space M) \ f \ borel_measurable M" using simple_function_borel_measurable[of f] borel_measurable_simple_function[of f] by (fastsimp simp: simple_function_def) lemma (in measure_space) simple_function_restricted: fixes f :: "'a \ pinfreal" assumes "A \ sets M" shows "sigma_algebra.simple_function (restricted_space A) f \ simple_function (\x. f x * indicator A x)" (is "sigma_algebra.simple_function ?R f \ simple_function ?f") proof - interpret R: sigma_algebra ?R by (rule restricted_sigma_algebra[OF `A \ sets M`]) have "finite (f`A) \ finite (?f`space M)" proof cases assume "A = space M" then have "f`A = ?f`space M" by (fastsimp simp: image_iff) then show ?thesis by simp next assume "A \ space M" then obtain x where x: "x \ space M" "x \ A" using sets_into_space `A \ sets M` by auto have *: "?f`space M = f`A \ {0}" proof (auto simp add: image_iff) show "\x\space M. f x = 0 \ indicator A x = 0" using x by (auto intro!: bexI[of _ x]) next fix x assume "x \ A" then show "\y\space M. f x = f y * indicator A y" using `A \ sets M` sets_into_space by (auto intro!: bexI[of _ x]) next fix x assume "indicator A x \ (0::pinfreal)" then have "x \ A" by (auto simp: indicator_def split: split_if_asm) moreover assume "x \ space M" "\y\A. ?f x \ f y" ultimately show "f x = 0" by auto qed then show ?thesis by auto qed then show ?thesis unfolding simple_function_eq_borel_measurable R.simple_function_eq_borel_measurable unfolding borel_measurable_restricted[OF `A \ sets M`] by auto qed lemma (in sigma_algebra) simple_function_subalgebra: assumes "sigma_algebra.simple_function (M\sets:=N\) f" and N_subalgebra: "N \ sets M" "sigma_algebra (M\sets:=N\)" shows "simple_function f" using assms unfolding simple_function_def unfolding sigma_algebra.simple_function_def[OF N_subalgebra(2)] by auto lemma (in sigma_algebra) simple_function_vimage: fixes g :: "'a \ pinfreal" and f :: "'d \ 'a" assumes g: "simple_function g" and f: "f \ S \ space M" shows "sigma_algebra.simple_function (vimage_algebra S f) (\x. g (f x))" proof - have subset: "(\x. g (f x)) ` S \ g ` space M" using f by auto interpret V: sigma_algebra "vimage_algebra S f" using f by (rule sigma_algebra_vimage) show ?thesis using g unfolding simple_function_eq_borel_measurable unfolding V.simple_function_eq_borel_measurable using measurable_vimage[OF _ f, of g borel] using finite_subset[OF subset] by auto qed section "Simple integral" definition (in measure_space) "simple_integral f = (\x \ f ` space M. x * \ (f -` {x} \ space M))" lemma (in measure_space) simple_integral_cong: assumes "\t. t \ space M \ f t = g t" shows "simple_integral f = simple_integral g" proof - have "f ` space M = g ` space M" "\x. f -` {x} \ space M = g -` {x} \ space M" using assms by (auto intro!: image_eqI) thus ?thesis unfolding simple_integral_def by simp qed lemma (in measure_space) simple_integral_cong_measure: assumes "\A. A \ sets M \ \ A = \ A" and "simple_function f" shows "measure_space.simple_integral M \ f = simple_integral f" proof - interpret v: measure_space M \ by (rule measure_space_cong) fact from simple_functionD[OF `simple_function f`] assms show ?thesis unfolding simple_integral_def v.simple_integral_def by (auto intro!: setsum_cong) qed lemma (in measure_space) simple_integral_const[simp]: "simple_integral (\x. c) = c * \ (space M)" proof (cases "space M = {}") case True thus ?thesis unfolding simple_integral_def by simp next case False hence "(\x. c) ` space M = {c}" by auto thus ?thesis unfolding simple_integral_def by simp qed lemma (in measure_space) simple_function_partition: assumes "simple_function f" and "simple_function g" shows "simple_integral f = (\A\(\x. f -` {f x} \ g -` {g x} \ space M) ` space M. the_elem (f`A) * \ A)" (is "_ = setsum _ (?p ` space M)") proof- let "?sub x" = "?p ` (f -` {x} \ space M)" let ?SIGMA = "Sigma (f`space M) ?sub" have [intro]: "finite (f ` space M)" "finite (g ` space M)" using assms unfolding simple_function_def by simp_all { fix A have "?p ` (A \ space M) \ (\(x,y). f -` {x} \ g -` {y} \ space M) ` (f`space M \ g`space M)" by auto hence "finite (?p ` (A \ space M))" by (rule finite_subset) auto } note this[intro, simp] { fix x assume "x \ space M" have "\(?sub (f x)) = (f -` {f x} \ space M)" by auto moreover { fix x y have *: "f -` {f x} \ g -` {g x} \ space M = (f -` {f x} \ space M) \ (g -` {g x} \ space M)" by auto assume "x \ space M" "y \ space M" hence "f -` {f x} \ g -` {g x} \ space M \ sets M" using assms unfolding simple_function_def * by auto } ultimately have "\ (f -` {f x} \ space M) = setsum (\) (?sub (f x))" by (subst measure_finitely_additive) auto } hence "simple_integral f = (\(x,A)\?SIGMA. x * \ A)" unfolding simple_integral_def by (subst setsum_Sigma[symmetric], auto intro!: setsum_cong simp: setsum_right_distrib[symmetric]) also have "\ = (\A\?p ` space M. the_elem (f`A) * \ A)" proof - have [simp]: "\x. x \ space M \ f ` ?p x = {f x}" by (auto intro!: imageI) have "(\A. (the_elem (f ` A), A)) ` ?p ` space M = (\x. (f x, ?p x)) ` space M" proof safe fix x assume "x \ space M" thus "(f x, ?p x) \ (\A. (the_elem (f`A), A)) ` ?p ` space M" by (auto intro!: image_eqI[of _ _ "?p x"]) qed auto thus ?thesis apply (auto intro!: setsum_reindex_cong[of "\A. (the_elem (f`A), A)"] inj_onI) apply (rule_tac x="xa" in image_eqI) by simp_all qed finally show ?thesis . qed lemma (in measure_space) simple_integral_add[simp]: assumes "simple_function f" and "simple_function g" shows "simple_integral (\x. f x + g x) = simple_integral f + simple_integral g" proof - { fix x let ?S = "g -` {g x} \ f -` {f x} \ space M" assume "x \ space M" hence "(\a. f a + g a) ` ?S = {f x + g x}" "f ` ?S = {f x}" "g ` ?S = {g x}" "(\x. (f x, g x)) -` {(f x, g x)} \ space M = ?S" by auto } thus ?thesis unfolding simple_function_partition[OF simple_function_add[OF assms] simple_function_Pair[OF assms]] simple_function_partition[OF `simple_function f` `simple_function g`] simple_function_partition[OF `simple_function g` `simple_function f`] apply (subst (3) Int_commute) by (auto simp add: field_simps setsum_addf[symmetric] intro!: setsum_cong) qed lemma (in measure_space) simple_integral_setsum[simp]: assumes "\i. i \ P \ simple_function (f i)" shows "simple_integral (\x. \i\P. f i x) = (\i\P. simple_integral (f i))" proof cases assume "finite P" from this assms show ?thesis by induct (auto simp: simple_function_setsum simple_integral_add) qed auto lemma (in measure_space) simple_integral_mult[simp]: assumes "simple_function f" shows "simple_integral (\x. c * f x) = c * simple_integral f" proof - note mult = simple_function_mult[OF simple_function_const[of c] assms] { fix x let ?S = "f -` {f x} \ (\x. c * f x) -` {c * f x} \ space M" assume "x \ space M" hence "(\x. c * f x) ` ?S = {c * f x}" "f ` ?S = {f x}" by auto } thus ?thesis unfolding simple_function_partition[OF mult assms] simple_function_partition[OF assms mult] by (auto simp: setsum_right_distrib field_simps intro!: setsum_cong) qed lemma (in sigma_algebra) simple_function_If: assumes sf: "simple_function f" "simple_function g" and A: "A \ sets M" shows "simple_function (\x. if x \ A then f x else g x)" (is "simple_function ?IF") proof - def F \ "\x. f -` {x} \ space M" and G \ "\x. g -` {x} \ space M" show ?thesis unfolding simple_function_def proof safe have "?IF ` space M \ f ` space M \ g ` space M" by auto from finite_subset[OF this] assms show "finite (?IF ` space M)" unfolding simple_function_def by auto next fix x assume "x \ space M" then have *: "?IF -` {?IF x} \ space M = (if x \ A then ((F (f x) \ A) \ (G (f x) - (G (f x) \ A))) else ((F (g x) \ A) \ (G (g x) - (G (g x) \ A))))" using sets_into_space[OF A] by (auto split: split_if_asm simp: G_def F_def) have [intro]: "\x. F x \ sets M" "\x. G x \ sets M" unfolding F_def G_def using sf[THEN simple_functionD(2)] by auto show "?IF -` {?IF x} \ space M \ sets M" unfolding * using A by auto qed qed lemma (in measure_space) simple_integral_mono_AE: assumes "simple_function f" and "simple_function g" and mono: "AE x. f x \ g x" shows "simple_integral f \ simple_integral g" proof - let "?S x" = "(g -` {g x} \ space M) \ (f -` {f x} \ space M)" have *: "\x. g -` {g x} \ f -` {f x} \ space M = ?S x" "\x. f -` {f x} \ g -` {g x} \ space M = ?S x" by auto show ?thesis unfolding * simple_function_partition[OF `simple_function f` `simple_function g`] simple_function_partition[OF `simple_function g` `simple_function f`] proof (safe intro!: setsum_mono) fix x assume "x \ space M" then have *: "f ` ?S x = {f x}" "g ` ?S x = {g x}" by auto show "the_elem (f`?S x) * \ (?S x) \ the_elem (g`?S x) * \ (?S x)" proof (cases "f x \ g x") case True then show ?thesis using * by (auto intro!: mult_right_mono) next case False obtain N where N: "{x\space M. \ f x \ g x} \ N" "N \ sets M" "\ N = 0" using mono by (auto elim!: AE_E) have "?S x \ N" using N `x \ space M` False by auto moreover have "?S x \ sets M" using assms by (rule_tac Int) (auto intro!: simple_functionD) ultimately have "\ (?S x) \ \ N" using `N \ sets M` by (auto intro!: measure_mono) then show ?thesis using `\ N = 0` by auto qed qed qed lemma (in measure_space) simple_integral_mono: assumes "simple_function f" and "simple_function g" and mono: "\ x. x \ space M \ f x \ g x" shows "simple_integral f \ simple_integral g" proof (rule simple_integral_mono_AE[OF assms(1, 2)]) show "AE x. f x \ g x" using mono by (rule AE_cong) auto qed lemma (in measure_space) simple_integral_cong_AE: assumes "simple_function f" "simple_function g" and "AE x. f x = g x" shows "simple_integral f = simple_integral g" using assms by (auto simp: eq_iff intro!: simple_integral_mono_AE) lemma (in measure_space) simple_integral_cong': assumes sf: "simple_function f" "simple_function g" and mea: "\ {x\space M. f x \ g x} = 0" shows "simple_integral f = simple_integral g" proof (intro simple_integral_cong_AE sf AE_I) show "\ {x\space M. f x \ g x} = 0" by fact show "{x \ space M. f x \ g x} \ sets M" using sf[THEN borel_measurable_simple_function] by auto qed simp lemma (in measure_space) simple_integral_indicator: assumes "A \ sets M" assumes "simple_function f" shows "simple_integral (\x. f x * indicator A x) = (\x \ f ` space M. x * \ (f -` {x} \ space M \ A))" proof cases assume "A = space M" moreover hence "simple_integral (\x. f x * indicator A x) = simple_integral f" by (auto intro!: simple_integral_cong) moreover have "\X. X \ space M \ space M = X \ space M" by auto ultimately show ?thesis by (simp add: simple_integral_def) next assume "A \ space M" then obtain x where x: "x \ space M" "x \ A" using sets_into_space[OF assms(1)] by auto have I: "(\x. f x * indicator A x) ` space M = f ` A \ {0}" (is "?I ` _ = _") proof safe fix y assume "?I y \ f ` A" hence "y \ A" by auto thus "?I y = 0" by auto next fix y assume "y \ A" thus "f y \ ?I ` space M" using sets_into_space[OF assms(1)] by (auto intro!: image_eqI[of _ _ y]) next show "0 \ ?I ` space M" using x by (auto intro!: image_eqI[of _ _ x]) qed have *: "simple_integral (\x. f x * indicator A x) = (\x \ f ` space M \ {0}. x * \ (f -` {x} \ space M \ A))" unfolding simple_integral_def I proof (rule setsum_mono_zero_cong_left) show "finite (f ` space M \ {0})" using assms(2) unfolding simple_function_def by auto show "f ` A \ {0} \ f`space M \ {0}" using sets_into_space[OF assms(1)] by auto have "\x. f x \ f ` A \ f -` {f x} \ space M \ A = {}" by (auto simp: image_iff) thus "\i\f ` space M \ {0} - (f ` A \ {0}). i * \ (f -` {i} \ space M \ A) = 0" by auto next fix x assume "x \ f`A \ {0}" hence "x \ 0 \ ?I -` {x} \ space M = f -` {x} \ space M \ A" by (auto simp: indicator_def split: split_if_asm) thus "x * \ (?I -` {x} \ space M) = x * \ (f -` {x} \ space M \ A)" by (cases "x = 0") simp_all qed show ?thesis unfolding * using assms(2) unfolding simple_function_def by (auto intro!: setsum_mono_zero_cong_right) qed lemma (in measure_space) simple_integral_indicator_only[simp]: assumes "A \ sets M" shows "simple_integral (indicator A) = \ A" proof cases assume "space M = {}" hence "A = {}" using sets_into_space[OF assms] by auto thus ?thesis unfolding simple_integral_def using `space M = {}` by auto next assume "space M \ {}" hence "(\x. 1) ` space M = {1::pinfreal}" by auto thus ?thesis using simple_integral_indicator[OF assms simple_function_const[of 1]] using sets_into_space[OF assms] by (auto intro!: arg_cong[where f="\"]) qed lemma (in measure_space) simple_integral_null_set: assumes "simple_function u" "N \ null_sets" shows "simple_integral (\x. u x * indicator N x) = 0" proof - have "AE x. indicator N x = (0 :: pinfreal)" using `N \ null_sets` by (auto simp: indicator_def intro!: AE_I[of _ N]) then have "simple_integral (\x. u x * indicator N x) = simple_integral (\x. 0)" using assms by (intro simple_integral_cong_AE) (auto intro!: AE_disjI2) then show ?thesis by simp qed lemma (in measure_space) simple_integral_cong_AE_mult_indicator: assumes sf: "simple_function f" and eq: "AE x. x \ S" and "S \ sets M" shows "simple_integral f = simple_integral (\x. f x * indicator S x)" proof (rule simple_integral_cong_AE) show "simple_function f" by fact show "simple_function (\x. f x * indicator S x)" using sf `S \ sets M` by auto from eq show "AE x. f x = f x * indicator S x" by (rule AE_mp) simp qed lemma (in measure_space) simple_integral_restricted: assumes "A \ sets M" assumes sf: "simple_function (\x. f x * indicator A x)" shows "measure_space.simple_integral (restricted_space A) \ f = simple_integral (\x. f x * indicator A x)" (is "_ = simple_integral ?f") unfolding measure_space.simple_integral_def[OF restricted_measure_space[OF `A \ sets M`]] unfolding simple_integral_def proof (simp, safe intro!: setsum_mono_zero_cong_left) from sf show "finite (?f ` space M)" unfolding simple_function_def by auto next fix x assume "x \ A" then show "f x \ ?f ` space M" using sets_into_space `A \ sets M` by (auto intro!: image_eqI[of _ _ x]) next fix x assume "x \ space M" "?f x \ f`A" then have "x \ A" by (auto simp: image_iff) then show "?f x * \ (?f -` {?f x} \ space M) = 0" by simp next fix x assume "x \ A" then have "f x \ 0 \ f -` {f x} \ A = ?f -` {f x} \ space M" using `A \ sets M` sets_into_space by (auto simp: indicator_def split: split_if_asm) then show "f x * \ (f -` {f x} \ A) = f x * \ (?f -` {f x} \ space M)" unfolding pinfreal_mult_cancel_left by auto qed lemma (in measure_space) simple_integral_subalgebra[simp]: assumes "measure_space (M\sets := N\) \" shows "measure_space.simple_integral (M\sets := N\) \ = simple_integral" unfolding simple_integral_def_raw unfolding measure_space.simple_integral_def_raw[OF assms] by simp lemma (in measure_space) simple_integral_vimage: fixes g :: "'a \ pinfreal" and f :: "'d \ 'a" assumes f: "bij_betw f S (space M)" shows "simple_integral g = measure_space.simple_integral (vimage_algebra S f) (\A. \ (f ` A)) (\x. g (f x))" (is "_ = measure_space.simple_integral ?T ?\ _") proof - from f interpret T: measure_space ?T ?\ by (rule measure_space_isomorphic) have surj: "f`S = space M" using f unfolding bij_betw_def by simp have *: "(\x. g (f x)) ` S = g ` f ` S" by auto have **: "f`S = space M" using f unfolding bij_betw_def by auto { fix x assume "x \ space M" have "(f ` ((\x. g (f x)) -` {g x} \ S)) = (f ` (f -` (g -` {g x}) \ S))" by auto also have "f -` (g -` {g x}) \ S = f -` (g -` {g x} \ space M) \ S" using f unfolding bij_betw_def by auto also have "(f ` (f -` (g -` {g x} \ space M) \ S)) = g -` {g x} \ space M" using ** by (intro image_vimage_inter_eq) auto finally have "(f ` ((\x. g (f x)) -` {g x} \ S)) = g -` {g x} \ space M" by auto } then show ?thesis using assms unfolding simple_integral_def T.simple_integral_def bij_betw_def by (auto simp add: * intro!: setsum_cong) qed section "Continuous posititve integration" definition (in measure_space) "positive_integral f = SUPR {g. simple_function g \ g \ f} simple_integral" lemma (in measure_space) positive_integral_alt: "positive_integral f = (SUPR {g. simple_function g \ g \ f \ \ \ g`space M} simple_integral)" (is "_ = ?alt") proof (rule antisym SUP_leI) show "positive_integral f \ ?alt" unfolding positive_integral_def proof (safe intro!: SUP_leI) fix g assume g: "simple_function g" "g \ f" let ?G = "g -` {\} \ space M" show "simple_integral g \ SUPR {g. simple_function g \ g \ f \ \ \ g ` space M} simple_integral" (is "simple_integral g \ SUPR ?A simple_integral") proof cases let ?g = "\x. indicator (space M - ?G) x * g x" have g': "simple_function ?g" using g by (auto intro: simple_functionD) moreover assume "\ ?G = 0" then have "AE x. g x = ?g x" using g by (intro AE_I[where N="?G"]) (auto intro: simple_functionD simp: indicator_def) with g(1) g' have "simple_integral g = simple_integral ?g" by (rule simple_integral_cong_AE) moreover have "?g \ g" by (auto simp: le_fun_def indicator_def) from this `g \ f` have "?g \ f" by (rule order_trans) moreover have "\ \ ?g ` space M" by (auto simp: indicator_def split: split_if_asm) ultimately show ?thesis by (auto intro!: le_SUPI) next assume "\ ?G \ 0" then have "?G \ {}" by auto then have "\ \ g`space M" by force then have "space M \ {}" by auto have "SUPR ?A simple_integral = \" proof (intro SUP_\[THEN iffD2] allI impI) fix x assume "x < \" then guess n unfolding less_\_Ex_of_nat .. note n = this then have "0 < n" by (intro neq0_conv[THEN iffD1] notI) simp let ?g = "\x. (of_nat n / (if \ ?G = \ then 1 else \ ?G)) * indicator ?G x" show "\i\?A. x < simple_integral i" proof (intro bexI impI CollectI conjI) show "simple_function ?g" using g by (auto intro!: simple_functionD simple_function_add) have "?g \ g" by (auto simp: le_fun_def indicator_def) from this g(2) show "?g \ f" by (rule order_trans) show "\ \ ?g ` space M" using `\ ?G \ 0` by (auto simp: indicator_def split: split_if_asm) have "x < (of_nat n / (if \ ?G = \ then 1 else \ ?G)) * \ ?G" using n `\ ?G \ 0` `0 < n` by (auto simp: pinfreal_noteq_omega_Ex field_simps) also have "\ = simple_integral ?g" using g `space M \ {}` by (subst simple_integral_indicator) (auto simp: image_constant ac_simps dest: simple_functionD) finally show "x < simple_integral ?g" . qed qed then show ?thesis by simp qed qed qed (auto intro!: SUP_subset simp: positive_integral_def) lemma (in measure_space) positive_integral_cong_measure: assumes "\A. A \ sets M \ \ A = \ A" shows "measure_space.positive_integral M \ f = positive_integral f" proof - interpret v: measure_space M \ by (rule measure_space_cong) fact with assms show ?thesis unfolding positive_integral_def v.positive_integral_def SUPR_def by (auto intro!: arg_cong[where f=Sup] image_cong simp: simple_integral_cong_measure[of \]) qed lemma (in measure_space) positive_integral_alt1: "positive_integral f = (SUP g : {g. simple_function g \ (\x\space M. g x \ f x \ g x \ \)}. simple_integral g)" unfolding positive_integral_alt SUPR_def proof (safe intro!: arg_cong[where f=Sup]) fix g let ?g = "\x. if x \ space M then g x else f x" assume "simple_function g" "\x\space M. g x \ f x \ g x \ \" hence "?g \ f" "simple_function ?g" "simple_integral g = simple_integral ?g" "\ \ g`space M" unfolding le_fun_def by (auto cong: simple_function_cong simple_integral_cong) thus "simple_integral g \ simple_integral ` {g. simple_function g \ g \ f \ \ \ g`space M}" by auto next fix g assume "simple_function g" "g \ f" "\ \ g`space M" hence "simple_function g" "\x\space M. g x \ f x \ g x \ \" by (auto simp add: le_fun_def image_iff) thus "simple_integral g \ simple_integral ` {g. simple_function g \ (\x\space M. g x \ f x \ g x \ \)}" by auto qed lemma (in measure_space) positive_integral_cong: assumes "\x. x \ space M \ f x = g x" shows "positive_integral f = positive_integral g" proof - have "\h. (\x\space M. h x \ f x \ h x \ \) = (\x\space M. h x \ g x \ h x \ \)" using assms by auto thus ?thesis unfolding positive_integral_alt1 by auto qed lemma (in measure_space) positive_integral_eq_simple_integral: assumes "simple_function f" shows "positive_integral f = simple_integral f" unfolding positive_integral_def proof (safe intro!: pinfreal_SUPI) fix g assume "simple_function g" "g \ f" with assms show "simple_integral g \ simple_integral f" by (auto intro!: simple_integral_mono simp: le_fun_def) next fix y assume "\x. x\{g. simple_function g \ g \ f} \ simple_integral x \ y" with assms show "simple_integral f \ y" by auto qed lemma (in measure_space) positive_integral_mono_AE: assumes ae: "AE x. u x \ v x" shows "positive_integral u \ positive_integral v" unfolding positive_integral_alt1 proof (safe intro!: SUPR_mono) fix a assume a: "simple_function a" and mono: "\x\space M. a x \ u x \ a x \ \" from ae obtain N where N: "{x\space M. \ u x \ v x} \ N" "N \ sets M" "\ N = 0" by (auto elim!: AE_E) have "simple_function (\x. a x * indicator (space M - N) x)" using `N \ sets M` a by auto with a show "\b\{g. simple_function g \ (\x\space M. g x \ v x \ g x \ \)}. simple_integral a \ simple_integral b" proof (safe intro!: bexI[of _ "\x. a x * indicator (space M - N) x"] simple_integral_mono_AE) show "AE x. a x \ a x * indicator (space M - N) x" proof (rule AE_I, rule subset_refl) have *: "{x \ space M. \ a x \ a x * indicator (space M - N) x} = N \ {x \ space M. a x \ 0}" (is "?N = _") using `N \ sets M`[THEN sets_into_space] by (auto simp: indicator_def) then show "?N \ sets M" using `N \ sets M` `simple_function a`[THEN borel_measurable_simple_function] by (auto intro!: measure_mono Int) then have "\ ?N \ \ N" unfolding * using `N \ sets M` by (auto intro!: measure_mono) then show "\ ?N = 0" using `\ N = 0` by auto qed next fix x assume "x \ space M" show "a x * indicator (space M - N) x \ v x" proof (cases "x \ N") case True then show ?thesis by simp next case False with N mono have "a x \ u x" "u x \ v x" using `x \ space M` by auto with False `x \ space M` show "a x * indicator (space M - N) x \ v x" by auto qed assume "a x * indicator (space M - N) x = \" with mono `x \ space M` show False by (simp split: split_if_asm add: indicator_def) qed qed lemma (in measure_space) positive_integral_cong_AE: "AE x. u x = v x \ positive_integral u = positive_integral v" by (auto simp: eq_iff intro!: positive_integral_mono_AE) lemma (in measure_space) positive_integral_mono: assumes mono: "\x. x \ space M \ u x \ v x" shows "positive_integral u \ positive_integral v" using mono by (auto intro!: AE_cong positive_integral_mono_AE) lemma image_set_cong: assumes A: "\x. x \ A \ \y\B. f x = g y" assumes B: "\y. y \ B \ \x\A. g y = f x" shows "f ` A = g ` B" using assms by blast lemma (in measure_space) positive_integral_vimage: fixes g :: "'a \ pinfreal" and f :: "'d \ 'a" assumes f: "bij_betw f S (space M)" shows "positive_integral g = measure_space.positive_integral (vimage_algebra S f) (\A. \ (f ` A)) (\x. g (f x))" (is "_ = measure_space.positive_integral ?T ?\ _") proof - from f interpret T: measure_space ?T ?\ by (rule measure_space_isomorphic) have f_fun: "f \ S \ space M" using assms unfolding bij_betw_def by auto from assms have inv: "bij_betw (the_inv_into S f) (space M) S" by (rule bij_betw_the_inv_into) then have inv_fun: "the_inv_into S f \ space M \ S" unfolding bij_betw_def by auto have surj: "f`S = space M" using f unfolding bij_betw_def by simp have inj: "inj_on f S" using f unfolding bij_betw_def by simp have inv_f: "\x. x \ space M \ f (the_inv_into S f x) = x" using f_the_inv_into_f[of f S] f unfolding bij_betw_def by auto from simple_integral_vimage[OF assms, symmetric] have *: "simple_integral = T.simple_integral \ (\g. g \ f)" by (simp add: comp_def) show ?thesis unfolding positive_integral_alt1 T.positive_integral_alt1 SUPR_def * image_compose proof (safe intro!: arg_cong[where f=Sup] image_set_cong, simp_all add: comp_def) fix g' :: "'a \ pinfreal" assume "simple_function g'" "\x\space M. g' x \ g x \ g' x \ \" then show "\h. T.simple_function h \ (\x\S. h x \ g (f x) \ h x \ \) \ T.simple_integral (\x. g' (f x)) = T.simple_integral h" using f unfolding bij_betw_def by (auto intro!: exI[of _ "\x. g' (f x)"] simp add: le_fun_def simple_function_vimage[OF _ f_fun]) next fix g' :: "'d \ pinfreal" assume g': "T.simple_function g'" "\x\S. g' x \ g (f x) \ g' x \ \" let ?g = "\x. g' (the_inv_into S f x)" show "\h. simple_function h \ (\x\space M. h x \ g x \ h x \ \) \ T.simple_integral g' = T.simple_integral (\x. h (f x))" proof (intro exI[of _ ?g] conjI ballI) { fix x assume x: "x \ space M" then have "the_inv_into S f x \ S" using inv_fun by auto with g' have "g' (the_inv_into S f x) \ g (f (the_inv_into S f x)) \ g' (the_inv_into S f x) \ \" by auto then show "g' (the_inv_into S f x) \ g x" "g' (the_inv_into S f x) \ \" using f_the_inv_into_f[of f S x] x f unfolding bij_betw_def by auto } note vimage_vimage_inv[OF f inv_f inv_fun, simp] from T.simple_function_vimage[OF g'(1), unfolded space_vimage_algebra, OF inv_fun] show "simple_function (\x. g' (the_inv_into S f x))" unfolding simple_function_def by (simp add: simple_function_def) show "T.simple_integral g' = T.simple_integral (\x. ?g (f x))" using the_inv_into_f_f[OF inj] by (auto intro!: T.simple_integral_cong) qed qed qed lemma (in measure_space) positive_integral_vimage_inv: fixes g :: "'d \ pinfreal" and f :: "'d \ 'a" assumes f: "bij_betw f S (space M)" shows "measure_space.positive_integral (vimage_algebra S f) (\A. \ (f ` A)) g = positive_integral (\x. g (the_inv_into S f x))" proof - interpret v: measure_space "vimage_algebra S f" "\A. \ (f ` A)" using f by (rule measure_space_isomorphic) show ?thesis unfolding positive_integral_vimage[OF f, of "\x. g (the_inv_into S f x)"] using f[unfolded bij_betw_def] by (auto intro!: v.positive_integral_cong simp: the_inv_into_f_f) qed lemma (in measure_space) positive_integral_SUP_approx: assumes "f \ s" and f: "\i. f i \ borel_measurable M" and "simple_function u" and le: "u \ s" and real: "\ \ u`space M" shows "simple_integral u \ (SUP i. positive_integral (f i))" (is "_ \ ?S") proof (rule pinfreal_le_mult_one_interval) fix a :: pinfreal assume "0 < a" "a < 1" hence "a \ 0" by auto let "?B i" = "{x \ space M. a * u x \ f i x}" have B: "\i. ?B i \ sets M" using f `simple_function u` by (auto simp: borel_measurable_simple_function) let "?uB i x" = "u x * indicator (?B i) x" { fix i have "?B i \ ?B (Suc i)" proof safe fix i x assume "a * u x \ f i x" also have "\ \ f (Suc i) x" using `f \ s` unfolding isoton_def le_fun_def by auto finally show "a * u x \ f (Suc i) x" . qed } note B_mono = this have u: "\x. x \ space M \ u -` {u x} \ space M \ sets M" using `simple_function u` by (auto simp add: simple_function_def) have "\i. (\n. (u -` {i} \ space M) \ ?B n) \ (u -` {i} \ space M)" using B_mono unfolding isoton_def proof safe fix x i assume "x \ space M" show "x \ (\i. (u -` {u x} \ space M) \ ?B i)" proof cases assume "u x = 0" thus ?thesis using `x \ space M` by simp next assume "u x \ 0" with `a < 1` real `x \ space M` have "a * u x < 1 * u x" by (rule_tac pinfreal_mult_strict_right_mono) (auto simp: image_iff) also have "\ \ (SUP i. f i x)" using le `f \ s` unfolding isoton_fun_expand by (auto simp: isoton_def le_fun_def) finally obtain i where "a * u x < f i x" unfolding SUPR_def by (auto simp add: less_Sup_iff) hence "a * u x \ f i x" by auto thus ?thesis using `x \ space M` by auto qed qed auto note measure_conv = measure_up[OF Int[OF u B] this] have "simple_integral u = (SUP i. simple_integral (?uB i))" unfolding simple_integral_indicator[OF B `simple_function u`] proof (subst SUPR_pinfreal_setsum, safe) fix x n assume "x \ space M" have "\ (u -` {u x} \ space M \ {x \ space M. a * u x \ f n x}) \ \ (u -` {u x} \ space M \ {x \ space M. a * u x \ f (Suc n) x})" using B_mono Int[OF u[OF `x \ space M`] B] by (auto intro!: measure_mono) thus "u x * \ (u -` {u x} \ space M \ ?B n) \ u x * \ (u -` {u x} \ space M \ ?B (Suc n))" by (auto intro: mult_left_mono) next show "simple_integral u = (\i\u ` space M. SUP n. i * \ (u -` {i} \ space M \ ?B n))" using measure_conv unfolding simple_integral_def isoton_def by (auto intro!: setsum_cong simp: pinfreal_SUP_cmult) qed moreover have "a * (SUP i. simple_integral (?uB i)) \ ?S" unfolding pinfreal_SUP_cmult[symmetric] proof (safe intro!: SUP_mono bexI) fix i have "a * simple_integral (?uB i) = simple_integral (\x. a * ?uB i x)" using B `simple_function u` by (subst simple_integral_mult[symmetric]) (auto simp: field_simps) also have "\ \ positive_integral (f i)" proof - have "\x. a * ?uB i x \ f i x" unfolding indicator_def by auto hence *: "simple_function (\x. a * ?uB i x)" using B assms(3) by (auto intro!: simple_integral_mono) show ?thesis unfolding positive_integral_eq_simple_integral[OF *, symmetric] by (auto intro!: positive_integral_mono simp: indicator_def) qed finally show "a * simple_integral (?uB i) \ positive_integral (f i)" by auto qed simp ultimately show "a * simple_integral u \ ?S" by simp qed text {* Beppo-Levi monotone convergence theorem *} lemma (in measure_space) positive_integral_isoton: assumes "f \ u" "\i. f i \ borel_measurable M" shows "(\i. positive_integral (f i)) \ positive_integral u" unfolding isoton_def proof safe fix i show "positive_integral (f i) \ positive_integral (f (Suc i))" apply (rule positive_integral_mono) using `f \ u` unfolding isoton_def le_fun_def by auto next have "u \ borel_measurable M" using borel_measurable_SUP[of UNIV f] assms by (auto simp: isoton_def) have u: "u = (SUP i. f i)" using `f \ u` unfolding isoton_def by auto show "(SUP i. positive_integral (f i)) = positive_integral u" proof (rule antisym) from `f \ u`[THEN isoton_Sup, unfolded le_fun_def] show "(SUP j. positive_integral (f j)) \ positive_integral u" by (auto intro!: SUP_leI positive_integral_mono) next show "positive_integral u \ (SUP i. positive_integral (f i))" unfolding positive_integral_alt[of u] by (auto intro!: SUP_leI positive_integral_SUP_approx[OF assms]) qed qed lemma (in measure_space) positive_integral_monotone_convergence_SUP: assumes "\i x. x \ space M \ f i x \ f (Suc i) x" assumes "\i. f i \ borel_measurable M" shows "(SUP i. positive_integral (f i)) = positive_integral (\x. SUP i. f i x)" (is "_ = positive_integral ?u") proof - have "?u \ borel_measurable M" using borel_measurable_SUP[of _ f] assms by (simp add: SUPR_fun_expand) show ?thesis proof (rule antisym) show "(SUP j. positive_integral (f j)) \ positive_integral ?u" by (auto intro!: SUP_leI positive_integral_mono le_SUPI) next def rf \ "\i. \x\space M. f i x" and ru \ "\x\space M. ?u x" have "\i. rf i \ borel_measurable M" unfolding rf_def using assms by (simp cong: measurable_cong) moreover have iso: "rf \ ru" using assms unfolding rf_def ru_def unfolding isoton_def SUPR_fun_expand le_fun_def fun_eq_iff using SUP_const[OF UNIV_not_empty] by (auto simp: restrict_def le_fun_def SUPR_fun_expand fun_eq_iff) ultimately have "positive_integral ru \ (SUP i. positive_integral (rf i))" unfolding positive_integral_alt[of ru] by (auto simp: le_fun_def intro!: SUP_leI positive_integral_SUP_approx) then show "positive_integral ?u \ (SUP i. positive_integral (f i))" unfolding ru_def rf_def by (simp cong: positive_integral_cong) qed qed lemma (in measure_space) SUP_simple_integral_sequences: assumes f: "f \ u" "\i. simple_function (f i)" and g: "g \ u" "\i. simple_function (g i)" shows "(SUP i. simple_integral (f i)) = (SUP i. simple_integral (g i))" (is "SUPR _ ?F = SUPR _ ?G") proof - have "(SUP i. ?F i) = (SUP i. positive_integral (f i))" using assms by (simp add: positive_integral_eq_simple_integral) also have "\ = positive_integral u" using positive_integral_isoton[OF f(1) borel_measurable_simple_function[OF f(2)]] unfolding isoton_def by simp also have "\ = (SUP i. positive_integral (g i))" using positive_integral_isoton[OF g(1) borel_measurable_simple_function[OF g(2)]] unfolding isoton_def by simp also have "\ = (SUP i. ?G i)" using assms by (simp add: positive_integral_eq_simple_integral) finally show ?thesis . qed lemma (in measure_space) positive_integral_const[simp]: "positive_integral (\x. c) = c * \ (space M)" by (subst positive_integral_eq_simple_integral) auto lemma (in measure_space) positive_integral_isoton_simple: assumes "f \ u" and e: "\i. simple_function (f i)" shows "(\i. simple_integral (f i)) \ positive_integral u" using positive_integral_isoton[OF `f \ u` e(1)[THEN borel_measurable_simple_function]] unfolding positive_integral_eq_simple_integral[OF e] . lemma (in measure_space) positive_integral_linear: assumes f: "f \ borel_measurable M" and g: "g \ borel_measurable M" shows "positive_integral (\x. a * f x + g x) = a * positive_integral f + positive_integral g" (is "positive_integral ?L = _") proof - from borel_measurable_implies_simple_function_sequence'[OF f] guess u . note u = this positive_integral_isoton_simple[OF this(1-2)] from borel_measurable_implies_simple_function_sequence'[OF g] guess v . note v = this positive_integral_isoton_simple[OF this(1-2)] let "?L' i x" = "a * u i x + v i x" have "?L \ borel_measurable M" using assms by simp from borel_measurable_implies_simple_function_sequence'[OF this] guess l . note positive_integral_isoton_simple[OF this(1-2)] and l = this moreover have "(SUP i. simple_integral (l i)) = (SUP i. simple_integral (?L' i))" proof (rule SUP_simple_integral_sequences[OF l(1-2)]) show "?L' \ ?L" "\i. simple_function (?L' i)" using u v by (auto simp: isoton_fun_expand isoton_add isoton_cmult_right) qed moreover from u v have L'_isoton: "(\i. simple_integral (?L' i)) \ a * positive_integral f + positive_integral g" by (simp add: isoton_add isoton_cmult_right) ultimately show ?thesis by (simp add: isoton_def) qed lemma (in measure_space) positive_integral_cmult: assumes "f \ borel_measurable M" shows "positive_integral (\x. c * f x) = c * positive_integral f" using positive_integral_linear[OF assms, of "\x. 0" c] by auto lemma (in measure_space) positive_integral_indicator[simp]: "A \ sets M \ positive_integral (\x. indicator A x) = \ A" by (subst positive_integral_eq_simple_integral) (auto simp: simple_function_indicator simple_integral_indicator) lemma (in measure_space) positive_integral_cmult_indicator: "A \ sets M \ positive_integral (\x. c * indicator A x) = c * \ A" by (subst positive_integral_eq_simple_integral) (auto simp: simple_function_indicator simple_integral_indicator) lemma (in measure_space) positive_integral_add: assumes "f \ borel_measurable M" "g \ borel_measurable M" shows "positive_integral (\x. f x + g x) = positive_integral f + positive_integral g" using positive_integral_linear[OF assms, of 1] by simp lemma (in measure_space) positive_integral_setsum: assumes "\i. i\P \ f i \ borel_measurable M" shows "positive_integral (\x. \i\P. f i x) = (\i\P. positive_integral (f i))" proof cases assume "finite P" from this assms show ?thesis proof induct case (insert i P) have "f i \ borel_measurable M" "(\x. \i\P. f i x) \ borel_measurable M" using insert by (auto intro!: borel_measurable_pinfreal_setsum) from positive_integral_add[OF this] show ?case using insert by auto qed simp qed simp lemma (in measure_space) positive_integral_diff: assumes f: "f \ borel_measurable M" and g: "g \ borel_measurable M" and fin: "positive_integral g \ \" and mono: "\x. x \ space M \ g x \ f x" shows "positive_integral (\x. f x - g x) = positive_integral f - positive_integral g" proof - have borel: "(\x. f x - g x) \ borel_measurable M" using f g by (rule borel_measurable_pinfreal_diff) have "positive_integral (\x. f x - g x) + positive_integral g = positive_integral f" unfolding positive_integral_add[OF borel g, symmetric] proof (rule positive_integral_cong) fix x assume "x \ space M" from mono[OF this] show "f x - g x + g x = f x" by (cases "f x", cases "g x", simp, simp, cases "g x", auto) qed with mono show ?thesis by (subst minus_pinfreal_eq2[OF _ fin]) (auto intro!: positive_integral_mono) qed lemma (in measure_space) positive_integral_psuminf: assumes "\i. f i \ borel_measurable M" shows "positive_integral (\x. \\<^isub>\ i. f i x) = (\\<^isub>\ i. positive_integral (f i))" proof - have "(\i. positive_integral (\x. \i positive_integral (\x. \\<^isub>\i. f i x)" by (rule positive_integral_isoton) (auto intro!: borel_measurable_pinfreal_setsum assms positive_integral_mono arg_cong[where f=Sup] simp: isoton_def le_fun_def psuminf_def fun_eq_iff SUPR_def Sup_fun_def) thus ?thesis by (auto simp: isoton_def psuminf_def positive_integral_setsum[OF assms]) qed text {* Fatou's lemma: convergence theorem on limes inferior *} lemma (in measure_space) positive_integral_lim_INF: fixes u :: "nat \ 'a \ pinfreal" assumes "\i. u i \ borel_measurable M" shows "positive_integral (SUP n. INF m. u (m + n)) \ (SUP n. INF m. positive_integral (u (m + n)))" proof - have "(SUP n. INF m. u (m + n)) \ borel_measurable M" by (auto intro!: borel_measurable_SUP borel_measurable_INF assms) have "(\n. INF m. u (m + n)) \ (SUP n. INF m. u (m + n))" proof (unfold isoton_def, safe intro!: INF_mono bexI) fix i m show "u (Suc m + i) \ u (m + Suc i)" by simp qed simp from positive_integral_isoton[OF this] assms have "positive_integral (SUP n. INF m. u (m + n)) = (SUP n. positive_integral (INF m. u (m + n)))" unfolding isoton_def by (simp add: borel_measurable_INF) also have "\ \ (SUP n. INF m. positive_integral (u (m + n)))" apply (rule SUP_mono) apply (rule_tac x=n in bexI) by (auto intro!: positive_integral_mono INFI_bound INF_leI exI simp: INFI_fun_expand) finally show ?thesis . qed lemma (in measure_space) measure_space_density: assumes borel: "u \ borel_measurable M" shows "measure_space M (\A. positive_integral (\x. u x * indicator A x))" (is "measure_space M ?v") proof show "?v {} = 0" by simp show "countably_additive M ?v" unfolding countably_additive_def proof safe fix A :: "nat \ 'a set" assume "range A \ sets M" hence "\i. (\x. u x * indicator (A i) x) \ borel_measurable M" using borel by (auto intro: borel_measurable_indicator) moreover assume "disjoint_family A" note psuminf_indicator[OF this] ultimately show "(\\<^isub>\n. ?v (A n)) = ?v (\x. A x)" by (simp add: positive_integral_psuminf[symmetric]) qed qed lemma (in measure_space) positive_integral_translated_density: assumes "f \ borel_measurable M" "g \ borel_measurable M" shows "measure_space.positive_integral M (\A. positive_integral (\x. f x * indicator A x)) g = positive_integral (\x. f x * g x)" (is "measure_space.positive_integral M ?T _ = _") proof - from measure_space_density[OF assms(1)] interpret T: measure_space M ?T . from borel_measurable_implies_simple_function_sequence[OF assms(2)] obtain G where G: "\i. simple_function (G i)" "G \ g" by blast note G_borel = borel_measurable_simple_function[OF this(1)] from T.positive_integral_isoton[OF `G \ g` G_borel] have *: "(\i. T.positive_integral (G i)) \ T.positive_integral g" . { fix i have [simp]: "finite (G i ` space M)" using G(1) unfolding simple_function_def by auto have "T.positive_integral (G i) = T.simple_integral (G i)" using G T.positive_integral_eq_simple_integral by simp also have "\ = positive_integral (\x. f x * (\y\G i`space M. y * indicator (G i -` {y} \ space M) x))" apply (simp add: T.simple_integral_def) apply (subst positive_integral_cmult[symmetric]) using G_borel assms(1) apply (fastsimp intro: borel_measurable_indicator borel_measurable_vimage) apply (subst positive_integral_setsum[symmetric]) using G_borel assms(1) apply (fastsimp intro: borel_measurable_indicator borel_measurable_vimage) by (simp add: setsum_right_distrib field_simps) also have "\ = positive_integral (\x. f x * G i x)" by (auto intro!: positive_integral_cong simp: indicator_def if_distrib setsum_cases) finally have "T.positive_integral (G i) = positive_integral (\x. f x * G i x)" . } with * have eq_Tg: "(\i. positive_integral (\x. f x * G i x)) \ T.positive_integral g" by simp from G(2) have "(\i x. f x * G i x) \ (\x. f x * g x)" unfolding isoton_fun_expand by (auto intro!: isoton_cmult_right) then have "(\i. positive_integral (\x. f x * G i x)) \ positive_integral (\x. f x * g x)" using assms(1) G_borel by (auto intro!: positive_integral_isoton borel_measurable_pinfreal_times) with eq_Tg show "T.positive_integral g = positive_integral (\x. f x * g x)" unfolding isoton_def by simp qed lemma (in measure_space) positive_integral_null_set: assumes "N \ null_sets" shows "positive_integral (\x. u x * indicator N x) = 0" proof - have "positive_integral (\x. u x * indicator N x) = positive_integral (\x. 0)" proof (intro positive_integral_cong_AE AE_I) show "{x \ space M. u x * indicator N x \ 0} \ N" by (auto simp: indicator_def) show "\ N = 0" "N \ sets M" using assms by auto qed then show ?thesis by simp qed lemma (in measure_space) positive_integral_Markov_inequality: assumes borel: "u \ borel_measurable M" and "A \ sets M" and c: "c \ \" shows "\ ({x\space M. 1 \ c * u x} \ A) \ c * positive_integral (\x. u x * indicator A x)" (is "\ ?A \ _ * ?PI") proof - have "?A \ sets M" using `A \ sets M` borel by auto hence "\ ?A = positive_integral (\x. indicator ?A x)" using positive_integral_indicator by simp also have "\ \ positive_integral (\x. c * (u x * indicator A x))" proof (rule positive_integral_mono) fix x assume "x \ space M" show "indicator ?A x \ c * (u x * indicator A x)" by (cases "x \ ?A") auto qed also have "\ = c * positive_integral (\x. u x * indicator A x)" using assms by (auto intro!: positive_integral_cmult borel_measurable_indicator) finally show ?thesis . qed lemma (in measure_space) positive_integral_0_iff: assumes borel: "u \ borel_measurable M" shows "positive_integral u = 0 \ \ {x\space M. u x \ 0} = 0" (is "_ \ \ ?A = 0") proof - have A: "?A \ sets M" using borel by auto have u: "positive_integral (\x. u x * indicator ?A x) = positive_integral u" by (auto intro!: positive_integral_cong simp: indicator_def) show ?thesis proof assume "\ ?A = 0" hence "?A \ null_sets" using `?A \ sets M` by auto from positive_integral_null_set[OF this] have "0 = positive_integral (\x. u x * indicator ?A x)" by simp thus "positive_integral u = 0" unfolding u by simp next assume *: "positive_integral u = 0" let "?M n" = "{x \ space M. 1 \ of_nat n * u x}" have "0 = (SUP n. \ (?M n \ ?A))" proof - { fix n from positive_integral_Markov_inequality[OF borel `?A \ sets M`, of "of_nat n"] have "\ (?M n \ ?A) = 0" unfolding * u by simp } thus ?thesis by simp qed also have "\ = \ (\n. ?M n \ ?A)" proof (safe intro!: continuity_from_below) fix n show "?M n \ ?A \ sets M" using borel by (auto intro!: Int) next fix n x assume "1 \ of_nat n * u x" also have "\ \ of_nat (Suc n) * u x" by (subst (1 2) mult_commute) (auto intro!: pinfreal_mult_cancel) finally show "1 \ of_nat (Suc n) * u x" . qed also have "\ = \ ?A" proof (safe intro!: arg_cong[where f="\"]) fix x assume "u x \ 0" and [simp, intro]: "x \ space M" show "x \ (\n. ?M n \ ?A)" proof (cases "u x") case (preal r) obtain j where "1 / r \ of_nat j" using ex_le_of_nat .. hence "1 / r * r \ of_nat j * r" using preal unfolding mult_le_cancel_right by auto hence "1 \ of_nat j * r" using preal `u x \ 0` by auto thus ?thesis using `u x \ 0` preal by (auto simp: real_of_nat_def[symmetric]) qed auto qed finally show "\ ?A = 0" by simp qed qed lemma (in measure_space) positive_integral_restricted: assumes "A \ sets M" shows "measure_space.positive_integral (restricted_space A) \ f = positive_integral (\x. f x * indicator A x)" (is "measure_space.positive_integral ?R \ f = positive_integral ?f") proof - have msR: "measure_space ?R \" by (rule restricted_measure_space[OF `A \ sets M`]) then interpret R: measure_space ?R \ . have saR: "sigma_algebra ?R" by fact have *: "R.positive_integral f = R.positive_integral ?f" by (intro R.positive_integral_cong) auto show ?thesis unfolding * R.positive_integral_def positive_integral_def unfolding simple_function_restricted[OF `A \ sets M`] apply (simp add: SUPR_def) apply (rule arg_cong[where f=Sup]) proof (auto simp add: image_iff simple_integral_restricted[OF `A \ sets M`]) fix g assume "simple_function (\x. g x * indicator A x)" "g \ f" then show "\x. simple_function x \ x \ (\x. f x * indicator A x) \ simple_integral (\x. g x * indicator A x) = simple_integral x" apply (rule_tac exI[of _ "\x. g x * indicator A x"]) by (auto simp: indicator_def le_fun_def) next fix g assume g: "simple_function g" "g \ (\x. f x * indicator A x)" then have *: "(\x. g x * indicator A x) = g" "\x. g x * indicator A x = g x" "\x. g x \ f x" by (auto simp: le_fun_def fun_eq_iff indicator_def split: split_if_asm) from g show "\x. simple_function (\xa. x xa * indicator A xa) \ x \ f \ simple_integral g = simple_integral (\xa. x xa * indicator A xa)" using `A \ sets M`[THEN sets_into_space] apply (rule_tac exI[of _ "\x. g x * indicator A x"]) by (fastsimp simp: le_fun_def *) qed qed lemma (in measure_space) positive_integral_subalgebra[simp]: assumes borel: "f \ borel_measurable (M\sets := N\)" and N_subalgebra: "N \ sets M" "sigma_algebra (M\sets := N\)" shows "measure_space.positive_integral (M\sets := N\) \ f = positive_integral f" proof - note msN = measure_space_subalgebra[OF N_subalgebra] then interpret N: measure_space "M\sets:=N\" \ . from N.borel_measurable_implies_simple_function_sequence[OF borel] obtain fs where Nsf: "\i. N.simple_function (fs i)" and "fs \ f" by blast then have sf: "\i. simple_function (fs i)" using simple_function_subalgebra[OF _ N_subalgebra] by blast from positive_integral_isoton_simple[OF `fs \ f` sf] N.positive_integral_isoton_simple[OF `fs \ f` Nsf] show ?thesis unfolding simple_integral_subalgebra[OF msN] isoton_def by simp qed section "Lebesgue Integral" definition (in measure_space) integrable where "integrable f \ f \ borel_measurable M \ positive_integral (\x. Real (f x)) \ \ \ positive_integral (\x. Real (- f x)) \ \" lemma (in measure_space) integrableD[dest]: assumes "integrable f" shows "f \ borel_measurable M" "positive_integral (\x. Real (f x)) \ \" "positive_integral (\x. Real (- f x)) \ \" using assms unfolding integrable_def by auto definition (in measure_space) integral where "integral f = real (positive_integral (\x. Real (f x))) - real (positive_integral (\x. Real (- f x)))" lemma (in measure_space) integral_cong: assumes cong: "\x. x \ space M \ f x = g x" shows "integral f = integral g" using assms by (simp cong: positive_integral_cong add: integral_def) lemma (in measure_space) integral_cong_measure: assumes "\A. A \ sets M \ \ A = \ A" shows "measure_space.integral M \ f = integral f" proof - interpret v: measure_space M \ by (rule measure_space_cong) fact show ?thesis unfolding integral_def v.integral_def by (simp add: positive_integral_cong_measure[OF assms]) qed lemma (in measure_space) integral_cong_AE: assumes cong: "AE x. f x = g x" shows "integral f = integral g" proof - have "AE x. Real (f x) = Real (g x)" using cong by (rule AE_mp) simp moreover have "AE x. Real (- f x) = Real (- g x)" using cong by (rule AE_mp) simp ultimately show ?thesis by (simp cong: positive_integral_cong_AE add: integral_def) qed lemma (in measure_space) integrable_cong: "(\x. x \ space M \ f x = g x) \ integrable f \ integrable g" by (simp cong: positive_integral_cong measurable_cong add: integrable_def) lemma (in measure_space) integral_eq_positive_integral: assumes "\x. 0 \ f x" shows "integral f = real (positive_integral (\x. Real (f x)))" proof - have "\x. Real (- f x) = 0" using assms by simp thus ?thesis by (simp del: Real_eq_0 add: integral_def) qed lemma (in measure_space) integral_vimage_inv: assumes f: "bij_betw f S (space M)" shows "measure_space.integral (vimage_algebra S f) (\A. \ (f ` A)) (\x. g x) = integral (\x. g (the_inv_into S f x))" proof - interpret v: measure_space "vimage_algebra S f" "\A. \ (f ` A)" using f by (rule measure_space_isomorphic) have "\x. x \ space (vimage_algebra S f) \ the_inv_into S f (f x) = x" using f[unfolded bij_betw_def] by (simp add: the_inv_into_f_f) then have *: "v.positive_integral (\x. Real (g (the_inv_into S f (f x)))) = v.positive_integral (\x. Real (g x))" "v.positive_integral (\x. Real (- g (the_inv_into S f (f x)))) = v.positive_integral (\x. Real (- g x))" by (auto intro!: v.positive_integral_cong) show ?thesis unfolding integral_def v.integral_def unfolding positive_integral_vimage[OF f] by (simp add: *) qed lemma (in measure_space) integral_minus[intro, simp]: assumes "integrable f" shows "integrable (\x. - f x)" "integral (\x. - f x) = - integral f" using assms by (auto simp: integrable_def integral_def) lemma (in measure_space) integral_of_positive_diff: assumes integrable: "integrable u" "integrable v" and f_def: "\x. f x = u x - v x" and pos: "\x. 0 \ u x" "\x. 0 \ v x" shows "integrable f" and "integral f = integral u - integral v" proof - let ?PI = positive_integral let "?f x" = "Real (f x)" let "?mf x" = "Real (- f x)" let "?u x" = "Real (u x)" let "?v x" = "Real (v x)" from borel_measurable_diff[of u v] integrable have f_borel: "?f \ borel_measurable M" and mf_borel: "?mf \ borel_measurable M" and v_borel: "?v \ borel_measurable M" and u_borel: "?u \ borel_measurable M" and "f \ borel_measurable M" by (auto simp: f_def[symmetric] integrable_def) have "?PI (\x. Real (u x - v x)) \ ?PI ?u" using pos by (auto intro!: positive_integral_mono) moreover have "?PI (\x. Real (v x - u x)) \ ?PI ?v" using pos by (auto intro!: positive_integral_mono) ultimately show f: "integrable f" using `integrable u` `integrable v` `f \ borel_measurable M` by (auto simp: integrable_def f_def) hence mf: "integrable (\x. - f x)" .. have *: "\x. Real (- v x) = 0" "\x. Real (- u x) = 0" using pos by auto have "\x. ?u x + ?mf x = ?v x + ?f x" unfolding f_def using pos by simp hence "?PI (\x. ?u x + ?mf x) = ?PI (\x. ?v x + ?f x)" by simp hence "real (?PI ?u + ?PI ?mf) = real (?PI ?v + ?PI ?f)" using positive_integral_add[OF u_borel mf_borel] using positive_integral_add[OF v_borel f_borel] by auto then show "integral f = integral u - integral v" using f mf `integrable u` `integrable v` unfolding integral_def integrable_def * by (cases "?PI ?f", cases "?PI ?mf", cases "?PI ?v", cases "?PI ?u") (auto simp add: field_simps) qed lemma (in measure_space) integral_linear: assumes "integrable f" "integrable g" and "0 \ a" shows "integrable (\t. a * f t + g t)" and "integral (\t. a * f t + g t) = a * integral f + integral g" proof - let ?PI = positive_integral let "?f x" = "Real (f x)" let "?g x" = "Real (g x)" let "?mf x" = "Real (- f x)" let "?mg x" = "Real (- g x)" let "?p t" = "max 0 (a * f t) + max 0 (g t)" let "?n t" = "max 0 (- (a * f t)) + max 0 (- g t)" have pos: "?f \ borel_measurable M" "?g \ borel_measurable M" and neg: "?mf \ borel_measurable M" "?mg \ borel_measurable M" and p: "?p \ borel_measurable M" and n: "?n \ borel_measurable M" using assms by (simp_all add: integrable_def) have *: "\x. Real (?p x) = Real a * ?f x + ?g x" "\x. Real (?n x) = Real a * ?mf x + ?mg x" "\x. Real (- ?p x) = 0" "\x. Real (- ?n x) = 0" using `0 \ a` by (auto simp: max_def min_def zero_le_mult_iff mult_le_0_iff add_nonpos_nonpos) note linear = positive_integral_linear[OF pos] positive_integral_linear[OF neg] have "integrable ?p" "integrable ?n" "\t. a * f t + g t = ?p t - ?n t" "\t. 0 \ ?p t" "\t. 0 \ ?n t" using assms p n unfolding integrable_def * linear by auto note diff = integral_of_positive_diff[OF this] show "integrable (\t. a * f t + g t)" by (rule diff) from assms show "integral (\t. a * f t + g t) = a * integral f + integral g" unfolding diff(2) unfolding integral_def * linear integrable_def by (cases "?PI ?f", cases "?PI ?mf", cases "?PI ?g", cases "?PI ?mg") (auto simp add: field_simps zero_le_mult_iff) qed lemma (in measure_space) integral_add[simp, intro]: assumes "integrable f" "integrable g" shows "integrable (\t. f t + g t)" and "integral (\t. f t + g t) = integral f + integral g" using assms integral_linear[where a=1] by auto lemma (in measure_space) integral_zero[simp, intro]: shows "integrable (\x. 0)" and "integral (\x. 0) = 0" unfolding integrable_def integral_def by (auto simp add: borel_measurable_const) lemma (in measure_space) integral_cmult[simp, intro]: assumes "integrable f" shows "integrable (\t. a * f t)" (is ?P) and "integral (\t. a * f t) = a * integral f" (is ?I) proof - have "integrable (\t. a * f t) \ integral (\t. a * f t) = a * integral f" proof (cases rule: le_cases) assume "0 \ a" show ?thesis using integral_linear[OF assms integral_zero(1) `0 \ a`] by (simp add: integral_zero) next assume "a \ 0" hence "0 \ - a" by auto have *: "\t. - a * t + 0 = (-a) * t" by simp show ?thesis using integral_linear[OF assms integral_zero(1) `0 \ - a`] integral_minus(1)[of "\t. - a * f t"] unfolding * integral_zero by simp qed thus ?P ?I by auto qed lemma (in measure_space) integral_mono_AE: assumes fg: "integrable f" "integrable g" and mono: "AE t. f t \ g t" shows "integral f \ integral g" proof - have "AE x. Real (f x) \ Real (g x)" using mono by (rule AE_mp) (auto intro!: AE_cong) moreover have "AE x. Real (- g x) \ Real (- f x)" using mono by (rule AE_mp) (auto intro!: AE_cong) ultimately show ?thesis using fg by (auto simp: integral_def integrable_def diff_minus intro!: add_mono real_of_pinfreal_mono positive_integral_mono_AE) qed lemma (in measure_space) integral_mono: assumes fg: "integrable f" "integrable g" and mono: "\t. t \ space M \ f t \ g t" shows "integral f \ integral g" apply (rule integral_mono_AE[OF fg]) using mono by (rule AE_cong) auto lemma (in measure_space) integral_diff[simp, intro]: assumes f: "integrable f" and g: "integrable g" shows "integrable (\t. f t - g t)" and "integral (\t. f t - g t) = integral f - integral g" using integral_add[OF f integral_minus(1)[OF g]] unfolding diff_minus integral_minus(2)[OF g] by auto lemma (in measure_space) integral_indicator[simp, intro]: assumes "a \ sets M" and "\ a \ \" shows "integral (indicator a) = real (\ a)" (is ?int) and "integrable (indicator a)" (is ?able) proof - have *: "\A x. Real (indicator A x) = indicator A x" "\A x. Real (- indicator A x) = 0" unfolding indicator_def by auto show ?int ?able using assms unfolding integral_def integrable_def by (auto simp: * positive_integral_indicator borel_measurable_indicator) qed lemma (in measure_space) integral_cmul_indicator: assumes "A \ sets M" and "c \ 0 \ \ A \ \" shows "integrable (\x. c * indicator A x)" (is ?P) and "integral (\x. c * indicator A x) = c * real (\ A)" (is ?I) proof - show ?P proof (cases "c = 0") case False with assms show ?thesis by simp qed simp show ?I proof (cases "c = 0") case False with assms show ?thesis by simp qed simp qed lemma (in measure_space) integral_setsum[simp, intro]: assumes "\n. n \ S \ integrable (f n)" shows "integral (\x. \ i \ S. f i x) = (\ i \ S. integral (f i))" (is "?int S") and "integrable (\x. \ i \ S. f i x)" (is "?I S") proof - have "?int S \ ?I S" proof (cases "finite S") assume "finite S" from this assms show ?thesis by (induct S) simp_all qed simp thus "?int S" and "?I S" by auto qed lemma (in measure_space) integrable_abs: assumes "integrable f" shows "integrable (\ x. \f x\)" proof - have *: "\x. Real \f x\ = Real (f x) + Real (- f x)" "\x. Real (- \f x\) = 0" by auto have abs: "(\x. \f x\) \ borel_measurable M" and f: "(\x. Real (f x)) \ borel_measurable M" "(\x. Real (- f x)) \ borel_measurable M" using assms unfolding integrable_def by auto from abs assms show ?thesis unfolding integrable_def * using positive_integral_linear[OF f, of 1] by simp qed lemma (in measure_space) integrable_bound: assumes "integrable f" and f: "\x. x \ space M \ 0 \ f x" "\x. x \ space M \ \g x\ \ f x" assumes borel: "g \ borel_measurable M" shows "integrable g" proof - have "positive_integral (\x. Real (g x)) \ positive_integral (\x. Real \g x\)" by (auto intro!: positive_integral_mono) also have "\ \ positive_integral (\x. Real (f x))" using f by (auto intro!: positive_integral_mono) also have "\ < \" using `integrable f` unfolding integrable_def by (auto simp: pinfreal_less_\) finally have pos: "positive_integral (\x. Real (g x)) < \" . have "positive_integral (\x. Real (- g x)) \ positive_integral (\x. Real (\g x\))" by (auto intro!: positive_integral_mono) also have "\ \ positive_integral (\x. Real (f x))" using f by (auto intro!: positive_integral_mono) also have "\ < \" using `integrable f` unfolding integrable_def by (auto simp: pinfreal_less_\) finally have neg: "positive_integral (\x. Real (- g x)) < \" . from neg pos borel show ?thesis unfolding integrable_def by auto qed lemma (in measure_space) integrable_abs_iff: "f \ borel_measurable M \ integrable (\ x. \f x\) \ integrable f" by (auto intro!: integrable_bound[where g=f] integrable_abs) lemma (in measure_space) integrable_max: assumes int: "integrable f" "integrable g" shows "integrable (\ x. max (f x) (g x))" proof (rule integrable_bound) show "integrable (\x. \f x\ + \g x\)" using int by (simp add: integrable_abs) show "(\x. max (f x) (g x)) \ borel_measurable M" using int unfolding integrable_def by auto next fix x assume "x \ space M" show "0 \ \f x\ + \g x\" "\max (f x) (g x)\ \ \f x\ + \g x\" by auto qed lemma (in measure_space) integrable_min: assumes int: "integrable f" "integrable g" shows "integrable (\ x. min (f x) (g x))" proof (rule integrable_bound) show "integrable (\x. \f x\ + \g x\)" using int by (simp add: integrable_abs) show "(\x. min (f x) (g x)) \ borel_measurable M" using int unfolding integrable_def by auto next fix x assume "x \ space M" show "0 \ \f x\ + \g x\" "\min (f x) (g x)\ \ \f x\ + \g x\" by auto qed lemma (in measure_space) integral_triangle_inequality: assumes "integrable f" shows "\integral f\ \ integral (\x. \f x\)" proof - have "\integral f\ = max (integral f) (- integral f)" by auto also have "\ \ integral (\x. \f x\)" using assms integral_minus(2)[of f, symmetric] by (auto intro!: integral_mono integrable_abs simp del: integral_minus) finally show ?thesis . qed lemma (in measure_space) integral_positive: assumes "integrable f" "\x. x \ space M \ 0 \ f x" shows "0 \ integral f" proof - have "0 = integral (\x. 0)" by (auto simp: integral_zero) also have "\ \ integral f" using assms by (rule integral_mono[OF integral_zero(1)]) finally show ?thesis . qed lemma (in measure_space) integral_monotone_convergence_pos: assumes i: "\i. integrable (f i)" and mono: "\x. mono (\n. f n x)" and pos: "\x i. 0 \ f i x" and lim: "\x. (\i. f i x) ----> u x" and ilim: "(\i. integral (f i)) ----> x" shows "integrable u" and "integral u = x" proof - { fix x have "0 \ u x" using mono pos[of 0 x] incseq_le[OF _ lim, of x 0] by (simp add: mono_def incseq_def) } note pos_u = this hence [simp]: "\i x. Real (- f i x) = 0" "\x. Real (- u x) = 0" using pos by auto have SUP_F: "\x. (SUP n. Real (f n x)) = Real (u x)" using mono pos pos_u lim by (rule SUP_eq_LIMSEQ[THEN iffD2]) have borel_f: "\i. (\x. Real (f i x)) \ borel_measurable M" using i unfolding integrable_def by auto hence "(SUP i. (\x. Real (f i x))) \ borel_measurable M" by auto hence borel_u: "u \ borel_measurable M" using pos_u by (auto simp: borel_measurable_Real_eq SUPR_fun_expand SUP_F) have integral_eq: "\n. positive_integral (\x. Real (f n x)) = Real (integral (f n))" using i unfolding integral_def integrable_def by (auto simp: Real_real) have pos_integral: "\n. 0 \ integral (f n)" using pos i by (auto simp: integral_positive) hence "0 \ x" using LIMSEQ_le_const[OF ilim, of 0] by auto have "(\i. positive_integral (\x. Real (f i x))) \ positive_integral (\x. Real (u x))" proof (rule positive_integral_isoton) from SUP_F mono pos show "(\i x. Real (f i x)) \ (\x. Real (u x))" unfolding isoton_fun_expand by (auto simp: isoton_def mono_def) qed (rule borel_f) hence pI: "positive_integral (\x. Real (u x)) = (SUP n. positive_integral (\x. Real (f n x)))" unfolding isoton_def by simp also have "\ = Real x" unfolding integral_eq proof (rule SUP_eq_LIMSEQ[THEN iffD2]) show "mono (\n. integral (f n))" using mono i by (auto simp: mono_def intro!: integral_mono) show "\n. 0 \ integral (f n)" using pos_integral . show "0 \ x" using `0 \ x` . show "(\n. integral (f n)) ----> x" using ilim . qed finally show "integrable u" "integral u = x" using borel_u `0 \ x` unfolding integrable_def integral_def by auto qed lemma (in measure_space) integral_monotone_convergence: assumes f: "\i. integrable (f i)" and "mono f" and lim: "\x. (\i. f i x) ----> u x" and ilim: "(\i. integral (f i)) ----> x" shows "integrable u" and "integral u = x" proof - have 1: "\i. integrable (\x. f i x - f 0 x)" using f by (auto intro!: integral_diff) have 2: "\x. mono (\n. f n x - f 0 x)" using `mono f` unfolding mono_def le_fun_def by auto have 3: "\x n. 0 \ f n x - f 0 x" using `mono f` unfolding mono_def le_fun_def by (auto simp: field_simps) have 4: "\x. (\i. f i x - f 0 x) ----> u x - f 0 x" using lim by (auto intro!: LIMSEQ_diff) have 5: "(\i. integral (\x. f i x - f 0 x)) ----> x - integral (f 0)" using f ilim by (auto intro!: LIMSEQ_diff simp: integral_diff) note diff = integral_monotone_convergence_pos[OF 1 2 3 4 5] have "integrable (\x. (u x - f 0 x) + f 0 x)" using diff(1) f by (rule integral_add(1)) with diff(2) f show "integrable u" "integral u = x" by (auto simp: integral_diff) qed lemma (in measure_space) integral_0_iff: assumes "integrable f" shows "integral (\x. \f x\) = 0 \ \ {x\space M. f x \ 0} = 0" proof - have *: "\x. Real (- \f x\) = 0" by auto have "integrable (\x. \f x\)" using assms by (rule integrable_abs) hence "(\x. Real (\f x\)) \ borel_measurable M" "positive_integral (\x. Real \f x\) \ \" unfolding integrable_def by auto from positive_integral_0_iff[OF this(1)] this(2) show ?thesis unfolding integral_def * by (simp add: real_of_pinfreal_eq_0) qed lemma (in measure_space) positive_integral_omega: assumes "f \ borel_measurable M" and "positive_integral f \ \" shows "\ (f -` {\} \ space M) = 0" proof - have "\ * \ (f -` {\} \ space M) = positive_integral (\x. \ * indicator (f -` {\} \ space M) x)" using positive_integral_cmult_indicator[OF borel_measurable_vimage, OF assms(1), of \ \] by simp also have "\ \ positive_integral f" by (auto intro!: positive_integral_mono simp: indicator_def) finally show ?thesis using assms(2) by (cases ?thesis) auto qed lemma (in measure_space) simple_integral_omega: assumes "simple_function f" and "simple_integral f \ \" shows "\ (f -` {\} \ space M) = 0" proof (rule positive_integral_omega) show "f \ borel_measurable M" using assms by (auto intro: borel_measurable_simple_function) show "positive_integral f \ \" using assms by (simp add: positive_integral_eq_simple_integral) qed lemma (in measure_space) integral_dominated_convergence: assumes u: "\i. integrable (u i)" and bound: "\x j. x\space M \ \u j x\ \ w x" and w: "integrable w" "\x. x \ space M \ 0 \ w x" and u': "\x. x \ space M \ (\i. u i x) ----> u' x" shows "integrable u'" and "(\i. integral (\x. \u i x - u' x\)) ----> 0" (is "?lim_diff") and "(\i. integral (u i)) ----> integral u'" (is ?lim) proof - { fix x j assume x: "x \ space M" from u'[OF x] have "(\i. \u i x\) ----> \u' x\" by (rule LIMSEQ_imp_rabs) from LIMSEQ_le_const2[OF this] have "\u' x\ \ w x" using bound[OF x] by auto } note u'_bound = this from u[unfolded integrable_def] have u'_borel: "u' \ borel_measurable M" using u' by (blast intro: borel_measurable_LIMSEQ[of u]) show "integrable u'" proof (rule integrable_bound) show "integrable w" by fact show "u' \ borel_measurable M" by fact next fix x assume x: "x \ space M" thus "0 \ w x" by fact show "\u' x\ \ w x" using u'_bound[OF x] . qed let "?diff n x" = "2 * w x - \u n x - u' x\" have diff: "\n. integrable (\x. \u n x - u' x\)" using w u `integrable u'` by (auto intro!: integral_add integral_diff integral_cmult integrable_abs) { fix j x assume x: "x \ space M" have "\u j x - u' x\ \ \u j x\ + \u' x\" by auto also have "\ \ w x + w x" by (rule add_mono[OF bound[OF x] u'_bound[OF x]]) finally have "\u j x - u' x\ \ 2 * w x" by simp } note diff_less_2w = this have PI_diff: "\m n. positive_integral (\x. Real (?diff (m + n) x)) = positive_integral (\x. Real (2 * w x)) - positive_integral (\x. Real \u (m + n) x - u' x\)" using diff w diff_less_2w by (subst positive_integral_diff[symmetric]) (auto simp: integrable_def intro!: positive_integral_cong) have "integrable (\x. 2 * w x)" using w by (auto intro: integral_cmult) hence I2w_fin: "positive_integral (\x. Real (2 * w x)) \ \" and borel_2w: "(\x. Real (2 * w x)) \ borel_measurable M" unfolding integrable_def by auto have "(INF n. SUP m. positive_integral (\x. Real \u (m + n) x - u' x\)) = 0" (is "?lim_SUP = 0") proof cases assume eq_0: "positive_integral (\x. Real (2 * w x)) = 0" have "\i. positive_integral (\x. Real \u i x - u' x\) \ positive_integral (\x. Real (2 * w x))" proof (rule positive_integral_mono) fix i x assume "x \ space M" from diff_less_2w[OF this, of i] show "Real \u i x - u' x\ \ Real (2 * w x)" by auto qed hence "\i. positive_integral (\x. Real \u i x - u' x\) = 0" using eq_0 by auto thus ?thesis by simp next assume neq_0: "positive_integral (\x. Real (2 * w x)) \ 0" have "positive_integral (\x. Real (2 * w x)) = positive_integral (SUP n. INF m. (\x. Real (?diff (m + n) x)))" proof (rule positive_integral_cong, unfold SUPR_fun_expand INFI_fun_expand, subst add_commute) fix x assume x: "x \ space M" show "Real (2 * w x) = (SUP n. INF m. Real (?diff (n + m) x))" proof (rule LIMSEQ_imp_lim_INF[symmetric]) fix j show "0 \ ?diff j x" using diff_less_2w[OF x, of j] by simp next have "(\i. ?diff i x) ----> 2 * w x - \u' x - u' x\" using u'[OF x] by (safe intro!: LIMSEQ_diff LIMSEQ_const LIMSEQ_imp_rabs) thus "(\i. ?diff i x) ----> 2 * w x" by simp qed qed also have "\ \ (SUP n. INF m. positive_integral (\x. Real (?diff (m + n) x)))" using u'_borel w u unfolding integrable_def by (auto intro!: positive_integral_lim_INF) also have "\ = positive_integral (\x. Real (2 * w x)) - (INF n. SUP m. positive_integral (\x. Real \u (m + n) x - u' x\))" unfolding PI_diff pinfreal_INF_minus[OF I2w_fin] pinfreal_SUP_minus .. finally show ?thesis using neq_0 I2w_fin by (rule pinfreal_le_minus_imp_0) qed have [simp]: "\n m x. Real (- \u (m + n) x - u' x\) = 0" by auto have [simp]: "\n m. positive_integral (\x. Real \u (m + n) x - u' x\) = Real (integral (\x. \u (n + m) x - u' x\))" using diff by (subst add_commute) (simp add: integral_def integrable_def Real_real) have "(SUP n. INF m. positive_integral (\x. Real \u (m + n) x - u' x\)) \ ?lim_SUP" (is "?lim_INF \ _") by (subst (1 2) add_commute) (rule lim_INF_le_lim_SUP) hence "?lim_INF = Real 0" "?lim_SUP = Real 0" using `?lim_SUP = 0` by auto thus ?lim_diff using diff by (auto intro!: integral_positive lim_INF_eq_lim_SUP) show ?lim proof (rule LIMSEQ_I) fix r :: real assume "0 < r" from LIMSEQ_D[OF `?lim_diff` this] obtain N where N: "\n. N \ n \ integral (\x. \u n x - u' x\) < r" using diff by (auto simp: integral_positive) show "\N. \n\N. norm (integral (u n) - integral u') < r" proof (safe intro!: exI[of _ N]) fix n assume "N \ n" have "\integral (u n) - integral u'\ = \integral (\x. u n x - u' x)\" using u `integrable u'` by (auto simp: integral_diff) also have "\ \ integral (\x. \u n x - u' x\)" using u `integrable u'` by (rule_tac integral_triangle_inequality) (auto intro!: integral_diff) also note N[OF `N \ n`] finally show "norm (integral (u n) - integral u') < r" by simp qed qed qed lemma (in measure_space) integral_sums: assumes borel: "\i. integrable (f i)" and summable: "\x. x \ space M \ summable (\i. \f i x\)" and sums: "summable (\i. integral (\x. \f i x\))" shows "integrable (\x. (\i. f i x))" (is "integrable ?S") and "(\i. integral (f i)) sums integral (\x. (\i. f i x))" (is ?integral) proof - have "\x\space M. \w. (\i. \f i x\) sums w" using summable unfolding summable_def by auto from bchoice[OF this] obtain w where w: "\x. x \ space M \ (\i. \f i x\) sums w x" by auto let "?w y" = "if y \ space M then w y else 0" obtain x where abs_sum: "(\i. integral (\x. \f i x\)) sums x" using sums unfolding summable_def .. have 1: "\n. integrable (\x. \i = 0.. space M" have "\\i = 0..< j. f i x\ \ (\i = 0..< j. \f i x\)" by (rule setsum_abs) also have "\ \ w x" using w[of x] series_pos_le[of "\i. \f i x\"] unfolding sums_iff by auto finally have "\\i = 0.. \ ?w x" by simp } note 2 = this have 3: "integrable ?w" proof (rule integral_monotone_convergence(1)) let "?F n y" = "(\i = 0..f i y\)" let "?w' n y" = "if y \ space M then ?F n y else 0" have "\n. integrable (?F n)" using borel by (auto intro!: integral_setsum integrable_abs) thus "\n. integrable (?w' n)" by (simp cong: integrable_cong) show "mono ?w'" by (auto simp: mono_def le_fun_def intro!: setsum_mono2) { fix x show "(\n. ?w' n x) ----> ?w x" using w by (cases "x \ space M") (simp_all add: LIMSEQ_const sums_def) } have *: "\n. integral (?w' n) = (\i = 0..< n. integral (\x. \f i x\))" using borel by (simp add: integral_setsum integrable_abs cong: integral_cong) from abs_sum show "(\i. integral (?w' i)) ----> x" unfolding * sums_def . qed have 4: "\x. x \ space M \ 0 \ ?w x" using 2[of _ 0] by simp from summable[THEN summable_rabs_cancel] have 5: "\x. x \ space M \ (\n. \i = 0.. (\i. f i x)" by (auto intro: summable_sumr_LIMSEQ_suminf) note int = integral_dominated_convergence(1,3)[OF 1 2 3 4 5] from int show "integrable ?S" by simp show ?integral unfolding sums_def integral_setsum(1)[symmetric, OF borel] using int(2) by simp qed section "Lebesgue integration on countable spaces" lemma (in measure_space) integral_on_countable: assumes f: "f \ borel_measurable M" and bij: "bij_betw enum S (f ` space M)" and enum_zero: "enum ` (-S) \ {0}" and fin: "\x. x \ 0 \ \ (f -` {x} \ space M) \ \" and abs_summable: "summable (\r. \enum r * real (\ (f -` {enum r} \ space M))\)" shows "integrable f" and "(\r. enum r * real (\ (f -` {enum r} \ space M))) sums integral f" (is ?sums) proof - let "?A r" = "f -` {enum r} \ space M" let "?F r x" = "enum r * indicator (?A r) x" have enum_eq: "\r. enum r * real (\ (?A r)) = integral (?F r)" using f fin by (simp add: borel_measurable_vimage integral_cmul_indicator) { fix x assume "x \ space M" hence "f x \ enum ` S" using bij unfolding bij_betw_def by auto then obtain i where "i\S" "enum i = f x" by auto have F: "\j. ?F j x = (if j = i then f x else 0)" proof cases fix j assume "j = i" thus "?thesis j" using `x \ space M` `enum i = f x` by (simp add: indicator_def) next fix j assume "j \ i" show "?thesis j" using bij `i \ S` `j \ i` `enum i = f x` enum_zero by (cases "j \ S") (auto simp add: indicator_def bij_betw_def inj_on_def) qed hence F_abs: "\j. \if j = i then f x else 0\ = (if j = i then \f x\ else 0)" by auto have "(\i. ?F i x) sums f x" "(\i. \?F i x\) sums \f x\" by (auto intro!: sums_single simp: F F_abs) } note F_sums_f = this(1) and F_abs_sums_f = this(2) have int_f: "integral f = integral (\x. \r. ?F r x)" "integrable f = integrable (\x. \r. ?F r x)" using F_sums_f by (auto intro!: integral_cong integrable_cong simp: sums_iff) { fix r have "integral (\x. \?F r x\) = integral (\x. \enum r\ * indicator (?A r) x)" by (auto simp: indicator_def intro!: integral_cong) also have "\ = \enum r\ * real (\ (?A r))" using f fin by (simp add: borel_measurable_vimage integral_cmul_indicator) finally have "integral (\x. \?F r x\) = \enum r * real (\ (?A r))\" by (simp add: abs_mult_pos real_pinfreal_pos) } note int_abs_F = this have 1: "\i. integrable (\x. ?F i x)" using f fin by (simp add: borel_measurable_vimage integral_cmul_indicator) have 2: "\x. x \ space M \ summable (\i. \?F i x\)" using F_abs_sums_f unfolding sums_iff by auto from integral_sums(2)[OF 1 2, unfolded int_abs_F, OF _ abs_summable] show ?sums unfolding enum_eq int_f by simp from integral_sums(1)[OF 1 2, unfolded int_abs_F, OF _ abs_summable] show "integrable f" unfolding int_f by simp qed section "Lebesgue integration on finite space" lemma (in measure_space) integral_on_finite: assumes f: "f \ borel_measurable M" and finite: "finite (f`space M)" and fin: "\x. x \ 0 \ \ (f -` {x} \ space M) \ \" shows "integrable f" and "integral (\x. f x) = (\ r \ f`space M. r * real (\ (f -` {r} \ space M)))" (is "?integral") proof - let "?A r" = "f -` {r} \ space M" let "?S x" = "\r\f`space M. r * indicator (?A r) x" { fix x assume "x \ space M" have "f x = (\r\f`space M. if x \ ?A r then r else 0)" using finite `x \ space M` by (simp add: setsum_cases) also have "\ = ?S x" by (auto intro!: setsum_cong) finally have "f x = ?S x" . } note f_eq = this have f_eq_S: "integrable f \ integrable ?S" "integral f = integral ?S" by (auto intro!: integrable_cong integral_cong simp only: f_eq) show "integrable f" ?integral using fin f f_eq_S by (simp_all add: integral_cmul_indicator borel_measurable_vimage) qed lemma (in finite_measure_space) simple_function_finite[simp, intro]: "simple_function f" unfolding simple_function_def using finite_space by auto lemma (in finite_measure_space) borel_measurable_finite[intro, simp]: "f \ borel_measurable M" by (auto intro: borel_measurable_simple_function) lemma (in finite_measure_space) positive_integral_finite_eq_setsum: "positive_integral f = (\x \ space M. f x * \ {x})" proof - have *: "positive_integral f = positive_integral (\x. \y\space M. f y * indicator {y} x)" by (auto intro!: positive_integral_cong simp add: indicator_def if_distrib setsum_cases[OF finite_space]) show ?thesis unfolding * using borel_measurable_finite[of f] by (simp add: positive_integral_setsum positive_integral_cmult_indicator) qed lemma (in finite_measure_space) integral_finite_singleton: shows "integrable f" and "integral f = (\x \ space M. f x * real (\ {x}))" (is ?I) proof - have [simp]: "positive_integral (\x. Real (f x)) = (\x \ space M. Real (f x) * \ {x})" "positive_integral (\x. Real (- f x)) = (\x \ space M. Real (- f x) * \ {x})" unfolding positive_integral_finite_eq_setsum by auto show "integrable f" using finite_space finite_measure by (simp add: setsum_\ integrable_def) show ?I using finite_measure apply (simp add: integral_def real_of_pinfreal_setsum[symmetric] real_of_pinfreal_mult[symmetric] setsum_subtractf[symmetric]) by (rule setsum_cong) (simp_all split: split_if) qed end