35582

1 
header {*Lebesgue Integration*}


2 


3 
theory Lebesgue


4 
imports Measure Borel


5 
begin


6 


7 
text{*From the HOL4 Hurd/Coble Lebesgue integration, translated by Armin Heller and Johannes Hoelzl.*}


8 


9 
definition


10 
"pos_part f = (\<lambda>x. max 0 (f x))"


11 


12 
definition


13 
"neg_part f = (\<lambda>x.  min 0 (f x))"


14 


15 
definition


16 
"nonneg f = (\<forall>x. 0 \<le> f x)"


17 


18 
lemma nonneg_pos_part[intro!]:


19 
fixes f :: "'c \<Rightarrow> 'd\<Colon>{linorder,zero}"


20 
shows "nonneg (pos_part f)"


21 
unfolding nonneg_def pos_part_def by auto


22 


23 
lemma nonneg_neg_part[intro!]:


24 
fixes f :: "'c \<Rightarrow> 'd\<Colon>{linorder,ordered_ab_group_add}"


25 
shows "nonneg (neg_part f)"


26 
unfolding nonneg_def neg_part_def min_def by auto


27 

36624

28 
lemma pos_neg_part_abs:


29 
fixes f :: "'a \<Rightarrow> real"


30 
shows "pos_part f x + neg_part f x = \<bar>f x\<bar>"


31 
unfolding real_abs_def pos_part_def neg_part_def by auto


32 


33 
lemma pos_part_abs:


34 
fixes f :: "'a \<Rightarrow> real"


35 
shows "pos_part (\<lambda> x. \<bar>f x\<bar>) y = \<bar>f y\<bar>"


36 
unfolding pos_part_def real_abs_def by auto


37 


38 
lemma neg_part_abs:


39 
fixes f :: "'a \<Rightarrow> real"


40 
shows "neg_part (\<lambda> x. \<bar>f x\<bar>) y = 0"


41 
unfolding neg_part_def real_abs_def by auto


42 

35692

43 
lemma (in measure_space)


44 
assumes "f \<in> borel_measurable M"


45 
shows pos_part_borel_measurable: "pos_part f \<in> borel_measurable M"


46 
and neg_part_borel_measurable: "neg_part f \<in> borel_measurable M"


47 
using assms


48 
proof 


49 
{ fix a :: real


50 
{ assume asm: "0 \<le> a"


51 
from asm have pp: "\<And> w. (pos_part f w \<le> a) = (f w \<le> a)" unfolding pos_part_def by auto


52 
have "{w  w. w \<in> space M \<and> f w \<le> a} \<in> sets M"


53 
unfolding pos_part_def using assms borel_measurable_le_iff by auto


54 
hence "{w . w \<in> space M \<and> pos_part f w \<le> a} \<in> sets M" using pp by auto }


55 
moreover have "a < 0 \<Longrightarrow> {w \<in> space M. pos_part f w \<le> a} \<in> sets M"


56 
unfolding pos_part_def using empty_sets by auto


57 
ultimately have "{w . w \<in> space M \<and> pos_part f w \<le> a} \<in> sets M"


58 
using le_less_linear by auto


59 
} hence pos: "pos_part f \<in> borel_measurable M" using borel_measurable_le_iff by auto


60 
{ fix a :: real


61 
{ assume asm: "0 \<le> a"


62 
from asm have pp: "\<And> w. (neg_part f w \<le> a) = (f w \<ge>  a)" unfolding neg_part_def by auto


63 
have "{w  w. w \<in> space M \<and> f w \<ge>  a} \<in> sets M"


64 
unfolding neg_part_def using assms borel_measurable_ge_iff by auto


65 
hence "{w . w \<in> space M \<and> neg_part f w \<le> a} \<in> sets M" using pp by auto }


66 
moreover have "a < 0 \<Longrightarrow> {w \<in> space M. neg_part f w \<le> a} = {}" unfolding neg_part_def by auto


67 
moreover hence "a < 0 \<Longrightarrow> {w \<in> space M. neg_part f w \<le> a} \<in> sets M" by (simp only: empty_sets)


68 
ultimately have "{w . w \<in> space M \<and> neg_part f w \<le> a} \<in> sets M"


69 
using le_less_linear by auto


70 
} hence neg: "neg_part f \<in> borel_measurable M" using borel_measurable_le_iff by auto


71 
from pos neg show "pos_part f \<in> borel_measurable M" and "neg_part f \<in> borel_measurable M" by auto


72 
qed


73 


74 
lemma (in measure_space) pos_part_neg_part_borel_measurable_iff:


75 
"f \<in> borel_measurable M \<longleftrightarrow>


76 
pos_part f \<in> borel_measurable M \<and> neg_part f \<in> borel_measurable M"


77 
proof 


78 
{ fix x


79 
have "f x = pos_part f x  neg_part f x"


80 
unfolding pos_part_def neg_part_def unfolding max_def min_def


81 
by auto }


82 
hence "(\<lambda> x. f x) = (\<lambda> x. pos_part f x  neg_part f x)" by auto


83 
hence "f = (\<lambda> x. pos_part f x  neg_part f x)" by blast


84 
from pos_part_borel_measurable[of f] neg_part_borel_measurable[of f]


85 
borel_measurable_diff_borel_measurable[of "pos_part f" "neg_part f"]


86 
this


87 
show ?thesis by auto


88 
qed


89 

35582

90 
context measure_space


91 
begin


92 

35692

93 
section "Simple discrete step function"


94 

35582

95 
definition


96 
"pos_simple f =


97 
{ (s :: nat set, a, x).


98 
finite s \<and> nonneg f \<and> nonneg x \<and> a ` s \<subseteq> sets M \<and>


99 
(\<forall>t \<in> space M. (\<exists>!i\<in>s. t\<in>a i) \<and> (\<forall>i\<in>s. t \<in> a i \<longrightarrow> f t = x i)) }"


100 


101 
definition


102 
"pos_simple_integral \<equiv> \<lambda>(s, a, x). \<Sum> i \<in> s. x i * measure M (a i)"


103 


104 
definition


105 
"psfis f = pos_simple_integral ` (pos_simple f)"


106 


107 
lemma pos_simpleE[consumes 1]:


108 
assumes ps: "(s, a, x) \<in> pos_simple f"


109 
obtains "finite s" and "nonneg f" and "nonneg x"


110 
and "a ` s \<subseteq> sets M" and "(\<Union>i\<in>s. a i) = space M"


111 
and "disjoint_family_on a s"


112 
and "\<And>t. t \<in> space M \<Longrightarrow> (\<exists>!i. i \<in> s \<and> t \<in> a i)"


113 
and "\<And>t i. \<lbrakk> t \<in> space M ; i \<in> s ; t \<in> a i \<rbrakk> \<Longrightarrow> f t = x i"


114 
proof


115 
show "finite s" and "nonneg f" and "nonneg x"


116 
and as_in_M: "a ` s \<subseteq> sets M"


117 
and *: "\<And>t. t \<in> space M \<Longrightarrow> (\<exists>!i. i \<in> s \<and> t \<in> a i)"


118 
and **: "\<And>t i. \<lbrakk> t \<in> space M ; i \<in> s ; t \<in> a i \<rbrakk> \<Longrightarrow> f t = x i"


119 
using ps unfolding pos_simple_def by auto


120 


121 
thus t: "(\<Union>i\<in>s. a i) = space M"


122 
proof safe


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


124 
from *[OF this] show "x \<in> (\<Union>i\<in>s. a i)" by auto


125 
next


126 
fix t i assume "i \<in> s"


127 
hence "a i \<in> sets M" using as_in_M by auto


128 
moreover assume "t \<in> a i"


129 
ultimately show "t \<in> space M" using sets_into_space by blast


130 
qed


131 


132 
show "disjoint_family_on a s" unfolding disjoint_family_on_def


133 
proof safe


134 
fix i j and t assume "i \<in> s" "t \<in> a i" and "j \<in> s" "t \<in> a j" and "i \<noteq> j"


135 
with t * show "t \<in> {}" by auto


136 
qed


137 
qed


138 


139 
lemma pos_simple_cong:


140 
assumes "nonneg f" and "nonneg g" and "\<And>t. t \<in> space M \<Longrightarrow> f t = g t"


141 
shows "pos_simple f = pos_simple g"


142 
unfolding pos_simple_def using assms by auto


143 


144 
lemma psfis_cong:


145 
assumes "nonneg f" and "nonneg g" and "\<And>t. t \<in> space M \<Longrightarrow> f t = g t"


146 
shows "psfis f = psfis g"


147 
unfolding psfis_def using pos_simple_cong[OF assms] by simp


148 

35692

149 
lemma psfis_0: "0 \<in> psfis (\<lambda>x. 0)"


150 
unfolding psfis_def pos_simple_def pos_simple_integral_def


151 
by (auto simp: nonneg_def


152 
intro: image_eqI[where x="({0}, (\<lambda>i. space M), (\<lambda>i. 0))"])


153 

35582

154 
lemma pos_simple_setsum_indicator_fn:


155 
assumes ps: "(s, a, x) \<in> pos_simple f"


156 
and "t \<in> space M"


157 
shows "(\<Sum>i\<in>s. x i * indicator_fn (a i) t) = f t"


158 
proof 


159 
from assms obtain i where *: "i \<in> s" "t \<in> a i"


160 
and "finite s" and xi: "x i = f t" by (auto elim!: pos_simpleE)


161 


162 
have **: "(\<Sum>i\<in>s. x i * indicator_fn (a i) t) =


163 
(\<Sum>j\<in>s. if j \<in> {i} then x i else 0)"


164 
unfolding indicator_fn_def using assms *


165 
by (auto intro!: setsum_cong elim!: pos_simpleE)


166 
show ?thesis unfolding ** setsum_cases[OF `finite s`] xi


167 
using `i \<in> s` by simp


168 
qed


169 

35692

170 
lemma pos_simple_common_partition:

35582

171 
assumes psf: "(s, a, x) \<in> pos_simple f"


172 
assumes psg: "(s', b, y) \<in> pos_simple g"


173 
obtains z z' c k where "(k, c, z) \<in> pos_simple f" "(k, c, z') \<in> pos_simple g"


174 
proof 


175 
(* definitions *)


176 


177 
def k == "{0 ..< card (s \<times> s')}"


178 
have fs: "finite s" "finite s'" "finite k" unfolding k_def


179 
using psf psg unfolding pos_simple_def by auto


180 
hence "finite (s \<times> s')" by simp


181 
then obtain p where p: "p ` k = s \<times> s'" "inj_on p k"


182 
using ex_bij_betw_nat_finite[of "s \<times> s'"] unfolding bij_betw_def k_def by blast


183 
def c == "\<lambda> i. a (fst (p i)) \<inter> b (snd (p i))"


184 
def z == "\<lambda> i. x (fst (p i))"


185 
def z' == "\<lambda> i. y (snd (p i))"


186 


187 
have "finite k" unfolding k_def by simp


188 


189 
have "nonneg z" and "nonneg z'"


190 
using psf psg unfolding z_def z'_def pos_simple_def nonneg_def by auto


191 


192 
have ck_subset_M: "c ` k \<subseteq> sets M"


193 
proof


194 
fix x assume "x \<in> c ` k"


195 
then obtain j where "j \<in> k" and "x = c j" by auto


196 
hence "p j \<in> s \<times> s'" using p(1) by auto


197 
hence "a (fst (p j)) \<in> sets M" (is "?a \<in> _")


198 
and "b (snd (p j)) \<in> sets M" (is "?b \<in> _")


199 
using psf psg unfolding pos_simple_def by auto


200 
thus "x \<in> sets M" unfolding `x = c j` c_def using Int by simp


201 
qed


202 


203 
{ fix t assume "t \<in> space M"


204 
hence ex1s: "\<exists>!i\<in>s. t \<in> a i" and ex1s': "\<exists>!i\<in>s'. t \<in> b i"


205 
using psf psg unfolding pos_simple_def by auto


206 
then obtain j j' where j: "j \<in> s" "t \<in> a j" and j': "j' \<in> s'" "t \<in> b j'"


207 
by auto


208 
then obtain i :: nat where i: "(j,j') = p i" and "i \<in> k" using p by auto


209 
have "\<exists>!i\<in>k. t \<in> c i"


210 
proof (rule ex1I[of _ i])


211 
show "\<And>x. x \<in> k \<Longrightarrow> t \<in> c x \<Longrightarrow> x = i"


212 
proof 


213 
fix l assume "l \<in> k" "t \<in> c l"


214 
hence "p l \<in> s \<times> s'" and t_in: "t \<in> a (fst (p l))" "t \<in> b (snd (p l))"


215 
using p unfolding c_def by auto


216 
hence "fst (p l) \<in> s" and "snd (p l) \<in> s'" by auto


217 
with t_in j j' ex1s ex1s' have "p l = (j, j')" by (cases "p l", auto)


218 
thus "l = i"


219 
using `(j, j') = p i` p(2)[THEN inj_onD] `l \<in> k` `i \<in> k` by auto


220 
qed


221 


222 
show "i \<in> k \<and> t \<in> c i"


223 
using `i \<in> k` `t \<in> a j` `t \<in> b j'` c_def i[symmetric] by auto


224 
qed auto


225 
} note ex1 = this


226 


227 
show thesis


228 
proof (rule that)


229 
{ fix t i assume "t \<in> space M" and "i \<in> k"


230 
hence "p i \<in> s \<times> s'" using p(1) by auto


231 
hence "fst (p i) \<in> s" by auto


232 
moreover


233 
assume "t \<in> c i"


234 
hence "t \<in> a (fst (p i))" unfolding c_def by auto


235 
ultimately have "f t = z i" using psf `t \<in> space M`


236 
unfolding z_def pos_simple_def by auto


237 
}


238 
thus "(k, c, z) \<in> pos_simple f"


239 
using psf `finite k` `nonneg z` ck_subset_M ex1


240 
unfolding pos_simple_def by auto


241 


242 
{ fix t i assume "t \<in> space M" and "i \<in> k"


243 
hence "p i \<in> s \<times> s'" using p(1) by auto


244 
hence "snd (p i) \<in> s'" by auto


245 
moreover


246 
assume "t \<in> c i"


247 
hence "t \<in> b (snd (p i))" unfolding c_def by auto


248 
ultimately have "g t = z' i" using psg `t \<in> space M`


249 
unfolding z'_def pos_simple_def by auto


250 
}


251 
thus "(k, c, z') \<in> pos_simple g"


252 
using psg `finite k` `nonneg z'` ck_subset_M ex1


253 
unfolding pos_simple_def by auto


254 
qed


255 
qed


256 

35692

257 
lemma pos_simple_integral_equal:

35582

258 
assumes psx: "(s, a, x) \<in> pos_simple f"


259 
assumes psy: "(s', b, y) \<in> pos_simple f"


260 
shows "pos_simple_integral (s, a, x) = pos_simple_integral (s', b, y)"


261 
unfolding pos_simple_integral_def


262 
proof simp


263 
have "(\<Sum>i\<in>s. x i * measure M (a i)) =


264 
(\<Sum>i\<in>s. (\<Sum>j \<in> s'. x i * measure M (a i \<inter> b j)))" (is "?left = _")


265 
using psy psx unfolding setsum_right_distrib[symmetric]


266 
by (auto intro!: setsum_cong measure_setsum_split elim!: pos_simpleE)


267 
also have "... = (\<Sum>i\<in>s. (\<Sum>j \<in> s'. y j * measure M (a i \<inter> b j)))"


268 
proof (rule setsum_cong, simp, rule setsum_cong, simp_all)


269 
fix i j assume i: "i \<in> s" and j: "j \<in> s'"


270 
hence "a i \<in> sets M" using psx by (auto elim!: pos_simpleE)


271 


272 
show "measure M (a i \<inter> b j) = 0 \<or> x i = y j"


273 
proof (cases "a i \<inter> b j = {}")


274 
case True thus ?thesis using empty_measure by simp


275 
next


276 
case False then obtain t where t: "t \<in> a i" "t \<in> b j" by auto


277 
hence "t \<in> space M" using `a i \<in> sets M` sets_into_space by auto


278 
with psx psy t i j have "x i = f t" and "y j = f t"


279 
unfolding pos_simple_def by auto


280 
thus ?thesis by simp


281 
qed


282 
qed


283 
also have "... = (\<Sum>j\<in>s'. (\<Sum>i\<in>s. y j * measure M (a i \<inter> b j)))"


284 
by (subst setsum_commute) simp


285 
also have "... = (\<Sum>i\<in>s'. y i * measure M (b i))" (is "?sum_sum = ?right")


286 
proof (rule setsum_cong)


287 
fix j assume "j \<in> s'"


288 
have "y j * measure M (b j) = (\<Sum>i\<in>s. y j * measure M (b j \<inter> a i))"


289 
using psx psy `j \<in> s'` unfolding setsum_right_distrib[symmetric]


290 
by (auto intro!: measure_setsum_split elim!: pos_simpleE)


291 
thus "(\<Sum>i\<in>s. y j * measure M (a i \<inter> b j)) = y j * measure M (b j)"


292 
by (auto intro!: setsum_cong arg_cong[where f="measure M"])


293 
qed simp


294 
finally show "?left = ?right" .


295 
qed


296 

35692

297 
lemma psfis_present:

35582

298 
assumes "A \<in> psfis f"


299 
assumes "B \<in> psfis g"


300 
obtains z z' c k where


301 
"A = pos_simple_integral (k, c, z)"


302 
"B = pos_simple_integral (k, c, z')"


303 
"(k, c, z) \<in> pos_simple f"


304 
"(k, c, z') \<in> pos_simple g"


305 
using assms


306 
proof 


307 
from assms obtain s a x s' b y where


308 
ps: "(s, a, x) \<in> pos_simple f" "(s', b, y) \<in> pos_simple g" and


309 
A: "A = pos_simple_integral (s, a, x)" and


310 
B: "B = pos_simple_integral (s', b, y)"


311 
unfolding psfis_def pos_simple_integral_def by auto


312 


313 
guess z z' c k using pos_simple_common_partition[OF ps] . note part = this


314 
show thesis


315 
proof (rule that[of k c z z', OF _ _ part])


316 
show "A = pos_simple_integral (k, c, z)"


317 
unfolding A by (rule pos_simple_integral_equal[OF ps(1) part(1)])


318 
show "B = pos_simple_integral (k, c, z')"


319 
unfolding B by (rule pos_simple_integral_equal[OF ps(2) part(2)])


320 
qed


321 
qed


322 

35692

323 
lemma pos_simple_integral_add:

35582

324 
assumes "(s, a, x) \<in> pos_simple f"


325 
assumes "(s', b, y) \<in> pos_simple g"


326 
obtains s'' c z where


327 
"(s'', c, z) \<in> pos_simple (\<lambda>x. f x + g x)"


328 
"(pos_simple_integral (s, a, x) +


329 
pos_simple_integral (s', b, y) =


330 
pos_simple_integral (s'', c, z))"


331 
using assms


332 
proof 


333 
guess z z' c k


334 
by (rule pos_simple_common_partition[OF `(s, a, x) \<in> pos_simple f ` `(s', b, y) \<in> pos_simple g`])


335 
note kczz' = this


336 
have x: "pos_simple_integral (s, a, x) = pos_simple_integral (k, c, z)"


337 
by (rule pos_simple_integral_equal) (fact, fact)


338 
have y: "pos_simple_integral (s', b, y) = pos_simple_integral (k, c, z')"


339 
by (rule pos_simple_integral_equal) (fact, fact)


340 


341 
have "pos_simple_integral (k, c, (\<lambda> x. z x + z' x))


342 
= (\<Sum> x \<in> k. (z x + z' x) * measure M (c x))"


343 
unfolding pos_simple_integral_def by auto


344 
also have "\<dots> = (\<Sum> x \<in> k. z x * measure M (c x) + z' x * measure M (c x))" using real_add_mult_distrib by auto


345 
also have "\<dots> = (\<Sum> x \<in> k. z x * measure M (c x)) + (\<Sum> x \<in> k. z' x * measure M (c x))" using setsum_addf by auto


346 
also have "\<dots> = pos_simple_integral (k, c, z) + pos_simple_integral (k, c, z')" unfolding pos_simple_integral_def by auto


347 
finally have ths: "pos_simple_integral (s, a, x) + pos_simple_integral (s', b, y) =


348 
pos_simple_integral (k, c, (\<lambda> x. z x + z' x))" using x y by auto


349 
show ?thesis


350 
apply (rule that[of k c "(\<lambda> x. z x + z' x)", OF _ ths])


351 
using kczz' unfolding pos_simple_def nonneg_def by (auto intro!: add_nonneg_nonneg)


352 
qed


353 


354 
lemma psfis_add:


355 
assumes "a \<in> psfis f" "b \<in> psfis g"


356 
shows "a + b \<in> psfis (\<lambda>x. f x + g x)"


357 
using assms pos_simple_integral_add


358 
unfolding psfis_def by auto blast


359 


360 
lemma pos_simple_integral_mono_on_mspace:


361 
assumes f: "(s, a, x) \<in> pos_simple f"


362 
assumes g: "(s', b, y) \<in> pos_simple g"


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


364 
shows "pos_simple_integral (s, a, x) \<le> pos_simple_integral (s', b, y)"


365 
using assms


366 
proof 


367 
guess z z' c k by (rule pos_simple_common_partition[OF f g])


368 
note kczz' = this


369 
(* w = z and w' = z' except where c _ = {} or undef *)


370 
def w == "\<lambda> i. if i \<notin> k \<or> c i = {} then 0 else z i"


371 
def w' == "\<lambda> i. if i \<notin> k \<or> c i = {} then 0 else z' i"


372 
{ fix i


373 
have "w i \<le> w' i"


374 
proof (cases "i \<notin> k \<or> c i = {}")


375 
case False hence "i \<in> k" "c i \<noteq> {}" by auto


376 
then obtain v where v: "v \<in> c i" and "c i \<in> sets M"


377 
using kczz'(1) unfolding pos_simple_def by blast


378 
hence "v \<in> space M" using sets_into_space by blast


379 
with mono[OF `v \<in> space M`] kczz' `i \<in> k` `v \<in> c i`


380 
have "z i \<le> z' i" unfolding pos_simple_def by simp


381 
thus ?thesis unfolding w_def w'_def using False by auto


382 
next


383 
case True thus ?thesis unfolding w_def w'_def by auto


384 
qed


385 
} note w_mn = this


386 


387 
(* some technical stuff for the calculation*)


388 
have "\<And> i. i \<in> k \<Longrightarrow> c i \<in> sets M" using kczz' unfolding pos_simple_def by auto


389 
hence "\<And> i. i \<in> k \<Longrightarrow> measure M (c i) \<ge> 0" using positive by auto


390 
hence w_mono: "\<And> i. i \<in> k \<Longrightarrow> w i * measure M (c i) \<le> w' i * measure M (c i)"


391 
using mult_right_mono w_mn by blast


392 


393 
{ fix i have "\<lbrakk>i \<in> k ; z i \<noteq> w i\<rbrakk> \<Longrightarrow> measure M (c i) = 0"


394 
unfolding w_def by (cases "c i = {}") auto }


395 
hence zw: "\<And> i. i \<in> k \<Longrightarrow> z i * measure M (c i) = w i * measure M (c i)" by auto


396 


397 
{ fix i have "i \<in> k \<Longrightarrow> z i * measure M (c i) = w i * measure M (c i)"


398 
unfolding w_def by (cases "c i = {}") simp_all }


399 
note zw = this


400 


401 
{ fix i have "i \<in> k \<Longrightarrow> z' i * measure M (c i) = w' i * measure M (c i)"


402 
unfolding w'_def by (cases "c i = {}") simp_all }


403 
note z'w' = this


404 


405 
(* the calculation *)


406 
have "pos_simple_integral (s, a, x) = pos_simple_integral (k, c, z)"


407 
using f kczz'(1) by (rule pos_simple_integral_equal)


408 
also have "\<dots> = (\<Sum> i \<in> k. z i * measure M (c i))"


409 
unfolding pos_simple_integral_def by auto


410 
also have "\<dots> = (\<Sum> i \<in> k. w i * measure M (c i))"


411 
using setsum_cong2[of k, OF zw] by auto


412 
also have "\<dots> \<le> (\<Sum> i \<in> k. w' i * measure M (c i))"


413 
using setsum_mono[OF w_mono, of k] by auto


414 
also have "\<dots> = (\<Sum> i \<in> k. z' i * measure M (c i))"


415 
using setsum_cong2[of k, OF z'w'] by auto


416 
also have "\<dots> = pos_simple_integral (k, c, z')"


417 
unfolding pos_simple_integral_def by auto


418 
also have "\<dots> = pos_simple_integral (s', b, y)"


419 
using kczz'(2) g by (rule pos_simple_integral_equal)


420 
finally show "pos_simple_integral (s, a, x) \<le> pos_simple_integral (s', b, y)"


421 
by simp


422 
qed


423 


424 
lemma pos_simple_integral_mono:


425 
assumes a: "(s, a, x) \<in> pos_simple f" "(s', b, y) \<in> pos_simple g"


426 
assumes "\<And> z. f z \<le> g z"


427 
shows "pos_simple_integral (s, a, x) \<le> pos_simple_integral (s', b, y)"


428 
using assms pos_simple_integral_mono_on_mspace by auto


429 


430 
lemma psfis_mono:


431 
assumes "a \<in> psfis f" "b \<in> psfis g"


432 
assumes "\<And> x. x \<in> space M \<Longrightarrow> f x \<le> g x"


433 
shows "a \<le> b"


434 
using assms pos_simple_integral_mono_on_mspace unfolding psfis_def by auto


435 


436 
lemma pos_simple_fn_integral_unique:


437 
assumes "(s, a, x) \<in> pos_simple f" "(s', b, y) \<in> pos_simple f"


438 
shows "pos_simple_integral (s, a, x) = pos_simple_integral (s', b, y)"


439 
using assms real_le_antisym real_le_refl pos_simple_integral_mono by metis


440 


441 
lemma psfis_unique:


442 
assumes "a \<in> psfis f" "b \<in> psfis f"


443 
shows "a = b"


444 
using assms real_le_antisym real_le_refl psfis_mono by metis


445 


446 
lemma pos_simple_integral_indicator:


447 
assumes "A \<in> sets M"


448 
obtains s a x where


449 
"(s, a, x) \<in> pos_simple (indicator_fn A)"


450 
"measure M A = pos_simple_integral (s, a, x)"


451 
using assms


452 
proof 


453 
def s == "{0, 1} :: nat set"


454 
def a == "\<lambda> i :: nat. if i = 0 then A else space M  A"


455 
def x == "\<lambda> i :: nat. if i = 0 then 1 else (0 :: real)"


456 
have eq: "pos_simple_integral (s, a, x) = measure M A"


457 
unfolding s_def a_def x_def pos_simple_integral_def by auto


458 
have "(s, a, x) \<in> pos_simple (indicator_fn A)"


459 
unfolding pos_simple_def indicator_fn_def s_def a_def x_def nonneg_def


460 
using assms sets_into_space by auto


461 
from that[OF this] eq show thesis by auto


462 
qed


463 


464 
lemma psfis_indicator:


465 
assumes "A \<in> sets M"


466 
shows "measure M A \<in> psfis (indicator_fn A)"


467 
using pos_simple_integral_indicator[OF assms]


468 
unfolding psfis_def image_def by auto


469 


470 
lemma pos_simple_integral_mult:


471 
assumes f: "(s, a, x) \<in> pos_simple f"


472 
assumes "0 \<le> z"


473 
obtains s' b y where


474 
"(s', b, y) \<in> pos_simple (\<lambda>x. z * f x)"


475 
"pos_simple_integral (s', b, y) = z * pos_simple_integral (s, a, x)"


476 
using assms that[of s a "\<lambda>i. z * x i"]


477 
by (simp add: pos_simple_def pos_simple_integral_def setsum_right_distrib algebra_simps nonneg_def mult_nonneg_nonneg)


478 


479 
lemma psfis_mult:


480 
assumes "r \<in> psfis f"


481 
assumes "0 \<le> z"


482 
shows "z * r \<in> psfis (\<lambda>x. z * f x)"


483 
using assms


484 
proof 


485 
from assms obtain s a x


486 
where sax: "(s, a, x) \<in> pos_simple f"


487 
and r: "r = pos_simple_integral (s, a, x)"


488 
unfolding psfis_def image_def by auto


489 
obtain s' b y where


490 
"(s', b, y) \<in> pos_simple (\<lambda>x. z * f x)"


491 
"z * pos_simple_integral (s, a, x) = pos_simple_integral (s', b, y)"


492 
using pos_simple_integral_mult[OF sax `0 \<le> z`, of thesis] by auto


493 
thus ?thesis using r unfolding psfis_def image_def by auto


494 
qed


495 


496 
lemma psfis_setsum_image:


497 
assumes "finite P"


498 
assumes "\<And>i. i \<in> P \<Longrightarrow> a i \<in> psfis (f i)"


499 
shows "(setsum a P) \<in> psfis (\<lambda>t. \<Sum>i \<in> P. f i t)"


500 
using assms


501 
proof (induct P)


502 
case empty


503 
let ?s = "{0 :: nat}"


504 
let ?a = "\<lambda> i. if i = (0 :: nat) then space M else {}"


505 
let ?x = "\<lambda> (i :: nat). (0 :: real)"


506 
have "(?s, ?a, ?x) \<in> pos_simple (\<lambda> t. (0 :: real))"


507 
unfolding pos_simple_def image_def nonneg_def by auto


508 
moreover have "(\<Sum> i \<in> ?s. ?x i * measure M (?a i)) = 0" by auto


509 
ultimately have "0 \<in> psfis (\<lambda> t. 0)"


510 
unfolding psfis_def image_def pos_simple_integral_def nonneg_def


511 
by (auto intro!:bexI[of _ "(?s, ?a, ?x)"])


512 
thus ?case by auto


513 
next


514 
case (insert x P) note asms = this


515 
have "finite P" by fact


516 
have "x \<notin> P" by fact


517 
have "(\<And>i. i \<in> P \<Longrightarrow> a i \<in> psfis (f i)) \<Longrightarrow>


518 
setsum a P \<in> psfis (\<lambda>t. \<Sum>i\<in>P. f i t)" by fact


519 
have "setsum a (insert x P) = a x + setsum a P" using `finite P` `x \<notin> P` by auto


520 
also have "\<dots> \<in> psfis (\<lambda> t. f x t + (\<Sum> i \<in> P. f i t))"


521 
using asms psfis_add by auto


522 
also have "\<dots> = psfis (\<lambda> t. \<Sum> i \<in> insert x P. f i t)"


523 
using `x \<notin> P` `finite P` by auto


524 
finally show ?case by simp


525 
qed


526 


527 
lemma psfis_intro:


528 
assumes "a ` P \<subseteq> sets M" and "nonneg x" and "finite P"


529 
shows "(\<Sum>i\<in>P. x i * measure M (a i)) \<in> psfis (\<lambda>t. \<Sum>i\<in>P. x i * indicator_fn (a i) t)"


530 
using assms psfis_mult psfis_indicator


531 
unfolding image_def nonneg_def


532 
by (auto intro!:psfis_setsum_image)


533 


534 
lemma psfis_nonneg: "a \<in> psfis f \<Longrightarrow> nonneg f"


535 
unfolding psfis_def pos_simple_def by auto


536 


537 
lemma pos_psfis: "r \<in> psfis f \<Longrightarrow> 0 \<le> r"


538 
unfolding psfis_def pos_simple_integral_def image_def pos_simple_def nonneg_def


539 
using positive[unfolded positive_def] by (auto intro!:setsum_nonneg mult_nonneg_nonneg)


540 


541 
lemma psfis_borel_measurable:


542 
assumes "a \<in> psfis f"


543 
shows "f \<in> borel_measurable M"


544 
using assms


545 
proof 


546 
from assms obtain s a' x where sa'x: "(s, a', x) \<in> pos_simple f" and sa'xa: "pos_simple_integral (s, a', x) = a"


547 
and fs: "finite s"


548 
unfolding psfis_def pos_simple_integral_def image_def


549 
by (auto elim:pos_simpleE)


550 
{ fix w assume "w \<in> space M"


551 
hence "(f w \<le> a) = ((\<Sum> i \<in> s. x i * indicator_fn (a' i) w) \<le> a)"


552 
using pos_simple_setsum_indicator_fn[OF sa'x, of w] by simp


553 
} hence "\<And> w. (w \<in> space M \<and> f w \<le> a) = (w \<in> space M \<and> (\<Sum> i \<in> s. x i * indicator_fn (a' i) w) \<le> a)"


554 
by auto


555 
{ fix i assume "i \<in> s"


556 
hence "indicator_fn (a' i) \<in> borel_measurable M"


557 
using borel_measurable_indicator using sa'x[unfolded pos_simple_def] by auto


558 
hence "(\<lambda> w. x i * indicator_fn (a' i) w) \<in> borel_measurable M"


559 
using affine_borel_measurable[of "\<lambda> w. indicator_fn (a' i) w" 0 "x i"]


560 
real_mult_commute by auto }


561 
from borel_measurable_setsum_borel_measurable[OF fs this] affine_borel_measurable


562 
have "(\<lambda> w. (\<Sum> i \<in> s. x i * indicator_fn (a' i) w)) \<in> borel_measurable M" by auto


563 
from borel_measurable_cong[OF pos_simple_setsum_indicator_fn[OF sa'x]] this


564 
show ?thesis by simp


565 
qed


566 


567 
lemma psfis_mono_conv_mono:


568 
assumes mono: "mono_convergent u f (space M)"


569 
and ps_u: "\<And>n. x n \<in> psfis (u n)"


570 
and "x > y"


571 
and "r \<in> psfis s"


572 
and f_upper_bound: "\<And>t. t \<in> space M \<Longrightarrow> s t \<le> f t"


573 
shows "r <= y"


574 
proof (rule field_le_mult_one_interval)


575 
fix z :: real assume "0 < z" and "z < 1"


576 
hence "0 \<le> z" by auto


577 
let "?B' n" = "{w \<in> space M. z * s w <= u n w}"


578 


579 
have "incseq x" unfolding incseq_def


580 
proof safe


581 
fix m n :: nat assume "m \<le> n"


582 
show "x m \<le> x n"


583 
proof (rule psfis_mono[OF `x m \<in> psfis (u m)` `x n \<in> psfis (u n)`])


584 
fix t assume "t \<in> space M"


585 
with mono_convergentD[OF mono this] `m \<le> n` show "u m t \<le> u n t"


586 
unfolding incseq_def by auto


587 
qed


588 
qed


589 


590 
from `r \<in> psfis s`


591 
obtain s' a x' where r: "r = pos_simple_integral (s', a, x')"


592 
and ps_s: "(s', a, x') \<in> pos_simple s"


593 
unfolding psfis_def by auto


594 


595 
{ fix t i assume "i \<in> s'" "t \<in> a i"


596 
hence "t \<in> space M" using ps_s by (auto elim!: pos_simpleE) }


597 
note t_in_space = this


598 


599 
{ fix n


600 
from psfis_borel_measurable[OF `r \<in> psfis s`]


601 
psfis_borel_measurable[OF ps_u]


602 
have "?B' n \<in> sets M"


603 
by (auto intro!:


604 
borel_measurable_leq_borel_measurable


605 
borel_measurable_times_borel_measurable


606 
borel_measurable_const) }


607 
note B'_in_M = this


608 


609 
{ fix n have "(\<lambda>i. a i \<inter> ?B' n) ` s' \<subseteq> sets M" using B'_in_M ps_s


610 
by (auto intro!: Int elim!: pos_simpleE) }


611 
note B'_inter_a_in_M = this


612 


613 
let "?sum n" = "(\<Sum>i\<in>s'. x' i * measure M (a i \<inter> ?B' n))"


614 
{ fix n


615 
have "z * ?sum n \<le> x n"


616 
proof (rule psfis_mono[OF _ ps_u])


617 
have *: "\<And>i t. indicator_fn (?B' n) t * (x' i * indicator_fn (a i) t) =


618 
x' i * indicator_fn (a i \<inter> ?B' n) t" unfolding indicator_fn_def by auto


619 
have ps': "?sum n \<in> psfis (\<lambda>t. indicator_fn (?B' n) t * (\<Sum>i\<in>s'. x' i * indicator_fn (a i) t))"


620 
unfolding setsum_right_distrib * using B'_in_M ps_s


621 
by (auto intro!: psfis_intro Int elim!: pos_simpleE)


622 
also have "... = psfis (\<lambda>t. indicator_fn (?B' n) t * s t)" (is "psfis ?l = psfis ?r")


623 
proof (rule psfis_cong)


624 
show "nonneg ?l" using psfis_nonneg[OF ps'] .


625 
show "nonneg ?r" using psfis_nonneg[OF `r \<in> psfis s`] unfolding nonneg_def indicator_fn_def by auto


626 
fix t assume "t \<in> space M"


627 
show "?l t = ?r t" unfolding pos_simple_setsum_indicator_fn[OF ps_s `t \<in> space M`] ..


628 
qed


629 
finally show "z * ?sum n \<in> psfis (\<lambda>t. z * ?r t)" using psfis_mult[OF _ `0 \<le> z`] by simp


630 
next


631 
fix t assume "t \<in> space M"


632 
show "z * (indicator_fn (?B' n) t * s t) \<le> u n t"


633 
using psfis_nonneg[OF ps_u] unfolding nonneg_def indicator_fn_def by auto


634 
qed }


635 
hence *: "\<exists>N. \<forall>n\<ge>N. z * ?sum n \<le> x n" by (auto intro!: exI[of _ 0])


636 


637 
show "z * r \<le> y" unfolding r pos_simple_integral_def


638 
proof (rule LIMSEQ_le[OF mult_right.LIMSEQ `x > y` *],


639 
simp, rule LIMSEQ_setsum, rule mult_right.LIMSEQ)


640 
fix i assume "i \<in> s'"


641 
from psfis_nonneg[OF `r \<in> psfis s`, unfolded nonneg_def]


642 
have "\<And>t. 0 \<le> s t" by simp


643 


644 
have *: "(\<Union>j. a i \<inter> ?B' j) = a i"


645 
proof (safe, simp, safe)


646 
fix t assume "t \<in> a i"


647 
thus "t \<in> space M" using t_in_space[OF `i \<in> s'`] by auto


648 
show "\<exists>j. z * s t \<le> u j t"


649 
proof (cases "s t = 0")


650 
case True thus ?thesis


651 
using psfis_nonneg[OF ps_u] unfolding nonneg_def by auto


652 
next


653 
case False with `0 \<le> s t`


654 
have "0 < s t" by auto


655 
hence "z * s t < 1 * s t" using `0 < z` `z < 1`


656 
by (auto intro!: mult_strict_right_mono simp del: mult_1_left)


657 
also have "... \<le> f t" using f_upper_bound `t \<in> space M` by auto


658 
finally obtain b where "\<And>j. b \<le> j \<Longrightarrow> z * s t < u j t" using `t \<in> space M`


659 
using mono_conv_outgrow[of "\<lambda>n. u n t" "f t" "z * s t"]


660 
using mono_convergentD[OF mono] by auto


661 
from this[of b] show ?thesis by (auto intro!: exI[of _ b])


662 
qed


663 
qed


664 


665 
show "(\<lambda>n. measure M (a i \<inter> ?B' n)) > measure M (a i)"


666 
proof (safe intro!:


667 
monotone_convergence[of "\<lambda>n. a i \<inter> ?B' n", unfolded comp_def *])


668 
fix n show "a i \<inter> ?B' n \<in> sets M"


669 
using B'_inter_a_in_M[of n] `i \<in> s'` by auto


670 
next


671 
fix j t assume "t \<in> space M" and "z * s t \<le> u j t"


672 
thus "z * s t \<le> u (Suc j) t"


673 
using mono_convergentD(1)[OF mono, unfolded incseq_def,


674 
rule_format, of t j "Suc j"]


675 
by auto


676 
qed


677 
qed


678 
qed


679 

35692

680 
section "Continuous posititve integration"


681 


682 
definition


683 
"nnfis f = { y. \<exists>u x. mono_convergent u f (space M) \<and>


684 
(\<forall>n. x n \<in> psfis (u n)) \<and> x > y }"


685 

35582

686 
lemma psfis_nnfis:


687 
"a \<in> psfis f \<Longrightarrow> a \<in> nnfis f"


688 
unfolding nnfis_def mono_convergent_def incseq_def


689 
by (auto intro!: exI[of _ "\<lambda>n. f"] exI[of _ "\<lambda>n. a"] LIMSEQ_const)


690 

35748

691 
lemma nnfis_0: "0 \<in> nnfis (\<lambda> x. 0)"


692 
by (rule psfis_nnfis[OF psfis_0])


693 

35582

694 
lemma nnfis_times:


695 
assumes "a \<in> nnfis f" and "0 \<le> z"


696 
shows "z * a \<in> nnfis (\<lambda>t. z * f t)"


697 
proof 


698 
obtain u x where "mono_convergent u f (space M)" and


699 
"\<And>n. x n \<in> psfis (u n)" "x > a"


700 
using `a \<in> nnfis f` unfolding nnfis_def by auto


701 
with `0 \<le> z`show ?thesis unfolding nnfis_def mono_convergent_def incseq_def


702 
by (auto intro!: exI[of _ "\<lambda>n w. z * u n w"] exI[of _ "\<lambda>n. z * x n"]


703 
LIMSEQ_mult LIMSEQ_const psfis_mult mult_mono1)


704 
qed


705 


706 
lemma nnfis_add:


707 
assumes "a \<in> nnfis f" and "b \<in> nnfis g"


708 
shows "a + b \<in> nnfis (\<lambda>t. f t + g t)"


709 
proof 


710 
obtain u x w y


711 
where "mono_convergent u f (space M)" and


712 
"\<And>n. x n \<in> psfis (u n)" "x > a" and


713 
"mono_convergent w g (space M)" and


714 
"\<And>n. y n \<in> psfis (w n)" "y > b"


715 
using `a \<in> nnfis f` `b \<in> nnfis g` unfolding nnfis_def by auto


716 
thus ?thesis unfolding nnfis_def mono_convergent_def incseq_def


717 
by (auto intro!: exI[of _ "\<lambda>n a. u n a + w n a"] exI[of _ "\<lambda>n. x n + y n"]


718 
LIMSEQ_add LIMSEQ_const psfis_add add_mono)


719 
qed


720 


721 
lemma nnfis_mono:


722 
assumes nnfis: "a \<in> nnfis f" "b \<in> nnfis g"


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


724 
shows "a \<le> b"


725 
proof 


726 
obtain u x w y where


727 
mc: "mono_convergent u f (space M)" "mono_convergent w g (space M)" and


728 
psfis: "\<And>n. x n \<in> psfis (u n)" "\<And>n. y n \<in> psfis (w n)" and


729 
limseq: "x > a" "y > b" using nnfis unfolding nnfis_def by auto


730 
show ?thesis


731 
proof (rule LIMSEQ_le_const2[OF limseq(1)], rule exI[of _ 0], safe)


732 
fix n


733 
show "x n \<le> b"


734 
proof (rule psfis_mono_conv_mono[OF mc(2) psfis(2) limseq(2) psfis(1)])


735 
fix t assume "t \<in> space M"


736 
from mono_convergent_le[OF mc(1) this] mono[OF this]


737 
show "u n t \<le> g t" by (rule order_trans)


738 
qed


739 
qed


740 
qed


741 


742 
lemma nnfis_unique:


743 
assumes a: "a \<in> nnfis f" and b: "b \<in> nnfis f"


744 
shows "a = b"


745 
using nnfis_mono[OF a b] nnfis_mono[OF b a]


746 
by (auto intro!: real_le_antisym[of a b])


747 


748 
lemma psfis_equiv:


749 
assumes "a \<in> psfis f" and "nonneg g"


750 
and "\<And>t. t \<in> space M \<Longrightarrow> f t = g t"


751 
shows "a \<in> psfis g"


752 
using assms unfolding psfis_def pos_simple_def by auto


753 


754 
lemma psfis_mon_upclose:


755 
assumes "\<And>m. a m \<in> psfis (u m)"


756 
shows "\<exists>c. c \<in> psfis (mon_upclose n u)"


757 
proof (induct n)


758 
case 0 thus ?case unfolding mon_upclose.simps using assms ..


759 
next


760 
case (Suc n)


761 
then obtain sn an xn where ps: "(sn, an, xn) \<in> pos_simple (mon_upclose n u)"


762 
unfolding psfis_def by auto


763 
obtain ss as xs where ps': "(ss, as, xs) \<in> pos_simple (u (Suc n))"


764 
using assms[of "Suc n"] unfolding psfis_def by auto


765 
from pos_simple_common_partition[OF ps ps'] guess x x' a s .


766 
hence "(s, a, upclose x x') \<in> pos_simple (mon_upclose (Suc n) u)"


767 
by (simp add: upclose_def pos_simple_def nonneg_def max_def)


768 
thus ?case unfolding psfis_def by auto


769 
qed


770 


771 
text {* BeppoLevi monotone convergence theorem *}


772 
lemma nnfis_mon_conv:


773 
assumes mc: "mono_convergent f h (space M)"


774 
and nnfis: "\<And>n. x n \<in> nnfis (f n)"


775 
and "x > z"


776 
shows "z \<in> nnfis h"


777 
proof 


778 
have "\<forall>n. \<exists>u y. mono_convergent u (f n) (space M) \<and> (\<forall>m. y m \<in> psfis (u m)) \<and>


779 
y > x n"


780 
using nnfis unfolding nnfis_def by auto


781 
from choice[OF this] guess u ..


782 
from choice[OF this] guess y ..


783 
hence mc_u: "\<And>n. mono_convergent (u n) (f n) (space M)"


784 
and psfis: "\<And>n m. y n m \<in> psfis (u n m)" and "\<And>n. y n > x n"


785 
by auto


786 


787 
let "?upclose n" = "mon_upclose n (\<lambda>m. u m n)"


788 


789 
have "\<exists>c. \<forall>n. c n \<in> psfis (?upclose n)"


790 
by (safe intro!: choice psfis_mon_upclose) (rule psfis)


791 
then guess c .. note c = this[rule_format]


792 


793 
show ?thesis unfolding nnfis_def


794 
proof (safe intro!: exI)


795 
show mc_upclose: "mono_convergent ?upclose h (space M)"


796 
by (rule mon_upclose_mono_convergent[OF mc_u mc])


797 
show psfis_upclose: "\<And>n. c n \<in> psfis (?upclose n)"


798 
using c .


799 


800 
{ fix n m :: nat assume "n \<le> m"


801 
hence "c n \<le> c m"


802 
using psfis_mono[OF c c]


803 
using mono_convergentD(1)[OF mc_upclose, unfolded incseq_def]


804 
by auto }


805 
hence "incseq c" unfolding incseq_def by auto


806 


807 
{ fix n


808 
have c_nnfis: "c n \<in> nnfis (?upclose n)" using c by (rule psfis_nnfis)


809 
from nnfis_mono[OF c_nnfis nnfis]


810 
mon_upclose_le_mono_convergent[OF mc_u]


811 
mono_convergentD(1)[OF mc]


812 
have "c n \<le> x n" by fast }


813 
note c_less_x = this


814 


815 
{ fix n


816 
note c_less_x[of n]


817 
also have "x n \<le> z"


818 
proof (rule incseq_le)


819 
show "x > z" by fact


820 
from mono_convergentD(1)[OF mc]


821 
show "incseq x" unfolding incseq_def


822 
by (auto intro!: nnfis_mono[OF nnfis nnfis])


823 
qed


824 
finally have "c n \<le> z" . }


825 
note c_less_z = this


826 


827 
have "convergent c"


828 
proof (rule Bseq_mono_convergent[unfolded incseq_def[symmetric]])


829 
show "Bseq c"


830 
using pos_psfis[OF c] c_less_z


831 
by (auto intro!: BseqI'[of _ z])


832 
show "incseq c" by fact


833 
qed


834 
then obtain l where l: "c > l" unfolding convergent_def by auto


835 


836 
have "l \<le> z" using c_less_x l


837 
by (auto intro!: LIMSEQ_le[OF _ `x > z`])


838 
moreover have "z \<le> l"


839 
proof (rule LIMSEQ_le_const2[OF `x > z`], safe intro!: exI[of _ 0])


840 
fix n


841 
have "l \<in> nnfis h"


842 
unfolding nnfis_def using l mc_upclose psfis_upclose by auto


843 
from nnfis this mono_convergent_le[OF mc]


844 
show "x n \<le> l" by (rule nnfis_mono)


845 
qed


846 
ultimately have "l = z" by (rule real_le_antisym)


847 
thus "c > z" using `c > l` by simp


848 
qed


849 
qed


850 


851 
lemma nnfis_pos_on_mspace:


852 
assumes "a \<in> nnfis f" and "x \<in>space M"


853 
shows "0 \<le> f x"


854 
using assms


855 
proof 


856 
from assms[unfolded nnfis_def] guess u y by auto note uy = this

35748

857 
hence "\<And> n. 0 \<le> u n x"

35582

858 
unfolding nnfis_def psfis_def pos_simple_def nonneg_def mono_convergent_def


859 
by auto


860 
thus "0 \<le> f x" using uy[rule_format]


861 
unfolding nnfis_def psfis_def pos_simple_def nonneg_def mono_convergent_def


862 
using incseq_le[of "\<lambda> n. u n x" "f x"] real_le_trans


863 
by fast


864 
qed


865 


866 
lemma nnfis_borel_measurable:


867 
assumes "a \<in> nnfis f"


868 
shows "f \<in> borel_measurable M"


869 
using assms unfolding nnfis_def


870 
apply auto


871 
apply (rule mono_convergent_borel_measurable)


872 
using psfis_borel_measurable


873 
by auto


874 


875 
lemma borel_measurable_mon_conv_psfis:


876 
assumes f_borel: "f \<in> borel_measurable M"


877 
and nonneg: "\<And>t. t \<in> space M \<Longrightarrow> 0 \<le> f t"


878 
shows"\<exists>u x. mono_convergent u f (space M) \<and> (\<forall>n. x n \<in> psfis (u n))"


879 
proof (safe intro!: exI)


880 
let "?I n" = "{0<..<n * 2^n}"


881 
let "?A n i" = "{w \<in> space M. real (i :: nat) / 2^(n::nat) \<le> f w \<and> f w < real (i + 1) / 2^n}"


882 
let "?u n t" = "\<Sum>i\<in>?I n. real i / 2^n * indicator_fn (?A n i) t"


883 
let "?x n" = "\<Sum>i\<in>?I n. real i / 2^n * measure M (?A n i)"


884 


885 
let "?w n t" = "if f t < real n then real (natfloor (f t * 2^n)) / 2^n else 0"


886 


887 
{ fix t n assume t: "t \<in> space M"


888 
have "?u n t = ?w n t" (is "_ = (if _ then real ?i / _ else _)")


889 
proof (cases "f t < real n")


890 
case True


891 
with nonneg t


892 
have i: "?i < n * 2^n"


893 
by (auto simp: real_of_nat_power[symmetric]


894 
intro!: less_natfloor mult_nonneg_nonneg)


895 


896 
hence t_in_A: "t \<in> ?A n ?i"


897 
unfolding divide_le_eq less_divide_eq


898 
using nonneg t True


899 
by (auto intro!: real_natfloor_le


900 
real_natfloor_gt_diff_one[unfolded diff_less_eq]


901 
simp: real_of_nat_Suc zero_le_mult_iff)


902 


903 
hence *: "real ?i / 2^n \<le> f t"


904 
"f t < real (?i + 1) / 2^n" by auto


905 
{ fix j assume "t \<in> ?A n j"


906 
hence "real j / 2^n \<le> f t"


907 
and "f t < real (j + 1) / 2^n" by auto


908 
with * have "j \<in> {?i}" unfolding divide_le_eq less_divide_eq


909 
by auto }


910 
hence *: "\<And>j. t \<in> ?A n j \<longleftrightarrow> j \<in> {?i}" using t_in_A by auto


911 


912 
have "?u n t = real ?i / 2^n"


913 
unfolding indicator_fn_def if_distrib *


914 
setsum_cases[OF finite_greaterThanLessThan]


915 
using i by (cases "?i = 0") simp_all


916 
thus ?thesis using True by auto


917 
next


918 
case False


919 
have "?u n t = (\<Sum>i \<in> {0 <..< n*2^n}. 0)"


920 
proof (rule setsum_cong)


921 
fix i assume "i \<in> {0 <..< n*2^n}"


922 
hence "i + 1 \<le> n * 2^n" by simp


923 
hence "real (i + 1) \<le> real n * 2^n"


924 
unfolding real_of_nat_le_iff[symmetric]


925 
by (auto simp: real_of_nat_power[symmetric])


926 
also have "... \<le> f t * 2^n"


927 
using False by (auto intro!: mult_nonneg_nonneg)


928 
finally have "t \<notin> ?A n i"


929 
by (auto simp: divide_le_eq less_divide_eq)


930 
thus "real i / 2^n * indicator_fn (?A n i) t = 0"


931 
unfolding indicator_fn_def by auto


932 
qed simp


933 
thus ?thesis using False by auto


934 
qed }


935 
note u_at_t = this


936 


937 
show "mono_convergent ?u f (space M)" unfolding mono_convergent_def


938 
proof safe


939 
fix t assume t: "t \<in> space M"


940 
{ fix m n :: nat assume "m \<le> n"


941 
hence *: "(2::real)^n = 2^m * 2^(n  m)" unfolding class_semiring.mul_pwr by auto


942 
have "real (natfloor (f t * 2^m) * natfloor (2^(nm))) \<le> real (natfloor (f t * 2 ^ n))"


943 
apply (subst *)


944 
apply (subst class_semiring.mul_a)


945 
apply (subst real_of_nat_le_iff)


946 
apply (rule le_mult_natfloor)


947 
using nonneg[OF t] by (auto intro!: mult_nonneg_nonneg)


948 
hence "real (natfloor (f t * 2^m)) * 2^n \<le> real (natfloor (f t * 2^n)) * 2^m"


949 
apply (subst *)


950 
apply (subst (3) class_semiring.mul_c)


951 
apply (subst class_semiring.mul_a)


952 
by (auto intro: mult_right_mono simp: natfloor_power real_of_nat_power[symmetric]) }


953 
thus "incseq (\<lambda>n. ?u n t)" unfolding u_at_t[OF t] unfolding incseq_def


954 
by (auto simp add: le_divide_eq divide_le_eq less_divide_eq)


955 


956 
show "(\<lambda>i. ?u i t) > f t" unfolding u_at_t[OF t]


957 
proof (rule LIMSEQ_I, safe intro!: exI)


958 
fix r :: real and n :: nat


959 
let ?N = "natfloor (1/r) + 1"


960 
assume "0 < r" and N: "max ?N (natfloor (f t) + 1) \<le> n"


961 
hence "?N \<le> n" by auto


962 


963 
have "1 / r < real (natfloor (1/r) + 1)" using real_natfloor_add_one_gt


964 
by (simp add: real_of_nat_Suc)


965 
also have "... < 2^?N" by (rule two_realpow_gt)


966 
finally have less_r: "1 / 2^?N < r" using `0 < r`


967 
by (auto simp: less_divide_eq divide_less_eq algebra_simps)


968 


969 
have "f t < real (natfloor (f t) + 1)" using real_natfloor_add_one_gt[of "f t"] by auto


970 
also have "... \<le> real n" unfolding real_of_nat_le_iff using N by auto


971 
finally have "f t < real n" .


972 


973 
have "real (natfloor (f t * 2^n)) \<le> f t * 2^n"


974 
using nonneg[OF t] by (auto intro!: real_natfloor_le mult_nonneg_nonneg)


975 
hence less: "real (natfloor (f t * 2^n)) / 2^n \<le> f t" unfolding divide_le_eq by auto


976 


977 
have "f t * 2 ^ n  1 < real (natfloor (f t * 2^n))" using real_natfloor_gt_diff_one .


978 
hence "f t  real (natfloor (f t * 2^n)) / 2^n < 1 / 2^n"


979 
by (auto simp: less_divide_eq divide_less_eq algebra_simps)


980 
also have "... \<le> 1 / 2^?N" using `?N \<le> n`


981 
by (auto intro!: divide_left_mono mult_pos_pos simp del: power_Suc)


982 
also have "... < r" using less_r .


983 
finally show "norm (?w n t  f t) < r" using `f t < real n` less by auto


984 
qed


985 
qed


986 


987 
fix n


988 
show "?x n \<in> psfis (?u n)"


989 
proof (rule psfis_intro)


990 
show "?A n ` ?I n \<subseteq> sets M"


991 
proof safe


992 
fix i :: nat


993 
from Int[OF


994 
f_borel[unfolded borel_measurable_less_iff, rule_format, of "real (i+1) / 2^n"]


995 
f_borel[unfolded borel_measurable_ge_iff, rule_format, of "real i / 2^n"]]


996 
show "?A n i \<in> sets M"


997 
by (metis Collect_conj_eq Int_commute Int_left_absorb Int_left_commute)


998 
qed


999 
show "nonneg (\<lambda>i :: nat. real i / 2 ^ n)"


1000 
unfolding nonneg_def by (auto intro!: divide_nonneg_pos)


1001 
qed auto


1002 
qed


1003 


1004 
lemma nnfis_dom_conv:


1005 
assumes borel: "f \<in> borel_measurable M"


1006 
and nnfis: "b \<in> nnfis g"


1007 
and ord: "\<And>t. t \<in> space M \<Longrightarrow> f t \<le> g t"


1008 
and nonneg: "\<And>t. t \<in> space M \<Longrightarrow> 0 \<le> f t"


1009 
shows "\<exists>a. a \<in> nnfis f \<and> a \<le> b"


1010 
proof 


1011 
obtain u x where mc_f: "mono_convergent u f (space M)" and


1012 
psfis: "\<And>n. x n \<in> psfis (u n)"


1013 
using borel_measurable_mon_conv_psfis[OF borel nonneg] by auto


1014 


1015 
{ fix n


1016 
{ fix t assume t: "t \<in> space M"


1017 
note mono_convergent_le[OF mc_f this, of n]


1018 
also note ord[OF t]


1019 
finally have "u n t \<le> g t" . }


1020 
from nnfis_mono[OF psfis_nnfis[OF psfis] nnfis this]


1021 
have "x n \<le> b" by simp }


1022 
note x_less_b = this


1023 


1024 
have "convergent x"


1025 
proof (safe intro!: Bseq_mono_convergent)


1026 
from x_less_b pos_psfis[OF psfis]


1027 
show "Bseq x" by (auto intro!: BseqI'[of _ b])


1028 


1029 
fix n m :: nat assume *: "n \<le> m"


1030 
show "x n \<le> x m"


1031 
proof (rule psfis_mono[OF `x n \<in> psfis (u n)` `x m \<in> psfis (u m)`])


1032 
fix t assume "t \<in> space M"


1033 
from mc_f[THEN mono_convergentD(1), unfolded incseq_def, OF this]


1034 
show "u n t \<le> u m t" using * by auto


1035 
qed


1036 
qed


1037 
then obtain a where "x > a" unfolding convergent_def by auto


1038 
with LIMSEQ_le_const2[OF `x > a`] x_less_b mc_f psfis


1039 
show ?thesis unfolding nnfis_def by auto


1040 
qed


1041 


1042 
lemma the_nnfis[simp]: "a \<in> nnfis f \<Longrightarrow> (THE a. a \<in> nnfis f) = a"


1043 
by (auto intro: the_equality nnfis_unique)


1044 


1045 
lemma nnfis_cong:


1046 
assumes cong: "\<And>x. x \<in> space M \<Longrightarrow> f x = g x"


1047 
shows "nnfis f = nnfis g"


1048 
proof 


1049 
{ fix f g :: "'a \<Rightarrow> real" assume cong: "\<And>x. x \<in> space M \<Longrightarrow> f x = g x"


1050 
fix x assume "x \<in> nnfis f"


1051 
then guess u y unfolding nnfis_def by safe note x = this


1052 
hence "mono_convergent u g (space M)"


1053 
unfolding mono_convergent_def using cong by auto


1054 
with x(2,3) have "x \<in> nnfis g" unfolding nnfis_def by auto }


1055 
from this[OF cong] this[OF cong[symmetric]]


1056 
show ?thesis by safe


1057 
qed


1058 

35692

1059 
section "Lebesgue Integral"


1060 


1061 
definition


1062 
"integrable f \<longleftrightarrow> (\<exists>x. x \<in> nnfis (pos_part f)) \<and> (\<exists>y. y \<in> nnfis (neg_part f))"


1063 


1064 
definition


1065 
"integral f = (THE i :: real. i \<in> nnfis (pos_part f))  (THE j. j \<in> nnfis (neg_part f))"


1066 

35582

1067 
lemma integral_cong:


1068 
assumes cong: "\<And>x. x \<in> space M \<Longrightarrow> f x = g x"


1069 
shows "integral f = integral g"


1070 
proof 


1071 
have "nnfis (pos_part f) = nnfis (pos_part g)"


1072 
using cong by (auto simp: pos_part_def intro!: nnfis_cong)


1073 
moreover


1074 
have "nnfis (neg_part f) = nnfis (neg_part g)"


1075 
using cong by (auto simp: neg_part_def intro!: nnfis_cong)


1076 
ultimately show ?thesis


1077 
unfolding integral_def by auto


1078 
qed


1079 


1080 
lemma nnfis_integral:


1081 
assumes "a \<in> nnfis f"


1082 
shows "integrable f" and "integral f = a"


1083 
proof 


1084 
have a: "a \<in> nnfis (pos_part f)"


1085 
using assms nnfis_pos_on_mspace[OF assms]


1086 
by (auto intro!: nnfis_mon_conv[of "\<lambda>i. f" _ "\<lambda>i. a"]


1087 
LIMSEQ_const simp: mono_convergent_def pos_part_def incseq_def max_def)


1088 


1089 
have "\<And>t. t \<in> space M \<Longrightarrow> neg_part f t = 0"


1090 
unfolding neg_part_def min_def


1091 
using nnfis_pos_on_mspace[OF assms] by auto


1092 
hence 0: "0 \<in> nnfis (neg_part f)"


1093 
by (auto simp: nnfis_def mono_convergent_def psfis_0 incseq_def


1094 
intro!: LIMSEQ_const exI[of _ "\<lambda> x n. 0"] exI[of _ "\<lambda> n. 0"])


1095 


1096 
from 0 a show "integrable f" "integral f = a"


1097 
unfolding integrable_def integral_def by auto


1098 
qed


1099 


1100 
lemma nnfis_minus_nnfis_integral:


1101 
assumes "a \<in> nnfis f" and "b \<in> nnfis g"


1102 
shows "integrable (\<lambda>t. f t  g t)" and "integral (\<lambda>t. f t  g t) = a  b"


1103 
proof 


1104 
have borel: "(\<lambda>t. f t  g t) \<in> borel_measurable M" using assms


1105 
by (blast intro:


1106 
borel_measurable_diff_borel_measurable nnfis_borel_measurable)


1107 


1108 
have "\<exists>x. x \<in> nnfis (pos_part (\<lambda>t. f t  g t)) \<and> x \<le> a + b"


1109 
(is "\<exists>x. x \<in> nnfis ?pp \<and> _")


1110 
proof (rule nnfis_dom_conv)


1111 
show "?pp \<in> borel_measurable M"

35692

1112 
using borel by (rule pos_part_borel_measurable neg_part_borel_measurable)

35582

1113 
show "a + b \<in> nnfis (\<lambda>t. f t + g t)" using assms by (rule nnfis_add)


1114 
fix t assume "t \<in> space M"


1115 
with assms nnfis_add assms[THEN nnfis_pos_on_mspace[OF _ this]]


1116 
show "?pp t \<le> f t + g t" unfolding pos_part_def by auto


1117 
show "0 \<le> ?pp t" using nonneg_pos_part[of "\<lambda>t. f t  g t"]


1118 
unfolding nonneg_def by auto


1119 
qed


1120 
then obtain x where x: "x \<in> nnfis ?pp" by auto


1121 
moreover


1122 
have "\<exists>x. x \<in> nnfis (neg_part (\<lambda>t. f t  g t)) \<and> x \<le> a + b"


1123 
(is "\<exists>x. x \<in> nnfis ?np \<and> _")


1124 
proof (rule nnfis_dom_conv)


1125 
show "?np \<in> borel_measurable M"

35692

1126 
using borel by (rule pos_part_borel_measurable neg_part_borel_measurable)

35582

1127 
show "a + b \<in> nnfis (\<lambda>t. f t + g t)" using assms by (rule nnfis_add)


1128 
fix t assume "t \<in> space M"


1129 
with assms nnfis_add assms[THEN nnfis_pos_on_mspace[OF _ this]]


1130 
show "?np t \<le> f t + g t" unfolding neg_part_def by auto


1131 
show "0 \<le> ?np t" using nonneg_neg_part[of "\<lambda>t. f t  g t"]


1132 
unfolding nonneg_def by auto


1133 
qed


1134 
then obtain y where y: "y \<in> nnfis ?np" by auto


1135 
ultimately show "integrable (\<lambda>t. f t  g t)"


1136 
unfolding integrable_def by auto


1137 


1138 
from x and y


1139 
have "a + y \<in> nnfis (\<lambda>t. f t + ?np t)"


1140 
and "b + x \<in> nnfis (\<lambda>t. g t + ?pp t)" using assms by (auto intro: nnfis_add)


1141 
moreover


1142 
have "\<And>t. f t + ?np t = g t + ?pp t"


1143 
unfolding pos_part_def neg_part_def by auto


1144 
ultimately have "a  b = x  y"


1145 
using nnfis_unique by (auto simp: algebra_simps)


1146 
thus "integral (\<lambda>t. f t  g t) = a  b"


1147 
unfolding integral_def


1148 
using the_nnfis[OF x] the_nnfis[OF y] by simp


1149 
qed


1150 


1151 
lemma integral_borel_measurable:


1152 
"integrable f \<Longrightarrow> f \<in> borel_measurable M"


1153 
unfolding integrable_def


1154 
by (subst pos_part_neg_part_borel_measurable_iff)


1155 
(auto intro: nnfis_borel_measurable)


1156 


1157 
lemma integral_indicator_fn:


1158 
assumes "a \<in> sets M"


1159 
shows "integral (indicator_fn a) = measure M a"


1160 
and "integrable (indicator_fn a)"


1161 
using psfis_indicator[OF assms, THEN psfis_nnfis]


1162 
by (auto intro!: nnfis_integral)


1163 


1164 
lemma integral_add:


1165 
assumes "integrable f" and "integrable g"


1166 
shows "integrable (\<lambda>t. f t + g t)"


1167 
and "integral (\<lambda>t. f t + g t) = integral f + integral g"


1168 
proof 


1169 
{ fix t


1170 
have "pos_part f t + pos_part g t  (neg_part f t + neg_part g t) =


1171 
f t + g t"


1172 
unfolding pos_part_def neg_part_def by auto }


1173 
note part_sum = this


1174 


1175 
from assms obtain a b c d where


1176 
a: "a \<in> nnfis (pos_part f)" and b: "b \<in> nnfis (neg_part f)" and


1177 
c: "c \<in> nnfis (pos_part g)" and d: "d \<in> nnfis (neg_part g)"


1178 
unfolding integrable_def by auto


1179 
note sums = nnfis_add[OF a c] nnfis_add[OF b d]


1180 
note int = nnfis_minus_nnfis_integral[OF sums, unfolded part_sum]


1181 


1182 
show "integrable (\<lambda>t. f t + g t)" using int(1) .


1183 


1184 
show "integral (\<lambda>t. f t + g t) = integral f + integral g"


1185 
using int(2) sums a b c d by (simp add: the_nnfis integral_def)


1186 
qed


1187 


1188 
lemma integral_mono:


1189 
assumes "integrable f" and "integrable g"


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


1191 
shows "integral f \<le> integral g"


1192 
proof 


1193 
from assms obtain a b c d where


1194 
a: "a \<in> nnfis (pos_part f)" and b: "b \<in> nnfis (neg_part f)" and


1195 
c: "c \<in> nnfis (pos_part g)" and d: "d \<in> nnfis (neg_part g)"


1196 
unfolding integrable_def by auto


1197 


1198 
have "a \<le> c"


1199 
proof (rule nnfis_mono[OF a c])


1200 
fix t assume "t \<in> space M"


1201 
from mono[OF this] show "pos_part f t \<le> pos_part g t"


1202 
unfolding pos_part_def by auto


1203 
qed


1204 
moreover have "d \<le> b"


1205 
proof (rule nnfis_mono[OF d b])


1206 
fix t assume "t \<in> space M"


1207 
from mono[OF this] show "neg_part g t \<le> neg_part f t"


1208 
unfolding neg_part_def by auto


1209 
qed


1210 
ultimately have "a  b \<le> c  d" by auto


1211 
thus ?thesis unfolding integral_def


1212 
using a b c d by (simp add: the_nnfis)


1213 
qed


1214 


1215 
lemma integral_uminus:


1216 
assumes "integrable f"


1217 
shows "integrable (\<lambda>t.  f t)"


1218 
and "integral (\<lambda>t.  f t) =  integral f"


1219 
proof 


1220 
have "pos_part f = neg_part (\<lambda>t.f t)" and "neg_part f = pos_part (\<lambda>t.f t)"


1221 
unfolding pos_part_def neg_part_def by (auto intro!: ext)


1222 
with assms show "integrable (\<lambda>t.f t)" and "integral (\<lambda>t.f t) = integral f"


1223 
unfolding integrable_def integral_def by simp_all


1224 
qed


1225 


1226 
lemma integral_times_const:


1227 
assumes "integrable f"


1228 
shows "integrable (\<lambda>t. a * f t)" (is "?P a")


1229 
and "integral (\<lambda>t. a * f t) = a * integral f" (is "?I a")


1230 
proof 


1231 
{ fix a :: real assume "0 \<le> a"


1232 
hence "pos_part (\<lambda>t. a * f t) = (\<lambda>t. a * pos_part f t)"


1233 
and "neg_part (\<lambda>t. a * f t) = (\<lambda>t. a * neg_part f t)"


1234 
unfolding pos_part_def neg_part_def max_def min_def


1235 
by (auto intro!: ext simp: zero_le_mult_iff)


1236 
moreover


1237 
obtain x y where x: "x \<in> nnfis (pos_part f)" and y: "y \<in> nnfis (neg_part f)"


1238 
using assms unfolding integrable_def by auto


1239 
ultimately


1240 
have "a * x \<in> nnfis (pos_part (\<lambda>t. a * f t))" and


1241 
"a * y \<in> nnfis (neg_part (\<lambda>t. a * f t))"


1242 
using nnfis_times[OF _ `0 \<le> a`] by auto


1243 
with x y have "?P a \<and> ?I a"


1244 
unfolding integrable_def integral_def by (auto simp: algebra_simps) }


1245 
note int = this


1246 


1247 
have "?P a \<and> ?I a"


1248 
proof (cases "0 \<le> a")


1249 
case True from int[OF this] show ?thesis .


1250 
next


1251 
case False with int[of " a"] integral_uminus[of "\<lambda>t.  a * f t"]


1252 
show ?thesis by auto


1253 
qed


1254 
thus "integrable (\<lambda>t. a * f t)"


1255 
and "integral (\<lambda>t. a * f t) = a * integral f" by simp_all


1256 
qed


1257 


1258 
lemma integral_cmul_indicator:


1259 
assumes "s \<in> sets M"


1260 
shows "integral (\<lambda>x. c * indicator_fn s x) = c * (measure M s)"


1261 
and "integrable (\<lambda>x. c * indicator_fn s x)"


1262 
using assms integral_times_const integral_indicator_fn by auto


1263 


1264 
lemma integral_zero:


1265 
shows "integral (\<lambda>x. 0) = 0"


1266 
and "integrable (\<lambda>x. 0)"


1267 
using integral_cmul_indicator[OF empty_sets, of 0]


1268 
unfolding indicator_fn_def by auto


1269 


1270 
lemma integral_setsum:


1271 
assumes "finite S"


1272 
assumes "\<And>n. n \<in> S \<Longrightarrow> integrable (f n)"


1273 
shows "integral (\<lambda>x. \<Sum> i \<in> S. f i x) = (\<Sum> i \<in> S. integral (f i))" (is "?int S")


1274 
and "integrable (\<lambda>x. \<Sum> i \<in> S. f i x)" (is "?I s")


1275 
proof 


1276 
from assms have "?int S \<and> ?I S"


1277 
proof (induct S)


1278 
case empty thus ?case by (simp add: integral_zero)


1279 
next


1280 
case (insert i S)


1281 
thus ?case


1282 
apply simp


1283 
apply (subst integral_add)


1284 
using assms apply auto


1285 
apply (subst integral_add)


1286 
using assms by auto


1287 
qed


1288 
thus "?int S" and "?I S" by auto


1289 
qed


1290 

36624

1291 
lemma (in measure_space) integrable_abs:


1292 
assumes "integrable f"


1293 
shows "integrable (\<lambda> x. \<bar>f x\<bar>)"


1294 
using assms


1295 
proof 


1296 
from assms obtain p q where pq: "p \<in> nnfis (pos_part f)" "q \<in> nnfis (neg_part f)"


1297 
unfolding integrable_def by auto


1298 
hence "p + q \<in> nnfis (\<lambda> x. pos_part f x + neg_part f x)"


1299 
using nnfis_add by auto


1300 
hence "p + q \<in> nnfis (\<lambda> x. \<bar>f x\<bar>)" using pos_neg_part_abs[of f] by simp


1301 
thus ?thesis unfolding integrable_def


1302 
using ext[OF pos_part_abs[of f], of "\<lambda> y. y"]


1303 
ext[OF neg_part_abs[of f], of "\<lambda> y. y"]


1304 
using nnfis_0 by auto


1305 
qed


1306 

35582

1307 
lemma markov_ineq:


1308 
assumes "integrable f" "0 < a" "integrable (\<lambda>x. \<bar>f x\<bar>^n)"


1309 
shows "measure M (f ` {a ..} \<inter> space M) \<le> integral (\<lambda>x. \<bar>f x\<bar>^n) / a^n"


1310 
using assms


1311 
proof 


1312 
from assms have "0 < a ^ n" using real_root_pow_pos by auto


1313 
from assms have "f \<in> borel_measurable M"


1314 
using integral_borel_measurable[OF `integrable f`] by auto


1315 
hence w: "{w . w \<in> space M \<and> a \<le> f w} \<in> sets M"


1316 
using borel_measurable_ge_iff by auto


1317 
have i: "integrable (indicator_fn {w . w \<in> space M \<and> a \<le> f w})"


1318 
using integral_indicator_fn[OF w] by simp


1319 
have v1: "\<And> t. a ^ n * (indicator_fn {w . w \<in> space M \<and> a \<le> f w}) t


1320 
\<le> (f t) ^ n * (indicator_fn {w . w \<in> space M \<and> a \<le> f w}) t"


1321 
unfolding indicator_fn_def


1322 
using `0 < a` power_mono[of a] assms by auto


1323 
have v2: "\<And> t. (f t) ^ n * (indicator_fn {w . w \<in> space M \<and> a \<le> f w}) t \<le> \<bar>f t\<bar> ^ n"


1324 
unfolding indicator_fn_def


1325 
using power_mono[of a _ n] abs_ge_self `a > 0`


1326 
by auto


1327 
have "{w \<in> space M. a \<le> f w} \<inter> space M = {w . a \<le> f w} \<inter> space M"


1328 
using Collect_eq by auto


1329 
from Int_absorb2[OF sets_into_space[OF w]] `0 < a ^ n` sets_into_space[OF w] w this


1330 
have "(a ^ n) * (measure M ((f ` {y . a \<le> y}) \<inter> space M)) =


1331 
(a ^ n) * measure M {w . w \<in> space M \<and> a \<le> f w}"


1332 
unfolding vimage_Collect_eq[of f] by simp


1333 
also have "\<dots> = integral (\<lambda> t. a ^ n * (indicator_fn {w . w \<in> space M \<and> a \<le> f w}) t)"


1334 
using integral_cmul_indicator[OF w] i by auto


1335 
also have "\<dots> \<le> integral (\<lambda> t. \<bar> f t \<bar> ^ n)"


1336 
apply (rule integral_mono)


1337 
using integral_cmul_indicator[OF w]


1338 
`integrable (\<lambda> x. \<bar>f x\<bar> ^ n)` real_le_trans[OF v1 v2] by auto


1339 
finally show "measure M (f ` {a ..} \<inter> space M) \<le> integral (\<lambda>x. \<bar>f x\<bar>^n) / a^n"


1340 
unfolding atLeast_def


1341 
by (auto intro!: mult_imp_le_div_pos[OF `0 < a ^ n`], simp add: real_mult_commute)


1342 
qed


1343 

36624

1344 
lemma (in measure_space) integral_0:


1345 
fixes f :: "'a \<Rightarrow> real"


1346 
assumes "integrable f" "integral f = 0" "nonneg f" and borel: "f \<in> borel_measurable M"


1347 
shows "measure M ({x. f x \<noteq> 0} \<inter> space M) = 0"


1348 
proof 


1349 
have "{x. f x \<noteq> 0} = {x. \<bar>f x\<bar> > 0}" by auto


1350 
moreover


1351 
{ fix y assume "y \<in> {x. \<bar> f x \<bar> > 0}"


1352 
hence "\<bar> f y \<bar> > 0" by auto


1353 
hence "\<exists> n. \<bar>f y\<bar> \<ge> inverse (real (Suc n))"


1354 
using ex_inverse_of_nat_Suc_less[of "\<bar>f y\<bar>"] less_imp_le unfolding real_of_nat_def by auto


1355 
hence "y \<in> (\<Union> n. {x. \<bar>f x\<bar> \<ge> inverse (real (Suc n))})"


1356 
by auto }


1357 
moreover


1358 
{ fix y assume "y \<in> (\<Union> n. {x. \<bar>f x\<bar> \<ge> inverse (real (Suc n))})"


1359 
then obtain n where n: "y \<in> {x. \<bar>f x\<bar> \<ge> inverse (real (Suc n))}" by auto


1360 
hence "\<bar>f y\<bar> \<ge> inverse (real (Suc n))" by auto


1361 
hence "\<bar>f y\<bar> > 0"


1362 
using real_of_nat_Suc_gt_zero


1363 
positive_imp_inverse_positive[of "real_of_nat (Suc n)"] by fastsimp


1364 
hence "y \<in> {x. \<bar>f x\<bar> > 0}" by auto }


1365 
ultimately have fneq0_UN: "{x. f x \<noteq> 0} = (\<Union> n. {x. \<bar>f x\<bar> \<ge> inverse (real (Suc n))})"


1366 
by blast


1367 
{ fix n


1368 
have int_one: "integrable (\<lambda> x. \<bar>f x\<bar> ^ 1)" using integrable_abs assms by auto


1369 
have "measure M (f ` {inverse (real (Suc n))..} \<inter> space M)


1370 
\<le> integral (\<lambda> x. \<bar>f x\<bar> ^ 1) / (inverse (real (Suc n)) ^ 1)"


1371 
using markov_ineq[OF `integrable f` _ int_one] real_of_nat_Suc_gt_zero by auto


1372 
hence le0: "measure M (f ` {inverse (real (Suc n))..} \<inter> space M) \<le> 0"


1373 
using assms unfolding nonneg_def by auto


1374 
have "{x. f x \<ge> inverse (real (Suc n))} \<inter> space M \<in> sets M"


1375 
apply (subst Int_commute) unfolding Int_def


1376 
using borel[unfolded borel_measurable_ge_iff] by simp


1377 
hence m0: "measure M ({x. f x \<ge> inverse (real (Suc n))} \<inter> space M) = 0 \<and>


1378 
{x. f x \<ge> inverse (real (Suc n))} \<inter> space M \<in> sets M"


1379 
using positive le0 unfolding atLeast_def by fastsimp }


1380 
moreover hence "range (\<lambda> n. {x. f x \<ge> inverse (real (Suc n))} \<inter> space M) \<subseteq> sets M"


1381 
by auto


1382 
moreover


1383 
{ fix n


1384 
have "inverse (real (Suc n)) \<ge> inverse (real (Suc (Suc n)))"


1385 
using less_imp_inverse_less real_of_nat_Suc_gt_zero[of n] by fastsimp


1386 
hence "\<And> x. f x \<ge> inverse (real (Suc n)) \<Longrightarrow> f x \<ge> inverse (real (Suc (Suc n)))" by (rule order_trans)


1387 
hence "{x. f x \<ge> inverse (real (Suc n))} \<inter> space M


1388 
\<subseteq> {x. f x \<ge> inverse (real (Suc (Suc n)))} \<inter> space M" by auto }


1389 
ultimately have "(\<lambda> x. 0) > measure M (\<Union> n. {x. f x \<ge> inverse (real (Suc n))} \<inter> space M)"


1390 
using monotone_convergence[of "\<lambda> n. {x. f x \<ge> inverse (real (Suc n))} \<inter> space M"]


1391 
unfolding o_def by (simp del: of_nat_Suc)


1392 
hence "measure M (\<Union> n. {x. f x \<ge> inverse (real (Suc n))} \<inter> space M) = 0"


1393 
using LIMSEQ_const[of 0] LIMSEQ_unique by simp


1394 
hence "measure M ((\<Union> n. {x. \<bar>f x\<bar> \<ge> inverse (real (Suc n))}) \<inter> space M) = 0"


1395 
using assms unfolding nonneg_def by auto


1396 
thus "measure M ({x. f x \<noteq> 0} \<inter> space M) = 0" using fneq0_UN by simp


1397 
qed


1398 

35748

1399 
section "Lebesgue integration on countable spaces"


1400 


1401 
lemma nnfis_on_countable:


1402 
assumes borel: "f \<in> borel_measurable M"


1403 
and bij: "bij_betw enum S (f ` space M  {0})"


1404 
and enum_zero: "enum ` (S) \<subseteq> {0}"


1405 
and nn_enum: "\<And>n. 0 \<le> enum n"


1406 
and sums: "(\<lambda>r. enum r * measure M (f ` {enum r} \<inter> space M)) sums x" (is "?sum sums x")


1407 
shows "x \<in> nnfis f"


1408 
proof 


1409 
have inj_enum: "inj_on enum S"


1410 
and range_enum: "enum ` S = f ` space M  {0}"


1411 
using bij by (auto simp: bij_betw_def)


1412 


1413 
let "?x n z" = "\<Sum>i = 0..<n. enum i * indicator_fn (f ` {enum i} \<inter> space M) z"


1414 


1415 
show ?thesis


1416 
proof (rule nnfis_mon_conv)


1417 
show "(\<lambda>n. \<Sum>i = 0..<n. ?sum i) > x" using sums unfolding sums_def .


1418 
next

