38656

1 
(* Author: Armin Heller, Johannes Hoelzl, TU Muenchen *)


2 

35582

3 
header {*Lebesgue Integration*}


4 

38656

5 
theory Lebesgue_Integration

35582

6 
imports Measure Borel


7 
begin


8 

38656

9 
section "@{text \<mu>}null sets"

35582

10 

38656

11 
abbreviation (in measure_space) "null_sets \<equiv> {N\<in>sets M. \<mu> N = 0}"

35582

12 

38656

13 
lemma sums_If_finite:


14 
assumes finite: "finite {r. P r}"


15 
shows "(\<lambda>r. if P r then f r else 0) sums (\<Sum>r\<in>{r. P r}. f r)" (is "?F sums _")


16 
proof cases


17 
assume "{r. P r} = {}" hence "\<And>r. \<not> P r" by auto


18 
thus ?thesis by (simp add: sums_zero)


19 
next


20 
assume not_empty: "{r. P r} \<noteq> {}"


21 
have "?F sums (\<Sum>r = 0..< Suc (Max {r. P r}). ?F r)"


22 
by (rule series_zero)


23 
(auto simp add: Max_less_iff[OF finite not_empty] less_eq_Suc_le[symmetric])


24 
also have "(\<Sum>r = 0..< Suc (Max {r. P r}). ?F r) = (\<Sum>r\<in>{r. P r}. f r)"


25 
by (subst setsum_cases)


26 
(auto intro!: setsum_cong simp: Max_ge_iff[OF finite not_empty] less_Suc_eq_le)


27 
finally show ?thesis .


28 
qed

35582

29 

38656

30 
lemma sums_single:


31 
"(\<lambda>r. if r = i then f r else 0) sums f i"


32 
using sums_If_finite[of "\<lambda>r. r = i" f] by simp


33 


34 
section "Simple function"

35582

35 

38656

36 
text {*


37 


38 
Our simple functions are not restricted to positive real numbers. Instead


39 
they are just functions with a finite range and are measurable when singleton


40 
sets are measurable.

35582

41 

38656

42 
*}


43 


44 
definition (in sigma_algebra) "simple_function g \<longleftrightarrow>


45 
finite (g ` space M) \<and>


46 
(\<forall>x \<in> g ` space M. g ` {x} \<inter> space M \<in> sets M)"

36624

47 

38656

48 
lemma (in sigma_algebra) simple_functionD:


49 
assumes "simple_function g"


50 
shows "finite (g ` space M)"


51 
"x \<in> g ` space M \<Longrightarrow> g ` {x} \<inter> space M \<in> sets M"


52 
using assms unfolding simple_function_def by auto

36624

53 

38656

54 
lemma (in sigma_algebra) simple_function_indicator_representation:


55 
fixes f ::"'a \<Rightarrow> pinfreal"


56 
assumes f: "simple_function f" and x: "x \<in> space M"


57 
shows "f x = (\<Sum>y \<in> f ` space M. y * indicator (f ` {y} \<inter> space M) x)"


58 
(is "?l = ?r")


59 
proof 


60 
have "?r = (\<Sum>y \<in> f ` space M.


61 
(if y = f x then y * indicator (f ` {y} \<inter> space M) x else 0))"


62 
by (auto intro!: setsum_cong2)


63 
also have "... = f x * indicator (f ` {f x} \<inter> space M) x"


64 
using assms by (auto dest: simple_functionD simp: setsum_delta)


65 
also have "... = f x" using x by (auto simp: indicator_def)


66 
finally show ?thesis by auto


67 
qed

36624

68 

38656

69 
lemma (in measure_space) simple_function_notspace:


70 
"simple_function (\<lambda>x. h x * indicator ( space M) x::pinfreal)" (is "simple_function ?h")

35692

71 
proof 

38656

72 
have "?h ` space M \<subseteq> {0}" unfolding indicator_def by auto


73 
hence [simp, intro]: "finite (?h ` space M)" by (auto intro: finite_subset)


74 
have "?h ` {0} \<inter> space M = space M" by auto


75 
thus ?thesis unfolding simple_function_def by auto


76 
qed


77 


78 
lemma (in sigma_algebra) simple_function_cong:


79 
assumes "\<And>t. t \<in> space M \<Longrightarrow> f t = g t"


80 
shows "simple_function f \<longleftrightarrow> simple_function g"


81 
proof 


82 
have "f ` space M = g ` space M"


83 
"\<And>x. f ` {x} \<inter> space M = g ` {x} \<inter> space M"


84 
using assms by (auto intro!: image_eqI)


85 
thus ?thesis unfolding simple_function_def using assms by simp


86 
qed


87 


88 
lemma (in sigma_algebra) borel_measurable_simple_function:


89 
assumes "simple_function f"


90 
shows "f \<in> borel_measurable M"


91 
proof (rule borel_measurableI)


92 
fix S


93 
let ?I = "f ` (f ` S \<inter> space M)"


94 
have *: "(\<Union>x\<in>?I. f ` {x} \<inter> space M) = f ` S \<inter> space M" (is "?U = _") by auto


95 
have "finite ?I"


96 
using assms unfolding simple_function_def by (auto intro: finite_subset)


97 
hence "?U \<in> sets M"


98 
apply (rule finite_UN)


99 
using assms unfolding simple_function_def by auto


100 
thus "f ` S \<inter> space M \<in> sets M" unfolding * .

35692

101 
qed


102 

38656

103 
lemma (in sigma_algebra) simple_function_borel_measurable:


104 
fixes f :: "'a \<Rightarrow> 'x::t2_space"


105 
assumes "f \<in> borel_measurable M" and "finite (f ` space M)"


106 
shows "simple_function f"


107 
using assms unfolding simple_function_def


108 
by (auto intro: borel_measurable_vimage)


109 


110 
lemma (in sigma_algebra) simple_function_const[intro, simp]:


111 
"simple_function (\<lambda>x. c)"


112 
by (auto intro: finite_subset simp: simple_function_def)


113 


114 
lemma (in sigma_algebra) simple_function_compose[intro, simp]:


115 
assumes "simple_function f"


116 
shows "simple_function (g \<circ> f)"


117 
unfolding simple_function_def


118 
proof safe


119 
show "finite ((g \<circ> f) ` space M)"


120 
using assms unfolding simple_function_def by (auto simp: image_compose)


121 
next


122 
fix x assume "x \<in> space M"


123 
let ?G = "g ` {g (f x)} \<inter> (f`space M)"


124 
have *: "(g \<circ> f) ` {(g \<circ> f) x} \<inter> space M =


125 
(\<Union>x\<in>?G. f ` {x} \<inter> space M)" by auto


126 
show "(g \<circ> f) ` {(g \<circ> f) x} \<inter> space M \<in> sets M"


127 
using assms unfolding simple_function_def *


128 
by (rule_tac finite_UN) (auto intro!: finite_UN)


129 
qed


130 


131 
lemma (in sigma_algebra) simple_function_indicator[intro, simp]:


132 
assumes "A \<in> sets M"


133 
shows "simple_function (indicator A)"

35692

134 
proof 

38656

135 
have "indicator A ` space M \<subseteq> {0, 1}" (is "?S \<subseteq> _")


136 
by (auto simp: indicator_def)


137 
hence "finite ?S" by (rule finite_subset) simp


138 
moreover have " A \<inter> space M = space M  A" by auto


139 
ultimately show ?thesis unfolding simple_function_def


140 
using assms by (auto simp: indicator_def_raw)

35692

141 
qed


142 

38656

143 
lemma (in sigma_algebra) simple_function_Pair[intro, simp]:


144 
assumes "simple_function f"


145 
assumes "simple_function g"


146 
shows "simple_function (\<lambda>x. (f x, g x))" (is "simple_function ?p")


147 
unfolding simple_function_def


148 
proof safe


149 
show "finite (?p ` space M)"


150 
using assms unfolding simple_function_def


151 
by (rule_tac finite_subset[of _ "f`space M \<times> g`space M"]) auto


152 
next


153 
fix x assume "x \<in> space M"


154 
have "(\<lambda>x. (f x, g x)) ` {(f x, g x)} \<inter> space M =


155 
(f ` {f x} \<inter> space M) \<inter> (g ` {g x} \<inter> space M)"


156 
by auto


157 
with `x \<in> space M` show "(\<lambda>x. (f x, g x)) ` {(f x, g x)} \<inter> space M \<in> sets M"


158 
using assms unfolding simple_function_def by auto


159 
qed

35692

160 

38656

161 
lemma (in sigma_algebra) simple_function_compose1:


162 
assumes "simple_function f"


163 
shows "simple_function (\<lambda>x. g (f x))"


164 
using simple_function_compose[OF assms, of g]


165 
by (simp add: comp_def)

35582

166 

38656

167 
lemma (in sigma_algebra) simple_function_compose2:


168 
assumes "simple_function f" and "simple_function g"


169 
shows "simple_function (\<lambda>x. h (f x) (g x))"


170 
proof 


171 
have "simple_function ((\<lambda>(x, y). h x y) \<circ> (\<lambda>x. (f x, g x)))"


172 
using assms by auto


173 
thus ?thesis by (simp_all add: comp_def)


174 
qed

35582

175 

38656

176 
lemmas (in sigma_algebra) simple_function_add[intro, simp] = simple_function_compose2[where h="op +"]


177 
and simple_function_diff[intro, simp] = simple_function_compose2[where h="op "]


178 
and simple_function_uminus[intro, simp] = simple_function_compose[where g="uminus"]


179 
and simple_function_mult[intro, simp] = simple_function_compose2[where h="op *"]


180 
and simple_function_div[intro, simp] = simple_function_compose2[where h="op /"]


181 
and simple_function_inverse[intro, simp] = simple_function_compose[where g="inverse"]


182 


183 
lemma (in sigma_algebra) simple_function_setsum[intro, simp]:


184 
assumes "\<And>i. i \<in> P \<Longrightarrow> simple_function (f i)"


185 
shows "simple_function (\<lambda>x. \<Sum>i\<in>P. f i x)"


186 
proof cases


187 
assume "finite P" from this assms show ?thesis by induct auto


188 
qed auto

35582

189 

38656

190 
lemma (in sigma_algebra) simple_function_le_measurable:


191 
assumes "simple_function f" "simple_function g"


192 
shows "{x \<in> space M. f x \<le> g x} \<in> sets M"


193 
proof 


194 
have *: "{x \<in> space M. f x \<le> g x} =


195 
(\<Union>(F, G)\<in>f`space M \<times> g`space M.


196 
if F \<le> G then (f ` {F} \<inter> space M) \<inter> (g ` {G} \<inter> space M) else {})"


197 
apply (auto split: split_if_asm)


198 
apply (rule_tac x=x in bexI)


199 
apply (rule_tac x=x in bexI)


200 
by simp_all


201 
have **: "\<And>x y. x \<in> space M \<Longrightarrow> y \<in> space M \<Longrightarrow>


202 
(f ` {f x} \<inter> space M) \<inter> (g ` {g y} \<inter> space M) \<in> sets M"


203 
using assms unfolding simple_function_def by auto


204 
have "finite (f`space M \<times> g`space M)"


205 
using assms unfolding simple_function_def by auto


206 
thus ?thesis unfolding *


207 
apply (rule finite_UN)


208 
using assms unfolding simple_function_def


209 
by (auto intro!: **)

35582

210 
qed


211 

38656

212 
lemma setsum_indicator_disjoint_family:


213 
fixes f :: "'d \<Rightarrow> 'e::semiring_1"


214 
assumes d: "disjoint_family_on A P" and "x \<in> A j" and "finite P" and "j \<in> P"


215 
shows "(\<Sum>i\<in>P. f i * indicator (A i) x) = f j"


216 
proof 


217 
have "P \<inter> {i. x \<in> A i} = {j}"


218 
using d `x \<in> A j` `j \<in> P` unfolding disjoint_family_on_def


219 
by auto


220 
thus ?thesis


221 
unfolding indicator_def


222 
by (simp add: if_distrib setsum_cases[OF `finite P`])


223 
qed

35692

224 

38656

225 
lemma LeastI2_wellorder:


226 
fixes a :: "_ :: wellorder"


227 
assumes "P a"


228 
and "\<And>a. \<lbrakk> P a; \<forall>b. P b \<longrightarrow> a \<le> b \<rbrakk> \<Longrightarrow> Q a"


229 
shows "Q (Least P)"


230 
proof (rule LeastI2_order)


231 
show "P (Least P)" using `P a` by (rule LeastI)


232 
next


233 
fix y assume "P y" thus "Least P \<le> y" by (rule Least_le)


234 
next


235 
fix x assume "P x" "\<forall>y. P y \<longrightarrow> x \<le> y" thus "Q x" by (rule assms(2))

35582

236 
qed


237 

38656

238 
lemma (in sigma_algebra) borel_measurable_implies_simple_function_sequence:


239 
fixes u :: "'a \<Rightarrow> pinfreal"


240 
assumes u: "u \<in> borel_measurable M"


241 
shows "\<exists>f. (\<forall>i. simple_function (f i) \<and> (\<forall>x\<in>space M. f i x \<noteq> \<omega>)) \<and> f \<up> u"

35582

242 
proof 

38656

243 
have "\<exists>f. \<forall>x j. (of_nat j \<le> u x \<longrightarrow> f x j = j*2^j) \<and>


244 
(u x < of_nat j \<longrightarrow> of_nat (f x j) \<le> u x * 2^j \<and> u x * 2^j < of_nat (Suc (f x j)))"


245 
(is "\<exists>f. \<forall>x j. ?P x j (f x j)")


246 
proof(rule choice, rule, rule choice, rule)


247 
fix x j show "\<exists>n. ?P x j n"


248 
proof cases


249 
assume *: "u x < of_nat j"


250 
then obtain r where r: "u x = Real r" "0 \<le> r" by (cases "u x") auto


251 
from reals_Archimedean6a[of "r * 2^j"]


252 
obtain n :: nat where "real n \<le> r * 2 ^ j" "r * 2 ^ j < real (Suc n)"


253 
using `0 \<le> r` by (auto simp: zero_le_power zero_le_mult_iff)


254 
thus ?thesis using r * by (auto intro!: exI[of _ n])


255 
qed auto

35582

256 
qed

38656

257 
then obtain f where top: "\<And>j x. of_nat j \<le> u x \<Longrightarrow> f x j = j*2^j" and


258 
upper: "\<And>j x. u x < of_nat j \<Longrightarrow> of_nat (f x j) \<le> u x * 2^j" and


259 
lower: "\<And>j x. u x < of_nat j \<Longrightarrow> u x * 2^j < of_nat (Suc (f x j))" by blast

35582

260 

38656

261 
{ fix j x P


262 
assume 1: "of_nat j \<le> u x \<Longrightarrow> P (j * 2^j)"


263 
assume 2: "\<And>k. \<lbrakk> u x < of_nat j ; of_nat k \<le> u x * 2^j ; u x * 2^j < of_nat (Suc k) \<rbrakk> \<Longrightarrow> P k"


264 
have "P (f x j)"


265 
proof cases


266 
assume "of_nat j \<le> u x" thus "P (f x j)"


267 
using top[of j x] 1 by auto


268 
next


269 
assume "\<not> of_nat j \<le> u x"


270 
hence "u x < of_nat j" "of_nat (f x j) \<le> u x * 2^j" "u x * 2^j < of_nat (Suc (f x j))"


271 
using upper lower by auto


272 
from 2[OF this] show "P (f x j)" .


273 
qed }


274 
note fI = this


275 


276 
{ fix j x


277 
have "f x j = j * 2 ^ j \<longleftrightarrow> of_nat j \<le> u x"


278 
by (rule fI, simp, cases "u x") (auto split: split_if_asm) }


279 
note f_eq = this

35582

280 

38656

281 
{ fix j x


282 
have "f x j \<le> j * 2 ^ j"


283 
proof (rule fI)


284 
fix k assume *: "u x < of_nat j"


285 
assume "of_nat k \<le> u x * 2 ^ j"


286 
also have "\<dots> \<le> of_nat (j * 2^j)"


287 
using * by (cases "u x") (auto simp: zero_le_mult_iff)


288 
finally show "k \<le> j*2^j" by (auto simp del: real_of_nat_mult)


289 
qed simp }


290 
note f_upper = this

35582

291 

38656

292 
let "?g j x" = "of_nat (f x j) / 2^j :: pinfreal"


293 
show ?thesis unfolding simple_function_def isoton_fun_expand unfolding isoton_def


294 
proof (safe intro!: exI[of _ ?g])


295 
fix j


296 
have *: "?g j ` space M \<subseteq> (\<lambda>x. of_nat x / 2^j) ` {..j * 2^j}"


297 
using f_upper by auto


298 
thus "finite (?g j ` space M)" by (rule finite_subset) auto


299 
next


300 
fix j t assume "t \<in> space M"


301 
have **: "?g j ` {?g j t} \<inter> space M = {x \<in> space M. f t j = f x j}"


302 
by (auto simp: power_le_zero_eq Real_eq_Real mult_le_0_iff)

35582

303 

38656

304 
show "?g j ` {?g j t} \<inter> space M \<in> sets M"


305 
proof cases


306 
assume "of_nat j \<le> u t"


307 
hence "?g j ` {?g j t} \<inter> space M = {x\<in>space M. of_nat j \<le> u x}"


308 
unfolding ** f_eq[symmetric] by auto


309 
thus "?g j ` {?g j t} \<inter> space M \<in> sets M"


310 
using u by auto

35582

311 
next

38656

312 
assume not_t: "\<not> of_nat j \<le> u t"


313 
hence less: "f t j < j*2^j" using f_eq[symmetric] `f t j \<le> j*2^j` by auto


314 
have split_vimage: "?g j ` {?g j t} \<inter> space M =


315 
{x\<in>space M. of_nat (f t j)/2^j \<le> u x} \<inter> {x\<in>space M. u x < of_nat (Suc (f t j))/2^j}"


316 
unfolding **


317 
proof safe


318 
fix x assume [simp]: "f t j = f x j"


319 
have *: "\<not> of_nat j \<le> u x" using not_t f_eq[symmetric] by simp


320 
hence "of_nat (f t j) \<le> u x * 2^j \<and> u x * 2^j < of_nat (Suc (f t j))"


321 
using upper lower by auto


322 
hence "of_nat (f t j) / 2^j \<le> u x \<and> u x < of_nat (Suc (f t j))/2^j" using *


323 
by (cases "u x") (auto simp: zero_le_mult_iff power_le_zero_eq divide_real_def[symmetric] field_simps)


324 
thus "of_nat (f t j) / 2^j \<le> u x" "u x < of_nat (Suc (f t j))/2^j" by auto


325 
next


326 
fix x


327 
assume "of_nat (f t j) / 2^j \<le> u x" "u x < of_nat (Suc (f t j))/2^j"


328 
hence "of_nat (f t j) \<le> u x * 2 ^ j \<and> u x * 2 ^ j < of_nat (Suc (f t j))"


329 
by (cases "u x") (auto simp: zero_le_mult_iff power_le_zero_eq divide_real_def[symmetric] field_simps)


330 
hence 1: "of_nat (f t j) \<le> u x * 2 ^ j" and 2: "u x * 2 ^ j < of_nat (Suc (f t j))" by auto


331 
note 2


332 
also have "\<dots> \<le> of_nat (j*2^j)"


333 
using less by (auto simp: zero_le_mult_iff simp del: real_of_nat_mult)


334 
finally have bound_ux: "u x < of_nat j"


335 
by (cases "u x") (auto simp: zero_le_mult_iff power_le_zero_eq)


336 
show "f t j = f x j"


337 
proof (rule antisym)


338 
from 1 lower[OF bound_ux]


339 
show "f t j \<le> f x j" by (cases "u x") (auto split: split_if_asm)


340 
from upper[OF bound_ux] 2


341 
show "f x j \<le> f t j" by (cases "u x") (auto split: split_if_asm)


342 
qed


343 
qed


344 
show ?thesis unfolding split_vimage using u by auto

35582

345 
qed

38656

346 
next


347 
fix j t assume "?g j t = \<omega>" thus False by (auto simp: power_le_zero_eq)


348 
next


349 
fix t


350 
{ fix i


351 
have "f t i * 2 \<le> f t (Suc i)"


352 
proof (rule fI)


353 
assume "of_nat (Suc i) \<le> u t"


354 
hence "of_nat i \<le> u t" by (cases "u t") auto


355 
thus "f t i * 2 \<le> Suc i * 2 ^ Suc i" unfolding f_eq[symmetric] by simp


356 
next


357 
fix k


358 
assume *: "u t * 2 ^ Suc i < of_nat (Suc k)"


359 
show "f t i * 2 \<le> k"


360 
proof (rule fI)


361 
assume "of_nat i \<le> u t"


362 
hence "of_nat (i * 2^Suc i) \<le> u t * 2^Suc i"


363 
by (cases "u t") (auto simp: zero_le_mult_iff power_le_zero_eq)


364 
also have "\<dots> < of_nat (Suc k)" using * by auto


365 
finally show "i * 2 ^ i * 2 \<le> k"


366 
by (auto simp del: real_of_nat_mult)


367 
next


368 
fix j assume "of_nat j \<le> u t * 2 ^ i"


369 
with * show "j * 2 \<le> k" by (cases "u t") (auto simp: zero_le_mult_iff power_le_zero_eq)


370 
qed


371 
qed


372 
thus "?g i t \<le> ?g (Suc i) t"


373 
by (auto simp: zero_le_mult_iff power_le_zero_eq divide_real_def[symmetric] field_simps) }


374 
hence mono: "mono (\<lambda>i. ?g i t)" unfolding mono_iff_le_Suc by auto

35582

375 

38656

376 
show "(SUP j. of_nat (f t j) / 2 ^ j) = u t"


377 
proof (rule pinfreal_SUPI)


378 
fix j show "of_nat (f t j) / 2 ^ j \<le> u t"


379 
proof (rule fI)


380 
assume "of_nat j \<le> u t" thus "of_nat (j * 2 ^ j) / 2 ^ j \<le> u t"


381 
by (cases "u t") (auto simp: power_le_zero_eq divide_real_def[symmetric] field_simps)


382 
next


383 
fix k assume "of_nat k \<le> u t * 2 ^ j"


384 
thus "of_nat k / 2 ^ j \<le> u t"


385 
by (cases "u t")


386 
(auto simp: power_le_zero_eq divide_real_def[symmetric] field_simps zero_le_mult_iff)


387 
qed


388 
next


389 
fix y :: pinfreal assume *: "\<And>j. j \<in> UNIV \<Longrightarrow> of_nat (f t j) / 2 ^ j \<le> y"


390 
show "u t \<le> y"


391 
proof (cases "u t")


392 
case (preal r)


393 
show ?thesis


394 
proof (rule ccontr)


395 
assume "\<not> u t \<le> y"


396 
then obtain p where p: "y = Real p" "0 \<le> p" "p < r" using preal by (cases y) auto


397 
with LIMSEQ_inverse_realpow_zero[of 2, unfolded LIMSEQ_iff, rule_format, of "r  p"]


398 
obtain n where n: "\<And>N. n \<le> N \<Longrightarrow> inverse (2^N) < r  p" by auto


399 
let ?N = "max n (natfloor r + 1)"


400 
have "u t < of_nat ?N" "n \<le> ?N"


401 
using ge_natfloor_plus_one_imp_gt[of r n] preal


402 
by (auto simp: max_def real_Suc_natfloor)


403 
from lower[OF this(1)]


404 
have "r < (real (f t ?N) + 1) / 2 ^ ?N" unfolding less_divide_eq


405 
using preal by (auto simp add: power_le_zero_eq zero_le_mult_iff real_of_nat_Suc split: split_if_asm)


406 
hence "u t < of_nat (f t ?N) / 2 ^ ?N + 1 / 2 ^ ?N"


407 
using preal by (auto simp: field_simps divide_real_def[symmetric])


408 
with n[OF `n \<le> ?N`] p preal *[of ?N]


409 
show False


410 
by (cases "f t ?N") (auto simp: power_le_zero_eq split: split_if_asm)


411 
qed


412 
next


413 
case infinite


414 
{ fix j have "f t j = j*2^j" using top[of j t] infinite by simp


415 
hence "of_nat j \<le> y" using *[of j]


416 
by (cases y) (auto simp: power_le_zero_eq zero_le_mult_iff field_simps) }


417 
note all_less_y = this


418 
show ?thesis unfolding infinite


419 
proof (rule ccontr)


420 
assume "\<not> \<omega> \<le> y" then obtain r where r: "y = Real r" "0 \<le> r" by (cases y) auto


421 
moreover obtain n ::nat where "r < real n" using ex_less_of_nat by (auto simp: real_eq_of_nat)


422 
with all_less_y[of n] r show False by auto


423 
qed


424 
qed


425 
qed

35582

426 
qed


427 
qed


428 

38656

429 
lemma (in sigma_algebra) borel_measurable_implies_simple_function_sequence':


430 
fixes u :: "'a \<Rightarrow> pinfreal"


431 
assumes "u \<in> borel_measurable M"


432 
obtains (x) f where "f \<up> u" "\<And>i. simple_function (f i)" "\<And>i. \<omega>\<notin>f i`space M"

35582

433 
proof 

38656

434 
from borel_measurable_implies_simple_function_sequence[OF assms]


435 
obtain f where x: "\<And>i. simple_function (f i)" "f \<up> u"


436 
and fin: "\<And>i. \<And>x. x\<in>space M \<Longrightarrow> f i x \<noteq> \<omega>" by auto


437 
{ fix i from fin[of _ i] have "\<omega> \<notin> f i`space M" by fastsimp }


438 
with x show thesis by (auto intro!: that[of f])


439 
qed


440 


441 
section "Simple integral"


442 


443 
definition (in measure_space)


444 
"simple_integral f = (\<Sum>x \<in> f ` space M. x * \<mu> (f ` {x} \<inter> space M))"

35582

445 

38656

446 
lemma (in measure_space) simple_integral_cong:


447 
assumes "\<And>t. t \<in> space M \<Longrightarrow> f t = g t"


448 
shows "simple_integral f = simple_integral g"


449 
proof 


450 
have "f ` space M = g ` space M"


451 
"\<And>x. f ` {x} \<inter> space M = g ` {x} \<inter> space M"


452 
using assms by (auto intro!: image_eqI)


453 
thus ?thesis unfolding simple_integral_def by simp


454 
qed


455 


456 
lemma (in measure_space) simple_integral_const[simp]:


457 
"simple_integral (\<lambda>x. c) = c * \<mu> (space M)"


458 
proof (cases "space M = {}")


459 
case True thus ?thesis unfolding simple_integral_def by simp


460 
next


461 
case False hence "(\<lambda>x. c) ` space M = {c}" by auto


462 
thus ?thesis unfolding simple_integral_def by simp

35582

463 
qed


464 

38656

465 
lemma (in measure_space) simple_function_partition:


466 
assumes "simple_function f" and "simple_function g"


467 
shows "simple_integral f = (\<Sum>A\<in>(\<lambda>x. f ` {f x} \<inter> g ` {g x} \<inter> space M) ` space M. contents (f`A) * \<mu> A)"


468 
(is "_ = setsum _ (?p ` space M)")


469 
proof


470 
let "?sub x" = "?p ` (f ` {x} \<inter> space M)"


471 
let ?SIGMA = "Sigma (f`space M) ?sub"

35582

472 

38656

473 
have [intro]:


474 
"finite (f ` space M)"


475 
"finite (g ` space M)"


476 
using assms unfolding simple_function_def by simp_all


477 


478 
{ fix A


479 
have "?p ` (A \<inter> space M) \<subseteq>


480 
(\<lambda>(x,y). f ` {x} \<inter> g ` {y} \<inter> space M) ` (f`space M \<times> g`space M)"


481 
by auto


482 
hence "finite (?p ` (A \<inter> space M))"


483 
by (rule finite_subset) (auto intro: finite_SigmaI finite_imageI) }


484 
note this[intro, simp]

35582

485 

38656

486 
{ fix x assume "x \<in> space M"


487 
have "\<Union>(?sub (f x)) = (f ` {f x} \<inter> space M)" by auto


488 
moreover {


489 
fix x y


490 
have *: "f ` {f x} \<inter> g ` {g x} \<inter> space M


491 
= (f ` {f x} \<inter> space M) \<inter> (g ` {g x} \<inter> space M)" by auto


492 
assume "x \<in> space M" "y \<in> space M"


493 
hence "f ` {f x} \<inter> g ` {g x} \<inter> space M \<in> sets M"


494 
using assms unfolding simple_function_def * by auto }


495 
ultimately


496 
have "\<mu> (f ` {f x} \<inter> space M) = setsum (\<mu>) (?sub (f x))"


497 
by (subst measure_finitely_additive) auto }


498 
hence "simple_integral f = (\<Sum>(x,A)\<in>?SIGMA. x * \<mu> A)"


499 
unfolding simple_integral_def


500 
by (subst setsum_Sigma[symmetric],


501 
auto intro!: setsum_cong simp: setsum_right_distrib[symmetric])


502 
also have "\<dots> = (\<Sum>A\<in>?p ` space M. contents (f`A) * \<mu> A)"


503 
proof 


504 
have [simp]: "\<And>x. x \<in> space M \<Longrightarrow> f ` ?p x = {f x}" by (auto intro!: imageI)


505 
have "(\<lambda>A. (contents (f ` A), A)) ` ?p ` space M


506 
= (\<lambda>x. (f x, ?p x)) ` space M"


507 
proof safe


508 
fix x assume "x \<in> space M"


509 
thus "(f x, ?p x) \<in> (\<lambda>A. (contents (f`A), A)) ` ?p ` space M"


510 
by (auto intro!: image_eqI[of _ _ "?p x"])


511 
qed auto


512 
thus ?thesis


513 
apply (auto intro!: setsum_reindex_cong[of "\<lambda>A. (contents (f`A), A)"] inj_onI)


514 
apply (rule_tac x="xa" in image_eqI)


515 
by simp_all


516 
qed


517 
finally show ?thesis .

35582

518 
qed


519 

38656

520 
lemma (in measure_space) simple_integral_add[simp]:


521 
assumes "simple_function f" and "simple_function g"


522 
shows "simple_integral (\<lambda>x. f x + g x) = simple_integral f + simple_integral g"

35582

523 
proof 

38656

524 
{ fix x let ?S = "g ` {g x} \<inter> f ` {f x} \<inter> space M"


525 
assume "x \<in> space M"


526 
hence "(\<lambda>a. f a + g a) ` ?S = {f x + g x}" "f ` ?S = {f x}" "g ` ?S = {g x}"


527 
"(\<lambda>x. (f x, g x)) ` {(f x, g x)} \<inter> space M = ?S"


528 
by auto }


529 
thus ?thesis


530 
unfolding


531 
simple_function_partition[OF simple_function_add[OF assms] simple_function_Pair[OF assms]]


532 
simple_function_partition[OF `simple_function f` `simple_function g`]


533 
simple_function_partition[OF `simple_function g` `simple_function f`]


534 
apply (subst (3) Int_commute)


535 
by (auto simp add: field_simps setsum_addf[symmetric] intro!: setsum_cong)

35582

536 
qed


537 

38656

538 
lemma (in measure_space) simple_integral_setsum[simp]:


539 
assumes "\<And>i. i \<in> P \<Longrightarrow> simple_function (f i)"


540 
shows "simple_integral (\<lambda>x. \<Sum>i\<in>P. f i x) = (\<Sum>i\<in>P. simple_integral (f i))"


541 
proof cases


542 
assume "finite P"


543 
from this assms show ?thesis


544 
by induct (auto simp: simple_function_setsum simple_integral_add)


545 
qed auto


546 


547 
lemma (in measure_space) simple_integral_mult[simp]:


548 
assumes "simple_function f"


549 
shows "simple_integral (\<lambda>x. c * f x) = c * simple_integral f"


550 
proof 


551 
note mult = simple_function_mult[OF simple_function_const[of c] assms]


552 
{ fix x let ?S = "f ` {f x} \<inter> (\<lambda>x. c * f x) ` {c * f x} \<inter> space M"


553 
assume "x \<in> space M"


554 
hence "(\<lambda>x. c * f x) ` ?S = {c * f x}" "f ` ?S = {f x}"


555 
by auto }


556 
thus ?thesis


557 
unfolding simple_function_partition[OF mult assms]


558 
simple_function_partition[OF assms mult]


559 
by (auto simp: setsum_right_distrib field_simps intro!: setsum_cong)

35582

560 
qed


561 

38656

562 
lemma (in measure_space) simple_integral_mono:


563 
assumes "simple_function f" and "simple_function g"


564 
and mono: "\<And> x. x \<in> space M \<Longrightarrow> f x \<le> g x"


565 
shows "simple_integral f \<le> simple_integral g"


566 
unfolding


567 
simple_function_partition[OF `simple_function f` `simple_function g`]


568 
simple_function_partition[OF `simple_function g` `simple_function f`]


569 
apply (subst Int_commute)


570 
proof (safe intro!: setsum_mono)


571 
fix x let ?S = "g ` {g x} \<inter> f ` {f x} \<inter> space M"


572 
assume "x \<in> space M"


573 
hence "f ` ?S = {f x}" "g ` ?S = {g x}" by auto


574 
thus "contents (f`?S) * \<mu> ?S \<le> contents (g`?S) * \<mu> ?S"


575 
using mono[OF `x \<in> space M`] by (auto intro!: mult_right_mono)

35582

576 
qed


577 

38656

578 
lemma (in measure_space) simple_integral_indicator:


579 
assumes "A \<in> sets M"


580 
assumes "simple_function f"


581 
shows "simple_integral (\<lambda>x. f x * indicator A x) =


582 
(\<Sum>x \<in> f ` space M. x * \<mu> (f ` {x} \<inter> space M \<inter> A))"


583 
proof cases


584 
assume "A = space M"


585 
moreover hence "simple_integral (\<lambda>x. f x * indicator A x) = simple_integral f"


586 
by (auto intro!: simple_integral_cong)


587 
moreover have "\<And>X. X \<inter> space M \<inter> space M = X \<inter> space M" by auto


588 
ultimately show ?thesis by (simp add: simple_integral_def)


589 
next


590 
assume "A \<noteq> space M"


591 
then obtain x where x: "x \<in> space M" "x \<notin> A" using sets_into_space[OF assms(1)] by auto


592 
have I: "(\<lambda>x. f x * indicator A x) ` space M = f ` A \<union> {0}" (is "?I ` _ = _")

35582

593 
proof safe

38656

594 
fix y assume "?I y \<notin> f ` A" hence "y \<notin> A" by auto thus "?I y = 0" by auto


595 
next


596 
fix y assume "y \<in> A" thus "f y \<in> ?I ` space M"


597 
using sets_into_space[OF assms(1)] by (auto intro!: image_eqI[of _ _ y])


598 
next


599 
show "0 \<in> ?I ` space M" using x by (auto intro!: image_eqI[of _ _ x])

35582

600 
qed

38656

601 
have *: "simple_integral (\<lambda>x. f x * indicator A x) =


602 
(\<Sum>x \<in> f ` space M \<union> {0}. x * \<mu> (f ` {x} \<inter> space M \<inter> A))"


603 
unfolding simple_integral_def I


604 
proof (rule setsum_mono_zero_cong_left)


605 
show "finite (f ` space M \<union> {0})"


606 
using assms(2) unfolding simple_function_def by auto


607 
show "f ` A \<union> {0} \<subseteq> f`space M \<union> {0}"


608 
using sets_into_space[OF assms(1)] by auto


609 
have "\<And>x. f x \<notin> f ` A \<Longrightarrow> f ` {f x} \<inter> space M \<inter> A = {}" by (auto simp: image_iff)


610 
thus "\<forall>i\<in>f ` space M \<union> {0}  (f ` A \<union> {0}).


611 
i * \<mu> (f ` {i} \<inter> space M \<inter> A) = 0" by auto


612 
next


613 
fix x assume "x \<in> f`A \<union> {0}"


614 
hence "x \<noteq> 0 \<Longrightarrow> ?I ` {x} \<inter> space M = f ` {x} \<inter> space M \<inter> A"


615 
by (auto simp: indicator_def split: split_if_asm)


616 
thus "x * \<mu> (?I ` {x} \<inter> space M) =


617 
x * \<mu> (f ` {x} \<inter> space M \<inter> A)" by (cases "x = 0") simp_all


618 
qed


619 
show ?thesis unfolding *


620 
using assms(2) unfolding simple_function_def


621 
by (auto intro!: setsum_mono_zero_cong_right)


622 
qed

35582

623 

38656

624 
lemma (in measure_space) simple_integral_indicator_only[simp]:


625 
assumes "A \<in> sets M"


626 
shows "simple_integral (indicator A) = \<mu> A"


627 
proof cases


628 
assume "space M = {}" hence "A = {}" using sets_into_space[OF assms] by auto


629 
thus ?thesis unfolding simple_integral_def using `space M = {}` by auto


630 
next


631 
assume "space M \<noteq> {}" hence "(\<lambda>x. 1) ` space M = {1::pinfreal}" by auto


632 
thus ?thesis


633 
using simple_integral_indicator[OF assms simple_function_const[of 1]]


634 
using sets_into_space[OF assms]


635 
by (auto intro!: arg_cong[where f="\<mu>"])


636 
qed

35582

637 

38656

638 
lemma (in measure_space) simple_integral_null_set:


639 
assumes "simple_function u" "N \<in> null_sets"


640 
shows "simple_integral (\<lambda>x. u x * indicator N x) = 0"


641 
proof 


642 
have "simple_integral (\<lambda>x. u x * indicator N x) \<le>


643 
simple_integral (\<lambda>x. \<omega> * indicator N x)"


644 
using assms


645 
by (safe intro!: simple_integral_mono simple_function_mult simple_function_indicator simple_function_const) simp


646 
also have "... = 0" apply(subst simple_integral_mult)


647 
using assms(2) by auto


648 
finally show ?thesis by auto


649 
qed

35582

650 

38656

651 
lemma (in measure_space) simple_integral_cong':


652 
assumes f: "simple_function f" and g: "simple_function g"


653 
and mea: "\<mu> {x\<in>space M. f x \<noteq> g x} = 0"


654 
shows "simple_integral f = simple_integral g"


655 
proof 


656 
let ?h = "\<lambda>h. \<lambda>x. (h x * indicator {x\<in>space M. f x = g x} x


657 
+ h x * indicator {x\<in>space M. f x \<noteq> g x} x


658 
+ h x * indicator (space M) x::pinfreal)"


659 
have *:"\<And>h. h = ?h h" unfolding indicator_def apply rule by auto


660 
have mea_neq:"{x \<in> space M. f x \<noteq> g x} \<in> sets M" using f g by (auto simp: borel_measurable_simple_function)


661 
then have mea_nullset: "{x \<in> space M. f x \<noteq> g x} \<in> null_sets" using mea by auto


662 
have h1:"\<And>h::_=>pinfreal. simple_function h \<Longrightarrow>


663 
simple_function (\<lambda>x. h x * indicator {x\<in>space M. f x = g x} x)"


664 
apply(safe intro!: simple_function_add simple_function_mult simple_function_indicator)


665 
using f g by (auto simp: borel_measurable_simple_function)


666 
have h2:"\<And>h::_\<Rightarrow>pinfreal. simple_function h \<Longrightarrow>


667 
simple_function (\<lambda>x. h x * indicator {x\<in>space M. f x \<noteq> g x} x)"


668 
apply(safe intro!: simple_function_add simple_function_mult simple_function_indicator)


669 
by(rule mea_neq)


670 
have **:"\<And>a b c d e f. a = b \<Longrightarrow> c = d \<Longrightarrow> e = f \<Longrightarrow> a+c+e = b+d+f" by auto


671 
note *** = simple_integral_add[OF simple_function_add[OF h1 h2] simple_function_notspace]


672 
simple_integral_add[OF h1 h2]


673 
show ?thesis apply(subst *[of g]) apply(subst *[of f])


674 
unfolding ***[OF f f] ***[OF g g]


675 
proof(rule **) case goal1 show ?case apply(rule arg_cong[where f=simple_integral]) apply rule


676 
unfolding indicator_def by auto


677 
next note * = simple_integral_null_set[OF _ mea_nullset]


678 
case goal2 show ?case unfolding *[OF f] *[OF g] ..


679 
next case goal3 show ?case apply(rule simple_integral_cong) by auto

35582

680 
qed


681 
qed


682 

35692

683 
section "Continuous posititve integration"


684 

38656

685 
definition (in measure_space)


686 
"positive_integral f =


687 
(SUP g : {g. simple_function g \<and> g \<le> f \<and> \<omega> \<notin> g`space M}. simple_integral g)"

35582

688 

38656

689 
lemma (in measure_space) positive_integral_alt1:


690 
"positive_integral f =


691 
(SUP g : {g. simple_function g \<and> (\<forall>x\<in>space M. g x \<le> f x \<and> g x \<noteq> \<omega>)}. simple_integral g)"


692 
unfolding positive_integral_def SUPR_def


693 
proof (safe intro!: arg_cong[where f=Sup])


694 
fix g let ?g = "\<lambda>x. if x \<in> space M then g x else f x"


695 
assume "simple_function g" "\<forall>x\<in>space M. g x \<le> f x \<and> g x \<noteq> \<omega>"


696 
hence "?g \<le> f" "simple_function ?g" "simple_integral g = simple_integral ?g"


697 
"\<omega> \<notin> g`space M"


698 
unfolding le_fun_def by (auto cong: simple_function_cong simple_integral_cong)


699 
thus "simple_integral g \<in> simple_integral ` {g. simple_function g \<and> g \<le> f \<and> \<omega> \<notin> g`space M}"


700 
by auto


701 
next


702 
fix g assume "simple_function g" "g \<le> f" "\<omega> \<notin> g`space M"


703 
hence "simple_function g" "\<forall>x\<in>space M. g x \<le> f x \<and> g x \<noteq> \<omega>"


704 
by (auto simp add: le_fun_def image_iff)


705 
thus "simple_integral g \<in> simple_integral ` {g. simple_function g \<and> (\<forall>x\<in>space M. g x \<le> f x \<and> g x \<noteq> \<omega>)}"


706 
by auto

35582

707 
qed


708 

38656

709 
lemma (in measure_space) positive_integral_alt:


710 
"positive_integral f =


711 
(SUP g : {g. simple_function g \<and> g \<le> f}. simple_integral g)"


712 
apply(rule order_class.antisym) unfolding positive_integral_def


713 
apply(rule SUPR_subset) apply blast apply(rule SUPR_mono_lim)


714 
proof safe fix u assume u:"simple_function u" and uf:"u \<le> f"


715 
let ?u = "\<lambda>n x. if u x = \<omega> then Real (real (n::nat)) else u x"


716 
have su:"\<And>n. simple_function (?u n)" using simple_function_compose1[OF u] .


717 
show "\<exists>b. \<forall>n. b n \<in> {g. simple_function g \<and> g \<le> f \<and> \<omega> \<notin> g ` space M} \<and>


718 
(\<lambda>n. simple_integral (b n)) > simple_integral u"


719 
apply(rule_tac x="?u" in exI, safe) apply(rule su)


720 
proof fix n::nat have "?u n \<le> u" unfolding le_fun_def by auto


721 
also note uf finally show "?u n \<le> f" .


722 
let ?s = "{x \<in> space M. u x = \<omega>}"


723 
show "(\<lambda>n. simple_integral (?u n)) > simple_integral u"


724 
proof(cases "\<mu> ?s = 0")


725 
case True have *:"\<And>n. {x\<in>space M. ?u n x \<noteq> u x} = {x\<in>space M. u x = \<omega>}" by auto


726 
have *:"\<And>n. simple_integral (?u n) = simple_integral u"


727 
apply(rule simple_integral_cong'[OF su u]) unfolding * True ..


728 
show ?thesis unfolding * by auto


729 
next case False note m0=this


730 
have s:"{x \<in> space M. u x = \<omega>} \<in> sets M" using u by (auto simp: borel_measurable_simple_function)


731 
have "\<omega> = simple_integral (\<lambda>x. \<omega> * indicator {x\<in>space M. u x = \<omega>} x)"


732 
apply(subst simple_integral_mult) using s


733 
unfolding simple_integral_indicator_only[OF s] using False by auto


734 
also have "... \<le> simple_integral u"


735 
apply (rule simple_integral_mono)


736 
apply (rule simple_function_mult)


737 
apply (rule simple_function_const)


738 
apply(rule ) prefer 3 apply(subst indicator_def)


739 
using s u by auto


740 
finally have *:"simple_integral u = \<omega>" by auto


741 
show ?thesis unfolding * Lim_omega_pos


742 
proof safe case goal1


743 
from real_arch_simple[of "B / real (\<mu> ?s)"] guess N0 .. note N=this


744 
def N \<equiv> "Suc N0" have N:"real N \<ge> B / real (\<mu> ?s)" "N > 0"


745 
unfolding N_def using N by auto


746 
show ?case applyapply(rule_tac x=N in exI,safe)


747 
proof case goal1


748 
have "Real B \<le> Real (real N) * \<mu> ?s"


749 
proof(cases "\<mu> ?s = \<omega>")


750 
case True thus ?thesis using `B>0` N by auto


751 
next case False


752 
have *:"B \<le> real N * real (\<mu> ?s)"


753 
using N(1) applyapply(subst (asm) pos_divide_le_eq)


754 
apply rule using m0 False by auto


755 
show ?thesis apply(subst Real_real'[THEN sym,OF False])


756 
apply(subst pinfreal_times,subst if_P) defer


757 
apply(subst pinfreal_less_eq,subst if_P) defer


758 
using * N `B>0` by(auto intro: mult_nonneg_nonneg)


759 
qed


760 
also have "... \<le> Real (real n) * \<mu> ?s"


761 
apply(rule mult_right_mono) using goal1 by auto


762 
also have "... = simple_integral (\<lambda>x. Real (real n) * indicator ?s x)"


763 
apply(subst simple_integral_mult) apply(rule simple_function_indicator[OF s])


764 
unfolding simple_integral_indicator_only[OF s] ..


765 
also have "... \<le> simple_integral (\<lambda>x. if u x = \<omega> then Real (real n) else u x)"


766 
apply(rule simple_integral_mono) apply(rule simple_function_mult)


767 
apply(rule simple_function_const)


768 
apply(rule simple_function_indicator) apply(rule s su)+ by auto


769 
finally show ?case .


770 
qed qed qed


771 
fix x assume x:"\<omega> = (if u x = \<omega> then Real (real n) else u x)" "x \<in> space M"


772 
hence "u x = \<omega>" applyapply(rule ccontr) by auto


773 
hence "\<omega> = Real (real n)" using x by auto


774 
thus False by auto

35582

775 
qed


776 
qed


777 

38656

778 
lemma (in measure_space) positive_integral_cong:


779 
assumes "\<And>x. x \<in> space M \<Longrightarrow> f x = g x"


780 
shows "positive_integral f = positive_integral g"


781 
proof 


782 
have "\<And>h. (\<forall>x\<in>space M. h x \<le> f x \<and> h x \<noteq> \<omega>) = (\<forall>x\<in>space M. h x \<le> g x \<and> h x \<noteq> \<omega>)"


783 
using assms by auto


784 
thus ?thesis unfolding positive_integral_alt1 by auto


785 
qed


786 


787 
lemma (in measure_space) positive_integral_eq_simple_integral:


788 
assumes "simple_function f"


789 
shows "positive_integral f = simple_integral f"


790 
unfolding positive_integral_alt


791 
proof (safe intro!: pinfreal_SUPI)


792 
fix g assume "simple_function g" "g \<le> f"


793 
with assms show "simple_integral g \<le> simple_integral f"


794 
by (auto intro!: simple_integral_mono simp: le_fun_def)


795 
next


796 
fix y assume "\<forall>x. x\<in>{g. simple_function g \<and> g \<le> f} \<longrightarrow> simple_integral x \<le> y"


797 
with assms show "simple_integral f \<le> y" by auto


798 
qed

35582

799 

38656

800 
lemma (in measure_space) positive_integral_mono:


801 
assumes mono: "\<And>x. x \<in> space M \<Longrightarrow> u x \<le> v x"


802 
shows "positive_integral u \<le> positive_integral v"


803 
unfolding positive_integral_alt1


804 
proof (safe intro!: SUPR_mono)


805 
fix a assume a: "simple_function a" and "\<forall>x\<in>space M. a x \<le> u x \<and> a x \<noteq> \<omega>"


806 
with mono have "\<forall>x\<in>space M. a x \<le> v x \<and> a x \<noteq> \<omega>" by fastsimp


807 
with a show "\<exists>b\<in>{g. simple_function g \<and> (\<forall>x\<in>space M. g x \<le> v x \<and> g x \<noteq> \<omega>)}. simple_integral a \<le> simple_integral b"


808 
by (auto intro!: bexI[of _ a])


809 
qed


810 


811 
lemma (in measure_space) positive_integral_SUP_approx:


812 
assumes "f \<up> s"


813 
and f: "\<And>i. f i \<in> borel_measurable M"


814 
and "simple_function u"


815 
and le: "u \<le> s" and real: "\<omega> \<notin> u`space M"


816 
shows "simple_integral u \<le> (SUP i. positive_integral (f i))" (is "_ \<le> ?S")


817 
proof (rule pinfreal_le_mult_one_interval)


818 
fix a :: pinfreal assume "0 < a" "a < 1"


819 
hence "a \<noteq> 0" by auto


820 
let "?B i" = "{x \<in> space M. a * u x \<le> f i x}"


821 
have B: "\<And>i. ?B i \<in> sets M"


822 
using f `simple_function u` by (auto simp: borel_measurable_simple_function)


823 


824 
let "?uB i x" = "u x * indicator (?B i) x"


825 


826 
{ fix i have "?B i \<subseteq> ?B (Suc i)"


827 
proof safe


828 
fix i x assume "a * u x \<le> f i x"


829 
also have "\<dots> \<le> f (Suc i) x"


830 
using `f \<up> s` unfolding isoton_def le_fun_def by auto


831 
finally show "a * u x \<le> f (Suc i) x" .


832 
qed }


833 
note B_mono = this

35582

834 

38656

835 
have u: "\<And>x. x \<in> space M \<Longrightarrow> u ` {u x} \<inter> space M \<in> sets M"


836 
using `simple_function u` by (auto simp add: simple_function_def)


837 


838 
{ fix i


839 
have "(\<lambda>n. (u ` {i} \<inter> space M) \<inter> ?B n) \<up> (u ` {i} \<inter> space M)" using B_mono unfolding isoton_def


840 
proof safe


841 
fix x assume "x \<in> space M"


842 
show "x \<in> (\<Union>i. (u ` {u x} \<inter> space M) \<inter> ?B i)"


843 
proof cases


844 
assume "u x = 0" thus ?thesis using `x \<in> space M` by simp


845 
next


846 
assume "u x \<noteq> 0"


847 
with `a < 1` real `x \<in> space M`


848 
have "a * u x < 1 * u x" by (rule_tac pinfreal_mult_strict_right_mono) (auto simp: image_iff)


849 
also have "\<dots> \<le> (SUP i. f i x)" using le `f \<up> s`


850 
unfolding isoton_fun_expand by (auto simp: isoton_def le_fun_def)


851 
finally obtain i where "a * u x < f i x" unfolding SUPR_def


852 
by (auto simp add: less_Sup_iff)


853 
hence "a * u x \<le> f i x" by auto


854 
thus ?thesis using `x \<in> space M` by auto


855 
qed


856 
qed auto }


857 
note measure_conv = measure_up[OF u Int[OF u B] this]


858 


859 
have "simple_integral u = (SUP i. simple_integral (?uB i))"


860 
unfolding simple_integral_indicator[OF B `simple_function u`]


861 
proof (subst SUPR_pinfreal_setsum, safe)


862 
fix x n assume "x \<in> space M"


863 
have "\<mu> (u ` {u x} \<inter> space M \<inter> {x \<in> space M. a * u x \<le> f n x})


864 
\<le> \<mu> (u ` {u x} \<inter> space M \<inter> {x \<in> space M. a * u x \<le> f (Suc n) x})"


865 
using B_mono Int[OF u[OF `x \<in> space M`] B] by (auto intro!: measure_mono)


866 
thus "u x * \<mu> (u ` {u x} \<inter> space M \<inter> ?B n)


867 
\<le> u x * \<mu> (u ` {u x} \<inter> space M \<inter> ?B (Suc n))"


868 
by (auto intro: mult_left_mono)


869 
next


870 
show "simple_integral u =


871 
(\<Sum>i\<in>u ` space M. SUP n. i * \<mu> (u ` {i} \<inter> space M \<inter> ?B n))"


872 
using measure_conv unfolding simple_integral_def isoton_def


873 
by (auto intro!: setsum_cong simp: pinfreal_SUP_cmult)


874 
qed


875 
moreover


876 
have "a * (SUP i. simple_integral (?uB i)) \<le> ?S"


877 
unfolding pinfreal_SUP_cmult[symmetric]


878 
proof (safe intro!: SUP_mono)


879 
fix i


880 
have "a * simple_integral (?uB i) = simple_integral (\<lambda>x. a * ?uB i x)"


881 
using B `simple_function u`


882 
by (subst simple_integral_mult[symmetric]) (auto simp: field_simps)


883 
also have "\<dots> \<le> positive_integral (f i)"


884 
proof 


885 
have "\<And>x. a * ?uB i x \<le> f i x" unfolding indicator_def by auto


886 
hence *: "simple_function (\<lambda>x. a * ?uB i x)" using B assms(3)


887 
by (auto intro!: simple_integral_mono)


888 
show ?thesis unfolding positive_integral_eq_simple_integral[OF *, symmetric]


889 
by (auto intro!: positive_integral_mono simp: indicator_def)


890 
qed


891 
finally show "a * simple_integral (?uB i) \<le> positive_integral (f i)"


892 
by auto


893 
qed


894 
ultimately show "a * simple_integral u \<le> ?S" by simp

35582

895 
qed


896 


897 
text {* BeppoLevi monotone convergence theorem *}

38656

898 
lemma (in measure_space) positive_integral_isoton:


899 
assumes "f \<up> u" "\<And>i. f i \<in> borel_measurable M"


900 
shows "(\<lambda>i. positive_integral (f i)) \<up> positive_integral u"


901 
unfolding isoton_def


902 
proof safe


903 
fix i show "positive_integral (f i) \<le> positive_integral (f (Suc i))"


904 
apply (rule positive_integral_mono)


905 
using `f \<up> u` unfolding isoton_def le_fun_def by auto


906 
next


907 
have "u \<in> borel_measurable M"


908 
using borel_measurable_SUP[of UNIV f] assms by (auto simp: isoton_def)


909 
have u: "u = (SUP i. f i)" using `f \<up> u` unfolding isoton_def by auto

35582

910 

38656

911 
show "(SUP i. positive_integral (f i)) = positive_integral u"


912 
proof (rule antisym)


913 
from `f \<up> u`[THEN isoton_Sup, unfolded le_fun_def]


914 
show "(SUP j. positive_integral (f j)) \<le> positive_integral u"


915 
by (auto intro!: SUP_leI positive_integral_mono)


916 
next


917 
show "positive_integral u \<le> (SUP i. positive_integral (f i))"


918 
unfolding positive_integral_def[of u]


919 
by (auto intro!: SUP_leI positive_integral_SUP_approx[OF assms])

35582

920 
qed


921 
qed


922 

38656

923 
lemma (in measure_space) SUP_simple_integral_sequences:


924 
assumes f: "f \<up> u" "\<And>i. simple_function (f i)"


925 
and g: "g \<up> u" "\<And>i. simple_function (g i)"


926 
shows "(SUP i. simple_integral (f i)) = (SUP i. simple_integral (g i))"


927 
(is "SUPR _ ?F = SUPR _ ?G")


928 
proof 


929 
have "(SUP i. ?F i) = (SUP i. positive_integral (f i))"


930 
using assms by (simp add: positive_integral_eq_simple_integral)


931 
also have "\<dots> = positive_integral u"


932 
using positive_integral_isoton[OF f(1) borel_measurable_simple_function[OF f(2)]]


933 
unfolding isoton_def by simp


934 
also have "\<dots> = (SUP i. positive_integral (g i))"


935 
using positive_integral_isoton[OF g(1) borel_measurable_simple_function[OF g(2)]]


936 
unfolding isoton_def by simp


937 
also have "\<dots> = (SUP i. ?G i)"


938 
using assms by (simp add: positive_integral_eq_simple_integral)


939 
finally show ?thesis .


940 
qed


941 


942 
lemma (in measure_space) positive_integral_const[simp]:


943 
"positive_integral (\<lambda>x. c) = c * \<mu> (space M)"


944 
by (subst positive_integral_eq_simple_integral) auto


945 


946 
lemma (in measure_space) positive_integral_isoton_simple:


947 
assumes "f \<up> u" and e: "\<And>i. simple_function (f i)"


948 
shows "(\<lambda>i. simple_integral (f i)) \<up> positive_integral u"


949 
using positive_integral_isoton[OF `f \<up> u` e(1)[THEN borel_measurable_simple_function]]


950 
unfolding positive_integral_eq_simple_integral[OF e] .


951 


952 
lemma (in measure_space) positive_integral_linear:


953 
assumes f: "f \<in> borel_measurable M"


954 
and g: "g \<in> borel_measurable M"


955 
shows "positive_integral (\<lambda>x. a * f x + g x) =


956 
a * positive_integral f + positive_integral g"


957 
(is "positive_integral ?L = _")

35582

958 
proof 

38656

959 
from borel_measurable_implies_simple_function_sequence'[OF f] guess u .


960 
note u = this positive_integral_isoton_simple[OF this(12)]


961 
from borel_measurable_implies_simple_function_sequence'[OF g] guess v .


962 
note v = this positive_integral_isoton_simple[OF this(12)]


963 
let "?L' i x" = "a * u i x + v i x"


964 


965 
have "?L \<in> borel_measurable M"


966 
using assms by simp


967 
from borel_measurable_implies_simple_function_sequence'[OF this] guess l .


968 
note positive_integral_isoton_simple[OF this(12)] and l = this


969 
moreover have


970 
"(SUP i. simple_integral (l i)) = (SUP i. simple_integral (?L' i))"


971 
proof (rule SUP_simple_integral_sequences[OF l(12)])


972 
show "?L' \<up> ?L" "\<And>i. simple_function (?L' i)"


973 
using u v by (auto simp: isoton_fun_expand isoton_add isoton_cmult_right)


974 
qed


975 
moreover from u v have L'_isoton:


976 
"(\<lambda>i. simple_integral (?L' i)) \<up> a * positive_integral f + positive_integral g"


977 
by (simp add: isoton_add isoton_cmult_right)


978 
ultimately show ?thesis by (simp add: isoton_def)


979 
qed


980 


981 
lemma (in measure_space) positive_integral_cmult:


982 
assumes "f \<in> borel_measurable M"


983 
shows "positive_integral (\<lambda>x. c * f x) = c * positive_integral f"


984 
using positive_integral_linear[OF assms, of "\<lambda>x. 0" c] by auto


985 


986 
lemma (in measure_space) positive_integral_indicator[simp]:


987 
"A \<in> sets M \<Longrightarrow> positive_integral (\<lambda>x. indicator A x) = \<mu> A"


988 
by (subst positive_integral_eq_simple_integral) (auto simp: simple_function_indicator simple_integral_indicator)


989 


990 
lemma (in measure_space) positive_integral_cmult_indicator:


991 
"A \<in> sets M \<Longrightarrow> positive_integral (\<lambda>x. c * indicator A x) = c * \<mu> A"


992 
by (subst positive_integral_eq_simple_integral) (auto simp: simple_function_indicator simple_integral_indicator)


993 


994 
lemma (in measure_space) positive_integral_add:


995 
assumes "f \<in> borel_measurable M" "g \<in> borel_measurable M"


996 
shows "positive_integral (\<lambda>x. f x + g x) = positive_integral f + positive_integral g"


997 
using positive_integral_linear[OF assms, of 1] by simp


998 


999 
lemma (in measure_space) positive_integral_setsum:


1000 
assumes "\<And>i. i\<in>P \<Longrightarrow> f i \<in> borel_measurable M"


1001 
shows "positive_integral (\<lambda>x. \<Sum>i\<in>P. f i x) = (\<Sum>i\<in>P. positive_integral (f i))"


1002 
proof cases


1003 
assume "finite P"


1004 
from this assms show ?thesis


1005 
proof induct


1006 
case (insert i P)


1007 
have "f i \<in> borel_measurable M"


1008 
"(\<lambda>x. \<Sum>i\<in>P. f i x) \<in> borel_measurable M"


1009 
using insert by (auto intro!: borel_measurable_pinfreal_setsum)


1010 
from positive_integral_add[OF this]


1011 
show ?case using insert by auto


1012 
qed simp


1013 
qed simp


1014 


1015 
lemma (in measure_space) positive_integral_diff:


1016 
assumes f: "f \<in> borel_measurable M" and g: "g \<in> borel_measurable M"


1017 
and fin: "positive_integral g \<noteq> \<omega>"


1018 
and mono: "\<And>x. x \<in> space M \<Longrightarrow> g x \<le> f x"


1019 
shows "positive_integral (\<lambda>x. f x  g x) = positive_integral f  positive_integral g"


1020 
proof 


1021 
have borel: "(\<lambda>x. f x  g x) \<in> borel_measurable M"


1022 
using f g by (rule borel_measurable_pinfreal_diff)


1023 
have "positive_integral (\<lambda>x. f x  g x) + positive_integral g =


1024 
positive_integral f"


1025 
unfolding positive_integral_add[OF borel g, symmetric]


1026 
proof (rule positive_integral_cong)


1027 
fix x assume "x \<in> space M"


1028 
from mono[OF this] show "f x  g x + g x = f x"


1029 
by (cases "f x", cases "g x", simp, simp, cases "g x", auto)


1030 
qed


1031 
with mono show ?thesis


1032 
by (subst minus_pinfreal_eq2[OF _ fin]) (auto intro!: positive_integral_mono)


1033 
qed


1034 


1035 
lemma (in measure_space) positive_integral_psuminf:


1036 
assumes "\<And>i. f i \<in> borel_measurable M"


1037 
shows "positive_integral (\<lambda>x. \<Sum>\<^isub>\<infinity> i. f i x) = (\<Sum>\<^isub>\<infinity> i. positive_integral (f i))"


1038 
proof 


1039 
have "(\<lambda>i. positive_integral (\<lambda>x. \<Sum>i<i. f i x)) \<up> positive_integral (\<lambda>x. \<Sum>\<^isub>\<infinity>i. f i x)"


1040 
by (rule positive_integral_isoton)


1041 
(auto intro!: borel_measurable_pinfreal_setsum assms positive_integral_mono


1042 
arg_cong[where f=Sup]


1043 
simp: isoton_def le_fun_def psuminf_def expand_fun_eq SUPR_def Sup_fun_def)


1044 
thus ?thesis


1045 
by (auto simp: isoton_def psuminf_def positive_integral_setsum[OF assms])


1046 
qed


1047 


1048 
text {* Fatou's lemma: convergence theorem on limes inferior *}


1049 
lemma (in measure_space) positive_integral_lim_INF:


1050 
fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> pinfreal"


1051 
assumes "\<And>i. u i \<in> borel_measurable M"


1052 
shows "positive_integral (SUP n. INF m. u (m + n)) \<le>


1053 
(SUP n. INF m. positive_integral (u (m + n)))"


1054 
proof 


1055 
have "(SUP n. INF m. u (m + n)) \<in> borel_measurable M"


1056 
by (auto intro!: borel_measurable_SUP borel_measurable_INF assms)


1057 


1058 
have "(\<lambda>n. INF m. u (m + n)) \<up> (SUP n. INF m. u (m + n))"


1059 
proof (unfold isoton_def, safe)


1060 
fix i show "(INF m. u (m + i)) \<le> (INF m. u (m + Suc i))"


1061 
by (rule INF_mono[where N=Suc]) simp


1062 
qed


1063 
from positive_integral_isoton[OF this] assms


1064 
have "positive_integral (SUP n. INF m. u (m + n)) =


1065 
(SUP n. positive_integral (INF m. u (m + n)))"


1066 
unfolding isoton_def by (simp add: borel_measurable_INF)


1067 
also have "\<dots> \<le> (SUP n. INF m. positive_integral (u (m + n)))"


1068 
by (auto intro!: SUP_mono[where N="\<lambda>x. x"] INFI_bound positive_integral_mono INF_leI simp: INFI_fun_expand)


1069 
finally show ?thesis .

35582

1070 
qed


1071 

38656

1072 
lemma (in measure_space) measure_space_density:


1073 
assumes borel: "u \<in> borel_measurable M"


1074 
shows "measure_space M (\<lambda>A. positive_integral (\<lambda>x. u x * indicator A x))" (is "measure_space M ?v")


1075 
proof


1076 
show "?v {} = 0" by simp


1077 
show "countably_additive M ?v"


1078 
unfolding countably_additive_def


1079 
proof safe


1080 
fix A :: "nat \<Rightarrow> 'a set"


1081 
assume "range A \<subseteq> sets M"


1082 
hence "\<And>i. (\<lambda>x. u x * indicator (A i) x) \<in> borel_measurable M"


1083 
using borel by (auto intro: borel_measurable_indicator)


1084 
moreover assume "disjoint_family A"


1085 
note psuminf_indicator[OF this]


1086 
ultimately show "(\<Sum>\<^isub>\<infinity>n. ?v (A n)) = ?v (\<Union>x. A x)"


1087 
by (simp add: positive_integral_psuminf[symmetric])


1088 
qed


1089 
qed

35582

1090 

38656

1091 
lemma (in measure_space) positive_integral_null_set:


1092 
assumes borel: "u \<in> borel_measurable M" and "N \<in> null_sets"


1093 
shows "positive_integral (\<lambda>x. u x * indicator N x) = 0" (is "?I = 0")


1094 
proof 


1095 
have "N \<in> sets M" using `N \<in> null_sets` by auto


1096 
have "(\<lambda>i x. min (of_nat i) (u x) * indicator N x) \<up> (\<lambda>x. u x * indicator N x)"


1097 
unfolding isoton_fun_expand


1098 
proof (safe intro!: isoton_cmult_left, unfold isoton_def, safe)


1099 
fix j i show "min (of_nat j) (u i) \<le> min (of_nat (Suc j)) (u i)"


1100 
by (rule min_max.inf_mono) auto


1101 
next


1102 
fix i show "(SUP j. min (of_nat j) (u i)) = u i"


1103 
proof (cases "u i")


1104 
case infinite


1105 
moreover hence "\<And>j. min (of_nat j) (u i) = of_nat j"


1106 
by (auto simp: min_def)


1107 
ultimately show ?thesis by (simp add: Sup_\<omega>)

35582

1108 
next

38656

1109 
case (preal r)


1110 
obtain j where "r \<le> of_nat j" using ex_le_of_nat ..


1111 
hence "u i \<le> of_nat j" using preal by (auto simp: real_of_nat_def)


1112 
show ?thesis


1113 
proof (rule pinfreal_SUPI)


1114 
fix y assume "\<And>j. j \<in> UNIV \<Longrightarrow> min (of_nat j) (u i) \<le> y"


1115 
note this[of j]


1116 
moreover have "min (of_nat j) (u i) = u i"


1117 
using `u i \<le> of_nat j` by (auto simp: min_def)


1118 
ultimately show "u i \<le> y" by simp

35582

1119 
qed simp


1120 
qed


1121 
qed

38656

1122 
from positive_integral_isoton[OF this]


1123 
have "?I = (SUP i. positive_integral (\<lambda>x. min (of_nat i) (u x) * indicator N x))"


1124 
unfolding isoton_def using borel `N \<in> sets M` by (simp add: borel_measurable_indicator)


1125 
also have "\<dots> \<le> (SUP i. positive_integral (\<lambda>x. of_nat i * indicator N x))"


1126 
proof (rule SUP_mono, rule positive_integral_mono)


1127 
fix x i show "min (of_nat i) (u x) * indicator N x \<le> of_nat i * indicator N x"


1128 
by (cases "x \<in> N") auto


1129 
qed


1130 
also have "\<dots> = 0"


1131 
using `N \<in> null_sets` by (simp add: positive_integral_cmult_indicator)


1132 
finally show ?thesis by simp


1133 
qed

35582

1134 

38656

1135 
lemma (in measure_space) positive_integral_Markov_inequality:


1136 
assumes borel: "u \<in> borel_measurable M" and "A \<in> sets M" and c: "c \<noteq> \<omega>"


1137 
shows "\<mu> ({x\<in>space M. 1 \<le> c * u x} \<inter> A) \<le> c * positive_integral (\<lambda>x. u x * indicator A x)"


1138 
(is "\<mu> ?A \<le> _ * ?PI")


1139 
proof 


1140 
have "?A \<in> sets M"


1141 
using `A \<in> sets M` borel by auto


1142 
hence "\<mu> ?A = positive_integral (\<lambda>x. indicator ?A x)"


1143 
using positive_integral_indicator by simp


1144 
also have "\<dots> \<le> positive_integral (\<lambda>x. c * (u x * indicator A x))"


1145 
proof (rule positive_integral_mono)


1146 
fix x assume "x \<in> space M"


1147 
show "indicator ?A x \<le> c * (u x * indicator A x)"


1148 
by (cases "x \<in> ?A") auto


1149 
qed


1150 
also have "\<dots> = c * positive_integral (\<lambda>x. u x * indicator A x)"


1151 
using assms


1152 
by (auto intro!: positive_integral_cmult borel_measurable_indicator)


1153 
finally show ?thesis .

35582

1154 
qed


1155 

38656

1156 
lemma (in measure_space) positive_integral_0_iff:


1157 
assumes borel: "u \<in> borel_measurable M"


1158 
shows "positive_integral u = 0 \<longleftrightarrow> \<mu> {x\<in>space M. u x \<noteq> 0} = 0"


1159 
(is "_ \<longleftrightarrow> \<mu> ?A = 0")

35582

1160 
proof 

38656

1161 
have A: "?A \<in> sets M" using borel by auto


1162 
have u: "positive_integral (\<lambda>x. u x * indicator ?A x) = positive_integral u"


1163 
by (auto intro!: positive_integral_cong simp: indicator_def)

35582

1164 

38656

1165 
show ?thesis


1166 
proof


1167 
assume "\<mu> ?A = 0"


1168 
hence "?A \<in> null_sets" using `?A \<in> sets M` by auto


1169 
from positive_integral_null_set[OF borel this]


1170 
have "0 = positive_integral (\<lambda>x. u x * indicator ?A x)" by simp


1171 
thus "positive_integral u = 0" unfolding u by simp


1172 
next


1173 
assume *: "positive_integral u = 0"


1174 
let "?M n" = "{x \<in> space M. 1 \<le> of_nat n * u x}"


1175 
have "0 = (SUP n. \<mu> (?M n \<inter> ?A))"


1176 
proof 


1177 
{ fix n


1178 
from positive_integral_Markov_inequality[OF borel `?A \<in> sets M`, of "of_nat n"]


1179 
have "\<mu> (?M n \<inter> ?A) = 0" unfolding * u by simp }


1180 
thus ?thesis by simp

35582

1181 
qed

38656

1182 
also have "\<dots> = \<mu> (\<Union>n. ?M n \<inter> ?A)"


1183 
proof (safe intro!: continuity_from_below)


1184 
fix n show "?M n \<inter> ?A \<in> sets M"


1185 
using borel by (auto intro!: Int)


1186 
next


1187 
fix n x assume "1 \<le> of_nat n * u x"


1188 
also have "\<dots> \<le> of_nat (Suc n) * u x"


1189 
by (subst (1 2) mult_commute) (auto intro!: pinfreal_mult_cancel)


1190 
finally show "1 \<le> of_nat (Suc n) * u x" .


1191 
qed


1192 
also have "\<dots> = \<mu> ?A"


1193 
proof (safe intro!: arg_cong[where f="\<mu>"])


1194 
fix x assume "u x \<noteq> 0" and [simp, intro]: "x \<in> space M"


1195 
show "x \<in> (\<Union>n. ?M n \<inter> ?A)"


1196 
proof (cases "u x")


1197 
case (preal r)


1198 
obtain j where "1 / r \<le> of_nat j" using ex_le_of_nat ..


1199 
hence "1 / r * r \<le> of_nat j * r" using preal unfolding mult_le_cancel_right by auto


1200 
hence "1 \<le> of_nat j * r" using preal `u x \<noteq> 0` by auto


1201 
thus ?thesis using `u x \<noteq> 0` preal by (auto simp: real_of_nat_def[symmetric])


1202 
qed auto


1203 
qed


1204 
finally show "\<mu> ?A = 0" by simp

35582

1205 
qed


1206 
qed


1207 

38656

1208 
lemma (in measure_space) positive_integral_cong_on_null_sets:


1209 
assumes f: "f \<in> borel_measurable M" and g: "g \<in> borel_measurable M"


1210 
and measure: "\<mu> {x\<in>space M. f x \<noteq> g x} = 0"


1211 
shows "positive_integral f = positive_integral g"

35582

1212 
proof 

38656

1213 
let ?N = "{x\<in>space M. f x \<noteq> g x}" and ?E = "{x\<in>space M. f x = g x}"


1214 
let "?A h x" = "h x * indicator ?E x :: pinfreal"


1215 
let "?B h x" = "h x * indicator ?N x :: pinfreal"


1216 


1217 
have A: "positive_integral (?A f) = positive_integral (?A g)"


1218 
by (auto intro!: positive_integral_cong simp: indicator_def)


1219 


1220 
have [intro]: "?N \<in> sets M" "?E \<in> sets M" using f g by auto


1221 
hence "?N \<in> null_sets" using measure by auto


1222 
hence B: "positive_integral (?B f) = positive_integral (?B g)"


1223 
using f g by (simp add: positive_integral_null_set)


1224 


1225 
have "positive_integral f = positive_integral (\<lambda>x. ?A f x + ?B f x)"


1226 
by (auto intro!: positive_integral_cong simp: indicator_def)


1227 
also have "\<dots> = positive_integral (?A f) + positive_integral (?B f)"

