# Theory Integral

theory Integral
imports RealRandVar
(* The Lebesgue Integral

Stefan Richter 2002 *)

section ‹The three-step approach \label{sec:stepwise-approach}›

theory Integral
imports RealRandVar
begin
(*simple function integral set*)
text ‹Having learnt from my failures, we take the safe and clean way
of Heinz Bauer \cite{Bauer}. It proceeds as outlined in the
introduction. In three steps, we fix the integral for elementary
(step-'')functions, for limits of these, and finally for
differences between such limits.
›

subsection ‹Simple functions \label{sec:simple-fun}›

text ‹
A simple function is a finite sum of characteristic functions, each
multiplied with a nonnegative constant. These functions must be
parametrized by measurable sets. Note that to check this condition,
a tuple consisting of
a set of measurable sets and a measure is required as
the integral operator's second argument, whereas the
measure only is given in informal notation. Usually the tuple will
be a measure space, though it is not required so by the definition at
this point.

It is most natural to declare the value of the integral in this
elementary case by simply replacing the characteristic functions
with the measures of their respective sets. Uniqueness remains to be
shown, for a function may have
infinitely many decompositions and these might give rise to more
than one integral value. This is why we construct a \emph{simple
function integral set} for any function and measurable sets/measure
pair by means of an inductive set definition containing but one
introduction rule.
›

inductive_set
sfis:: "('a ⇒ real) ⇒ ('a set set * ('a set ⇒ real)) ⇒ real set"
for f :: "'a ⇒ real" and M :: "'a set set * ('a set ⇒ real)"
where (*This uses normal forms*)
base:  "⟦f = (λt. ∑i∈(S::nat set). x i * χ (A i) t);
∀i ∈ S. A i ∈ measurable_sets M; nonnegative x; finite S;
∀i∈S. ∀j∈S. i ≠ j ⟶ A i ∩ A j = {}; (⋃i∈S. A i) = UNIV⟧
⟹ (∑i∈S. x i * measure M (A i)) ∈ sfis f M"
(*S may not be polymorphic*)

text‹As you can see we require two extra conditions, and they amount
to the sets being a partition of the universe. We say that a
function is in normal form if it is represented this way. Normal
forms are only needed to show additivity and monotonicity of simple
function integral sets. These theorems can then be used in turn to
get rid of the normality condition.

More precisely, normal forms
play a central role in the ‹sfis_present› lemma. For two
simple functions with different underlying partitions it states
the existence of a common finer-grained partition that can be used
to represent the functions uniformly. The proof is remarkably
lengthy, another case where informal reasoning is more intricate
than it seems. The reason it is included anyway, with the exception
of the two following lemmata, is that it gives insight into the
arising complication and its formal solution.

The problem is in the use of informal sum
notation, which easily permits for a change in index sets, allowing
for a pair of indices. This change has to be rectified in formal
reasoning. Luckily, the task is eased by an injective function from
$\mathbb{N}^2$ into $\mathbb{N}$, which was developed for the
rationals mentioned in \ref{sec:realrandvar}.
It might have been still easier if index sets were
polymorphic in our integral definition, permitting pairs to be
formed when necessary, but the logic doesn't allow for this.›

lemma assumes un: "(⋃i∈R. B i) = UNIV" and fin: "finite R"
and dis: "∀j1∈R. ∀j2∈R. j1 ≠ j2 ⟶ (B j1) ∩ (B j2) = {}"
shows char_split: "χ A t = (∑j∈R. χ (A ∩ B j) t)"
(*<*)proof (cases "t ∈ A")
case True
with un obtain j where jR: "j∈R" and tj: "t ∈ A ∩ B j" by fast
from tj have "χ (A ∩ B j) t = 1" by (simp add: characteristic_function_def)
with fin jR have "(∑i∈R-{j}. χ (A ∩ B i) t) = (∑i∈R. χ (A ∩ B i) t) - 1"
by (simp add: sum_diff1)
also
from dis jR tj have "R-{j} = R-{j}" and "⋀x. x ∈ R-{j} ⟹ χ (A ∩ B x) t = 0"
by (auto simp add: characteristic_function_def)
hence "(∑i∈R-{j}. χ (A ∩ B i) t) = (∑i∈R-{j}. 0)" by (rule sum.cong)
finally have "1 = (∑i∈R. χ (A ∩ B i) t)" by (simp)
with True show ?thesis by (simp add: characteristic_function_def)
next
case False
hence "⋀i. χ (A ∩ B i) t = 0" by (simp add: characteristic_function_def)
hence "0 = (∑i∈R. χ (A ∩ B i) t)" by (simp)
with False show ?thesis by (simp add: characteristic_function_def)
qed

lemma assumes ms: "measure_space M" and dis: "∀j1∈(R::nat set). ∀j2∈R. j1 ≠ j2 ⟶ (B j1) ∩ (B j2) = {}"
and meas: "∀j∈R. B j ∈ measurable_sets M"
shows measure_sums_UNION: "(λn. measure M (if n ∈ R then B n else {})) sums measure M (⋃i∈R. B i)"
(*<*)proof -
have eq: "(⋃i∈R. B i) = (⋃i. if i∈R then B i else {})"
by (auto split: if_splits)

from dis have dis2: "(∀i j. i ≠ j ⟶ (if i∈R then B i else {}) ∩ (if j∈R then B j else {})  = {})"
by simp

from meas have meas2: "range (λi. if i∈R then B i else {}) ⊆ measurable_sets M"
using ms by (auto simp add: measure_space_def sigma_algebra_def)
hence "∀i. (if i∈R then B i else {})∈ measurable_sets M"
by auto
with ms have "(⋃i. if i∈R then B i else {}) ∈ measurable_sets M"
by (auto simp add: measure_space_def sigma_algebra_def) (use eq in presburger)
with meas2 dis2 have "(λn. measure M (if n ∈ R then B n else {}))
sums measure M (⋃i. if i∈R then B i else {})"
using ms by (simp add: measure_space_def countably_additive_def cong: SUP_cong_simp)
with eq show ?thesis
by simp
qed(*>*)

lemma sumr_sum:
"(∑i=0..<k::nat. if i ∈ R then f i else (0::real)) = (∑i∈(R∩{..<k}). f i)"
(*<*)proof (induct k)
case 0
thus ?case
by simp
case (Suc l)
hence "(∑i=0..<Suc l. if i ∈ R then f i else 0) =
(if l ∈ R then f l else 0) + (∑i∈(R∩{..<l}). f i)"
by simp
also have "… =  (∑i∈(R ∩ {..<Suc l}). f i)"
proof (cases "l ∈ R")
case True
have "l ∉ (R∩{..<l})" by simp
have "f l + (∑i∈(R∩{..<l}). f i) = (∑i∈(insert l (R∩{..<l})). f i)"
by simp
also from True have "insert l (R∩{..<l}) = (R ∩ {..<Suc l})"
by (auto simp add: lessThan_Suc)
finally show ?thesis
using True by simp
next
case False
hence "(R∩{..<l}) = (R ∩ {..<Suc l})" by (auto simp add: lessThan_Suc)
thus ?thesis by auto
qed
finally show ?case .
qed(*>*)

lemma assumes ms: "measure_space M" and dis: "∀j1∈(R::nat set). ∀j2∈R. j1 ≠ j2 ⟶ (B j1) ∩ (B j2) = {}"
and meas: "∀j∈R. B j ∈ measurable_sets M" and fin: "finite R"
shows measure_sum: "measure M (⋃i∈R. B i) = (∑j∈R. measure M (B j))"
(*<*)proof (cases "R={}")
case False
with fin have leR: "∀r∈R. r  ≤ Max R"
by simp
hence "R = R ∩ {..Max R}"
by auto
also have "… = R ∩ {..<Suc (Max R)}"
by (simp add: lessThan_Suc_atMost[THEN sym])
finally have "(∑j∈R. measure M (B j)) = (∑j∈R∩ {..<Suc (Max R)} . measure M (B j))"
by simp
also have "… = (∑x=0..<Suc(Max R). if x ∈ R then measure M (B x) else 0)"
by (rule sumr_sum[THEN sym])
also {
fix x
from ms have "(if x ∈ R then measure M (B x) else 0) = (measure M (if x∈R then B x else {}))"
by (simp add: measure_space_def positive_def)
}
hence "… = (∑x=0..<Suc(Max R). measure M (if x∈R then B x else {}))" by simp
also {
fix m
assume "Suc (Max R) ≤ m"
hence "Max R < m" by simp
with leR have "m∉R" by auto
with ms have "measure M (if m∈R then B m else {}) = 0"
by (simp add: measure_space_def positive_def)
}
hence "∀m. (Suc (Max R)) ≤ m ⟶ measure M (if m∈R then B m else {}) = 0"
by simp
hence "(λn. measure M (if n ∈ R then B n else {})) sums (∑x=0..<Suc(Max R). measure M (if x∈R then B x else {}))"
by (intro sums_finite) auto
hence "(∑x=0..<Suc(Max R). measure M (if x∈R then B x else {})) = suminf (λn. measure M (if n ∈ R then B n else {}))"
by (rule sums_unique)
also from ms dis meas have "(λn. measure M (if n ∈ R then B n else {})) sums measure M (⋃i∈R. B i)"
by (rule measure_sums_UNION)
ultimately show ?thesis  by (simp add: sums_unique)
next
case True
with ms show ?thesis by (simp add: measure_space_def positive_def)
qed(*>*)

lemma assumes ms: "measure_space M" and un: "(⋃i∈R. B i) = UNIV" and
fin: "finite (R::nat set)" and dis: "∀j1∈R. ∀j2∈R. j1 ≠ j2 ⟶ (B j1) ∩ (B j2) = {}"
and meas: "∀j∈R. B j ∈ measurable_sets M" and Ameas: "A ∈ measurable_sets M"
shows measure_split: "measure M A = (∑j∈R. measure M (A ∩ B j))"
(*<*)proof -
note ms moreover
from dis have "∀j1∈R. ∀j2∈R. j1 ≠ j2 ⟶ (A ∩ B j1) ∩ (A ∩ B j2) = {}"
by fast
moreover
from ms meas Ameas have "∀j∈R. A ∩ B j ∈ measurable_sets M"
by (simp add: measure_space_def sigma_algebra_inter)
moreover note fin
ultimately have "measure M (⋃i∈R. A ∩ B i) = (∑j∈R. measure M (A ∩ B j))"
by (rule measure_sum)
also
from un have "A = (⋃i∈R. A ∩ B i)"
by auto
ultimately show ?thesis
by simp
qed(*>*)

lemma prod_encode_fst_inj: "inj (λi. prod_encode(i,j))" using inj_prod_encode
by (unfold inj_on_def) blast

lemma prod_encode_snd_inj: "inj (λj. prod_encode(i,j))" using inj_prod_encode
by (unfold inj_on_def) blast

(*>*)
lemma assumes (*<*)ms:(*>*) "measure_space M" and (*<*)a:(*>*) "a ∈ sfis f M" and (*<*)b:(*>*) "b ∈ sfis g M"
shows sfis_present: "∃ z1 z2 C K.
f = (λt. ∑i∈(K::nat set). z1 i * χ (C i) t) ∧ g = (λt. ∑i∈K. z2 i * χ (C i) t)
∧ a = (∑i∈K. z1 i * measure M (C i)) ∧ b = (∑i∈K. z2 i * measure M (C i))
∧ finite K ∧ (∀i∈K. ∀j∈K. i ≠ j ⟶ C i ∩ C j = {})
∧ (∀i ∈ K. C i ∈ measurable_sets M) ∧ (⋃i∈K. C i) = UNIV
∧ nonnegative z1 ∧ nonnegative z2"
using a
proof cases
case (base x A R)
note base_x = this
show ?thesis using b
proof cases
case (base y B S)

with assms base_x have ms: "measure_space M"
and f: "f = (λt. ∑i∈(R::nat set). x i * χ (A i) t)"
and a: "a = (∑i∈R. x i * measure M (A i))"
and Ams: "∀i ∈ R. A i ∈ measurable_sets M"
and R: "finite R" and Adis: "∀i∈R. ∀j∈R. i ≠ j ⟶ A i ∩ A j = {}"
and Aun: "(⋃i∈R. A i) = UNIV"
and g: "g = (λt. ∑i∈(S::nat set). y i * χ (B i) t)"
and b: "b = (∑j∈S. y j * measure M (B j))"
and Bms: "∀i ∈ S. B i ∈ measurable_sets M"
and S: "finite S"
and Bdis: "∀i∈S. ∀j∈S. i ≠ j ⟶ B i ∩ B j = {}"
and Bun: "(⋃i∈S. B i) = UNIV"
and x: "nonnegative x" and y: "nonnegative y"
by simp_all
txt‹\nopagebreak›
define C where "C = (λ(i,j). A i ∩ B j) ∘ prod_decode"
define z1 where "z1 k = x (fst (prod_decode k))" for k
define z2 where "z2 k = y (snd (prod_decode k))" for k
define K where "K = {k. ∃i∈R. ∃j∈S. k = prod_encode (i,j)}"
define G where "G i = (λj. prod_encode (i,j))  S" for i
define H where "H j = (λi. prod_encode (i,j))  R" for j

{ fix t
{ fix i
from Bun S Bdis have "χ (A i) t = (∑j∈S. χ (A i ∩ B j) t)"
by (rule char_split)
hence "x i * χ (A i) t = (∑j∈S. x i * χ (A i ∩ B j) t)"
by (simp add: sum_distrib_left)
also
{ fix j
have "S=S" and
"x i * χ (A i ∩ B j) t = (let k=prod_encode(i,j) in z1 k * χ (C k) t)"
by (auto simp add: C_def z1_def Let_def)
}
hence "… = (∑j∈S. let k=prod_encode (i,j) in z1 k * χ (C k) t)"
by (rule sum.cong)

also from S have "… = (∑k∈(G i). z1 k * χ (C k) t)"
by (simp add: G_def Let_def o_def
sum.reindex[OF subset_inj_on[OF prod_encode_snd_inj]])

finally have eq: "x i * χ (A i) t = (∑k∈ G i. z1 k * χ (C k) t)" .
(*Repeat with measure instead of char*)

from S have G: "finite (G i)"
by (simp add: G_def)

{ fix k assume "k ∈ G i"
then obtain j where kij: "k=prod_encode (i,j)"
by (auto simp only: G_def)
{
fix i2 assume i2: "i2 ≠ i"

{ fix k2 assume "k2 ∈ G i2"
then obtain j2 where kij2: "k2=prod_encode (i2,j2)"
by (auto simp only: G_def)

from i2 have "(i2,j2) ≠ (i,j)" and "(i2,j2) ∈ UNIV"
and "(i,j) ∈ UNIV" by auto
with inj_prod_encode have  "prod_encode (i2,j2) ≠ prod_encode (i,j)"
with kij kij2 have "k2 ≠ k"
by fast
}
hence "k ∉ G i2"
by fast
}
}
hence "⋀j. i ≠ j ⟹ G i ∩ G j = {}"
by fast
note eq G this
}
hence eq: "⋀i. x i * χ (A i) t = (∑k∈G i. z1 k * χ (C k) t)"
and G: "⋀i. finite (G i)"
and Gdis: "⋀i j. i ≠ j ⟹ G i ∩ G j = {}" .

{ fix i
assume "i∈R"
with ms Bun S Bdis Bms Ams have
"measure M (A i) = (∑j∈S. measure M (A i ∩ B j))"
by (simp add: measure_split)
hence "x i * measure M (A i) = (∑j∈S. x i * measure M (A i ∩ B j))"
by (simp add: sum_distrib_left)

also
{ fix j
have "S=S" and "x i * measure M (A i ∩ B j) =
(let k=prod_encode(i,j) in z1 k * measure M (C k))"
by (auto simp add: C_def z1_def Let_def)
}

hence "… = (∑j∈S. let k=prod_encode (i,j) in z1 k * measure M (C k))"
by (rule sum.cong)

also from S have "… = (∑k∈(G i). z1 k * measure M (C k))"
by (simp add: G_def Let_def o_def
sum.reindex[OF subset_inj_on[OF prod_encode_snd_inj]])

finally have
"x i * measure M (A i) = (∑k∈(G i). z1 k * measure M (C k))" .
}
with refl[of R] have
"(∑i∈R. x i * measure M (A i))
= (∑i∈R. (∑k∈(G i). z1 k * measure M (C k)))"
by (rule sum.cong)
with eq f a have "f t = (∑i∈R. (∑k∈G i. z1 k * χ (C k) t))"
and "a = (∑i∈R. (∑k∈(G i). z1 k * measure M (C k)))"
by auto
also have KG: "K = (⋃i∈R. G i)"
by (auto simp add: K_def G_def)
moreover note G Gdis R
ultimately have f: "f t = (∑k∈K. z1 k * χ (C k) t)"
and a: "a = (∑k∈K. z1 k * measure M (C k))"
by (auto simp add: sum.UNION_disjoint)
(*And now (almost) the same for g*)
{ fix j
from Aun R Adis have "χ (B j) t = (∑i∈R. χ (B j ∩ A i) t)"
by (rule char_split)
hence "y j * χ (B j) t = (∑i∈R. y j * χ (A i ∩ B j) t)"
by (simp add: sum_distrib_left Int_commute)
also
{ fix i
have "R=R" and
"y j * χ (A i ∩ B j) t = (let k=prod_encode(i,j) in z2 k * χ (C k) t)"
by (auto simp add: C_def z2_def Let_def)
}
hence "… = (∑i∈R. let k=prod_encode (i,j) in z2 k * χ (C k) t)"
by (rule sum.cong)
also from R have "… = (∑k∈(H j). z2 k * χ (C k) t)"
by (simp add: H_def Let_def o_def
sum.reindex[OF subset_inj_on[OF prod_encode_fst_inj]])
finally have eq: "y j * χ (B j) t = (∑k∈ H j. z2 k * χ (C k) t)" .

from R have H: "finite (H j)"  by (simp add: H_def)

{ fix k assume "k ∈ H j"
then obtain i where kij: "k=prod_encode (i,j)"
by (auto simp only: H_def)
{ fix j2 assume j2: "j2 ≠ j"
{ fix k2 assume "k2 ∈ H j2"
then obtain i2 where kij2: "k2=prod_encode (i2,j2)"
by (auto simp only: H_def)

from j2 have "(i2,j2) ≠ (i,j)" and "(i2,j2) ∈ UNIV" and "(i,j) ∈ UNIV"
by auto
with inj_prod_encode have  "prod_encode (i2,j2) ≠ prod_encode (i,j)"
with kij kij2 have "k2 ≠ k"
by fast
}
hence "k ∉ H j2"
by fast
}
}
hence "⋀i. i ≠ j ⟹  H i ∩ H j = {}"
by fast
note eq H this
}
hence eq: "⋀j.  y j * χ (B j) t = (∑k∈H j. z2 k * χ (C k) t)"
and H: "⋀i. finite (H i)"
and Hdis: "⋀i j. i ≠ j ⟹ H i ∩ H j = {}" .
from eq g have "g t = (∑j∈S. (∑k∈H j. z2 k * χ (C k) t))"
by simp
also
{ fix j assume jS: "j∈S"
from ms Aun R Adis Ams Bms jS have "measure M (B j) =
(∑i∈R. measure M (B j ∩ A i))"
by (simp add: measure_split)
hence "y j * measure M (B j) = (∑i∈R. y j * measure M (A i ∩ B j))"
by (simp add: sum_distrib_left Int_commute)
also
{ fix i
have "R=R" and "y j * measure M (A i ∩ B j) =
(let k=prod_encode(i,j) in z2 k * measure M (C k))"
by (auto simp add: C_def z2_def Let_def)
}
hence "… = (∑i∈R. let k=prod_encode(i,j) in z2 k * measure M (C k))"
by (rule sum.cong)
also from R have "… = (∑k∈(H j). z2 k * measure M (C k))"
by (simp add: H_def Let_def o_def
sum.reindex[OF subset_inj_on[OF prod_encode_fst_inj]])
finally have eq2:
"y j * measure M (B j) = (∑k∈(H j). z2 k * measure M (C k))" .
}
with refl have "(∑j∈S. y j * measure M (B j)) = (∑j∈S. (∑k∈(H j). z2 k * measure M (C k)))"
by (rule sum.cong)
with b have "b = (∑j∈S. (∑k∈(H j). z2 k * measure M (C k)))"
by simp
moreover have "K = (⋃j∈S. H j)"
by (auto simp add: K_def H_def)
moreover note H Hdis S
ultimately have g: "g t = (∑k∈K. z2 k * χ (C k) t)" and K: "finite K"
and b: "b = (∑k∈K. z2 k * measure M (C k))"
by (auto simp add: sum.UNION_disjoint)

{ fix i
from Bun have "(⋃k∈G i. C k) = A i"
by (simp add: G_def C_def)
}
with Aun have "(⋃i∈R. (⋃k∈G i. C k)) = UNIV"
by simp
hence "(⋃k∈(⋃i∈R. G i). C k) = UNIV"
by simp
with KG have Kun: "(⋃k∈K. C k) = UNIV"
by simp

note f g a b Kun K
}  txt‹\nopagebreak›
hence f: "f = (λt. (∑k∈K. z1 k * χ (C k) t))"
and g: "g = (λt. (∑k∈K. z2 k * χ (C k) t))"
and a: "a = (∑k∈K. z1 k * measure M (C k))"
and b: "b = (∑k∈K. z2 k * measure M (C k))"
and Kun: "⋃(C  K) = UNIV" and K: "finite K"
by (auto simp add: ext)

note f g a b K
moreover
{ fix k1 k2 assume "k1∈K" and "k2∈K" and diff: "k1 ≠ k2"
with K_def obtain i1 j1 i2 j2 where
RS: "i1 ∈ R ∧ i2 ∈ R ∧ j1 ∈ S ∧ j2 ∈ S"
and k1: "k1 = prod_encode (i1,j1)" and k2: "k2 = prod_encode (i2,j2)"
by auto

with diff have "(i1,j1) ≠ (i2,j2)"
by auto

with RS Adis Bdis k1 k2 have "C k1 ∩ C k2 = {}"
by (simp add: C_def) fast
}
moreover
{ fix k assume "k ∈ K"
with K_def obtain i j where R: "i ∈ R" and S: "j ∈ S"
and k: "k = prod_encode (i,j)"
by auto
with Ams Bms have "A i ∈ measurable_sets M" and "B j ∈ measurable_sets M"
by auto
with ms have "A i ∩ B j ∈ measurable_sets M"
by (simp add: measure_space_def sigma_algebra_inter)
with k have "C k ∈ measurable_sets M"
by (simp add: C_def)
}
moreover note Kun

moreover from x have "nonnegative z1"
by (simp add: z1_def nonnegative_def)
moreover from y have "nonnegative z2"
by (simp add: z2_def nonnegative_def)
ultimately show ?thesis by blast
qed
qed

text‹Additivity and monotonicity are now almost obvious, the latter
trivially implying uniqueness.›

lemma assumes ms: "measure_space M" and a: "a ∈ sfis f M" and b: "b ∈ sfis g M"
shows sfis_add: "a+b ∈ sfis (λw. f w + g w) M"
proof -
from assms have
"∃ z1 z2 C K. f = (λt. ∑i∈(K::nat set). z1 i * χ (C i) t) ∧
g = (λt. ∑i∈K. z2 i * χ (C i) t) ∧ a = (∑i∈K. z1 i * measure M (C i))
∧ b = (∑i∈K. z2 i * measure M (C i))
∧ finite K ∧ (∀i∈K. ∀j∈K. i ≠ j ⟶ C i ∩ C j = {})
∧ (∀i ∈ K. C i ∈ measurable_sets M) ∧ (⋃i∈K. C i) = UNIV
∧ nonnegative z1 ∧ nonnegative z2"
by (rule sfis_present)

then obtain z1 z2 C K where f: "f = (λt. ∑i∈(K::nat set). z1 i * χ (C i) t)"
and g: "g = (λt. ∑i∈K. z2 i * χ (C i) t)"
and a2: "a = (∑i∈K. z1 i * measure M (C i))"
and b2: "b = (∑i∈K. z2 i * measure M (C i))"
and CK: "finite K ∧ (∀i∈K. ∀j∈K. i ≠ j ⟶ C i ∩ C j = {}) ∧
(∀i∈K. C i ∈ measurable_sets M) ∧ ⋃(C  K) = UNIV"
and z1: "nonnegative z1" and z2: "nonnegative z2"
by auto

{ fix t
from f g have
"f t + g t = (∑i∈K. z1 i * χ (C i) t) + (∑i∈K. z2 i * χ (C i) t)"
by simp
also have "… = (∑i∈K. z1 i * χ (C i) t + z2 i * χ (C i) t)"
by (rule sum.distrib[THEN sym])
also have "… = (∑i∈K. (z1 i + z2 i) * χ (C i) t)"
by (simp add: distrib_right)
finally have "f t + g t = (∑i∈K. (z1 i + z2 i) * χ (C i) t)" .
}

also
{ fix t
from z1 have "0 ≤ z1 t"
by (simp add: nonnegative_def)
also from z2 have "0 ≤ z2 t"
by (simp add: nonnegative_def)
ultimately have "0 ≤ z1 t + z2 t"
}

hence "nonnegative (λw. z1 w + z2 w)"
by (simp add: nonnegative_def ext)
moreover note CK
ultimately have
"(∑i∈K. (z1 i + z2 i) * measure M (C i)) ∈ sfis (λw. f w + g w) M"
by (auto simp add: sfis.base)
also
from a2 b2 have "a+b = (∑i∈K. (z1 i + z2 i) * measure M (C i))"
by (simp add: sum.distrib[THEN sym] distrib_right)
ultimately show ?thesis by simp
qed

lemma assumes ms: "measure_space M" and a: "a ∈ sfis f M"
and b: "b ∈ sfis g M" and fg: "f≤g"
shows sfis_mono: "a ≤ b"
proof - txt‹\nopagebreak›
from ms a b have
"∃ z1 z2 C K. f = (λt. ∑i∈(K::nat set). z1 i * χ (C i) t) ∧
g = (λt. ∑i∈K. z2 i * χ (C i) t) ∧ a = (∑i∈K. z1 i * measure M (C i))
∧ b = (∑i∈K. z2 i * measure M (C i))
∧ finite K ∧ (∀i∈K. ∀j∈K. i ≠ j ⟶ C i ∩ C j = {})
∧ (∀i ∈ K. C i ∈ measurable_sets M) ∧ (⋃i∈K. C i) = UNIV
∧ nonnegative z1 ∧ nonnegative z2"
by (rule sfis_present)

then obtain z1 z2 C K where f: "f = (λt. ∑i∈(K::nat set). z1 i * χ (C i) t)"
and g: "g = (λt. ∑i∈K. z2 i * χ (C i) t)"
and a2: "a = (∑i∈K. z1 i * measure M (C i))"
and b2: "b = (∑i∈K. z2 i * measure M (C i))"
and K: "finite K" and dis: "(∀i∈K. ∀j∈K. i ≠ j ⟶ C i ∩ C j = {})"
and Cms: "(∀i∈K. C i ∈ measurable_sets M)" and Cun: "⋃(C  K) = UNIV"
by auto

{ fix i assume iK: "i ∈ K"
{ assume "C i ≠ {}"
then obtain t where ti: "t ∈ C i"
by auto
hence "z1 i = z1 i * χ (C i) t"
by (simp add: characteristic_function_def)
also
from dis iK ti have "K-{i} = K-{i}"
and "⋀x. x ∈ K-{i} ⟹ z1 x * χ (C x) t = 0"
by (auto simp add: characteristic_function_def)
hence "0 = (∑k∈K-{i}. z1 k * χ (C k) t)"
by (simp only: sum.neutral_const sum.cong)
with K iK have "z1 i * χ (C i) t = (∑k∈K. z1 k * χ (C k) t)"
by (simp add: sum_diff1)
also
from fg f g have "(∑i∈K. z1 i * χ (C i) t) ≤ (∑i∈K. z2 i * χ (C i) t)"
by (simp add: le_fun_def)
also
from dis iK ti have "K-{i} = K-{i}"
and "⋀x. x ∈ K-{i} ⟹ z2 x * χ (C x) t = 0"
by (auto simp add: characteristic_function_def)
hence "0 = (∑k∈K-{i}. z2 k * χ (C k) t)"
by (simp only: sum.neutral_const sum.cong)
with K iK have "(∑k∈K. z2 k * χ (C k) t) = z2 i * χ (C i) t"
by (simp add: sum_diff1)
also
from ti have "… = z2 i"
by (simp add: characteristic_function_def)
finally
have "z1 i ≤ z2 i" .
}
hence h: "C i ≠ {} ⟹ z1 i ≤ z2 i" .

have "z1 i * measure M (C i) ≤ z2 i * measure M (C i)"
proof (cases "C i ≠ {}")
case False
with ms show ?thesis
by (auto simp add: measure_space_def positive_def)

next
case True
with h have "z1 i ≤ z2 i"
by fast
also from iK ms Cms have "0 ≤ measure M (C i)"
by (auto simp add: measure_space_def positive_def )
ultimately show ?thesis
by (simp add: mult_right_mono)
qed
}
with a2 b2 show ?thesis by (simp add: sum_mono)
qed

lemma sfis_unique:
assumes ms: "measure_space M" and a: "a ∈ sfis f M" and b: "b ∈ sfis f M"
shows "a=b"
proof -
have "f≤f" by (simp add: le_fun_def)
with assms have "a≤b" and "b≤a"
by (auto simp add: sfis_mono)
thus ?thesis by simp
qed

text ‹The integral of characteristic functions, as well as the effect of
multiplication with a constant, follows directly from the
definition. Together with a generalization of the addition theorem
to sums, a less restrictive introduction rule emerges, making
normal forms obsolete. It is only valid in measure spaces though.›

lemma sfis_char:
assumes ms: "measure_space M" and mA: "A ∈ measurable_sets M"
shows "measure M A ∈ sfis χ A M"
(*<*)proof -
define R :: "nat ⇒ 'a set" where "R i = (if i = 0 then A else if i=1 then -A else {})" for i
define x :: "nat ⇒ real" where "x i = (if i = 0 then 1 else 0)" for i
define K :: "nat set" where "K = {0,1}"

from ms mA have Rms: "∀i∈K. R i ∈ measurable_sets M"
by (simp add: K_def R_def measure_space_def sigma_algebra_def)
have nn: "nonnegative x" by (simp add: nonnegative_def x_def)
have un: "(⋃i∈K. R i) = UNIV" by (simp add: R_def K_def)
have fin: "finite K" by (simp add: K_def)
have dis: "∀j1∈K. ∀j2∈K. j1 ≠ j2 ⟶ (R j1) ∩ (R j2) = {}" by (auto simp add: R_def K_def)
{ fix t
from un fin dis have "χ A t = (∑i∈K. χ (A ∩ R i) t)" by (rule char_split)
also
{ fix i
have "K=K" and "χ (A ∩ R i) t = x i * χ (R i) t"
by (auto simp add: R_def x_def characteristic_function_def)}
hence "… = (∑i∈K. x i * χ (R i) t)" by (rule sum.cong)
finally have "χ A t = (∑i∈K. x i * χ (R i) t)" .
}
hence "χ A = (λt. ∑i∈K. x i * χ (R i) t)" by (simp add: ext)

from this Rms nn fin dis un have "(∑i∈K. x i * measure M (R i)) ∈ sfis χ A M"
by (rule sfis.base)
also
{ fix i
from ms have "K=K" and "x i * measure M (R i) = measure M (A ∩ R i)"
by (auto simp add: R_def x_def measure_space_def positive_def)
} hence "(∑i∈K. x i * measure M (R i)) = (∑i∈K. measure M (A ∩ R i))"
by (rule sum.cong)
also from ms un fin dis Rms mA have "… = measure M A"
by (rule measure_split[THEN sym])

finally show ?thesis .
qed(*>*)
(*Sums are always problematic, since they use informal notation
all the time.*)

lemma sfis_times:
assumes a: "a ∈ sfis f M" and z: "0≤z"
shows "z*a ∈ sfis (λw. z*f w) M" (*<*)using a
proof cases
case (base x A S)
{
fix t
from base have "z*f t = (∑i∈S. z * (x i * χ (A i) t))"
by (simp add: sum_distrib_left)
also have "… = (∑i∈S. (z * x i) * χ (A i) t)"
proof (rule sum.cong)
show "S = S" ..
fix i show "z * (x i * χ (A i) t) = (z * x i) * χ (A i) t" by auto
qed
finally have "z * f t = (∑i∈S. z * x i * χ (A i) t)" .
}
hence zf: "(λw. z*f w) = (λt. ∑i∈S. z * x i * χ (A i) t)" by (simp add: ext)

from z base have "nonnegative (λw. z*x w)" by (simp add: nonnegative_def zero_le_mult_iff)
with base zf have "(∑i∈S. z * x i * measure M (A i)) ∈ sfis (λw. z*f w) M"
by (simp add: sfis.base)
also have "(∑i∈S. z * x i * measure M (A i)) = (∑i∈S. z * (x i * measure M (A i)))"
proof (rule sum.cong)
show "S = S" ..
fix i show "(z * x i) * measure M (A i) = z * (x i * measure M (A i))" by auto
qed
also from base have "… = z*a" by (simp add: sum_distrib_left)
finally show ?thesis .
qed(*>*)

lemma assumes ms: "measure_space M"
and a: "∀i∈S. a i ∈ sfis (f i) M" and S: "finite S"
shows sfis_sum: "(∑i∈S. a i) ∈ sfis (λt. ∑i∈S. f i t) M" (*<*)using S a
proof induct
case empty
with ms have "measure M {} ∈ sfis χ {} M"
by (simp add: measure_space_def sigma_algebra_def sfis_char)
with ms show ?case
by (simp add: sum.empty measure_space_def positive_def char_empty)
next
case (insert s S)
then have "⋀t. (∑i ∈ insert s S. f i t) = f s t + (∑i∈S. f i t)" by simp
moreover from insert have "(∑i ∈ insert s S. a i) = a s + (∑i∈S. a i)" by simp
moreover from insert have "a s ∈ sfis (f s) M" by fast
moreover from insert have "(∑i∈S. a i) ∈ sfis (λt. ∑i∈S. f i t) M" by fast
moreover note ms ultimately show ?case by (simp add: sfis_add ext)
qed(*>*)

(*The introduction rule without normal forms, only in measure_spaces*)
lemma sfis_intro:
assumes ms: "measure_space M" and Ams: "∀i ∈ S. A i ∈ measurable_sets M"
and nn: "nonnegative x" and S: "finite S"
shows "(∑i∈S. x i * measure M (A i)) ∈
sfis (λt. ∑i∈(S::nat set). x i * χ (A i) t) M"
proof -
{ fix i assume iS: "i ∈ S"
with ms Ams have "measure M (A i) ∈ sfis χ (A i) M"
by (simp add: sfis_char)
with nn have "x i * measure M (A i) ∈ sfis (λt. x i * χ (A i) t) M"
by (simp add: nonnegative_def sfis_times)
}
with ms S show ?thesis
by (simp add: sfis_sum)
qed

text‹That is nearly all there is to know about simple function
integral sets. It will be useful anyway to have the next two facts
available.›

lemma sfis_nn:
assumes f: "a ∈ sfis f M"
shows "nonnegative f" (*<*)using f
proof (cases)
case (base x A S)
{
fix t
from base have "⋀i. 0 ≤ x i * χ (A i) t"
by (simp add: nonnegative_def characteristic_function_def)
with base have "(∑i∈S. 0) ≤ f t"
by (simp del: sum.neutral_const sum_constant add: sum_mono)
hence "0 ≤ f t" by simp
}
thus ?thesis by (simp add: nonnegative_def)
qed(*>*)

lemma sum_rv:
assumes rvs: "∀k∈K. (f k) ∈ rv M" and ms: "measure_space M"
shows "(λt. ∑k∈K. f k t) ∈ rv M"
(*<*)proof (cases "finite K")
case False
hence "(λt. ∑k∈K. f k t) = (λt. 0)"
by simp
with ms show ?thesis
by (simp add: const_rv)
next
case True
from this rvs show ?thesis
proof (induct)
case empty
have "(λt. ∑k∈{}. f k t) = (λt. 0)"
by simp
with ms show ?case
by (simp add: const_rv)
next
case (insert x F)
hence "(λt. ∑k∈insert x F. f k t) = (λt. f x t + (∑k∈F. f k t))"
by simp
also
from insert have "f x ∈ rv M" and "(λt. (∑k∈F. f k t)) ∈ rv M"
by simp_all
ultimately show ?case
by (simp add: rv_plus_rv)
qed
qed(*>*)

lemma sfis_rv:
assumes ms: "measure_space M" and f: "a ∈ sfis f M"
shows "f ∈ rv M" using f
proof (cases)
case (base x A S)
hence "f = (λt. ∑i∈S. x i * χ (A i) t)"
by simp
also
{ fix i
assume "i ∈ S"
with base have "A i ∈ measurable_sets M"
by simp
with ms have "(λt. x i * χ (A i) t) ∈ rv M"
by (simp add: char_rv const_rv rv_times_rv)
} with ms
have "… ∈ rv M"
by (simp add: sum_rv)
ultimately show ?thesis
by simp
qed(*>*)(*>*)(*nonnegative function integral set*)(*>*)

subsection ‹Nonnegative Functions›

text ‹
\label{nnfis}There is one more important fact about ‹sfis›, easily the
hardest one to see. It is about the relationship with monotone
convergence and paves the way for a sensible definition of ‹nnfis›, the nonnegative function integral sets, enabling
monotonicity and thus uniqueness. A reasonably concise formal proof could
fortunately be achieved in spite of the nontrivial ideas involved
--- compared for instance to the intuitive but hard-to-formalize
‹sfis_present›. A small lemma is needed to ensure that the
inequation, which depends on an arbitrary $z$ strictly between
$0$ and $1$, carries over to $z=1$, thereby eliminating $z$ in the end.›

lemma real_le_mult_sustain:
assumes zr: "⋀z. ⟦0<z; z<1⟧ ⟹ z * r ≤ y"
shows "r ≤ (y::real)"(*<*)
proof (cases "0<y")
case False

have "0<(1::real)"
by simp
hence "∃z::real. 0<z ∧ z<1"
by (rule dense)
then obtain z::real where 0: "0<z" and 1: "z<1"
by fast
with zr have a: "z*r ≤ y"
by simp

also
from False have "y≤0"
by simp
with a have "z*r ≤ 0"
by simp
with 0 1 have z1: "z≤1" and r0: "r≤0"
by (simp_all add: mult_le_0_iff)
hence "1*r ≤ z*r"
by (rule mult_right_mono_neg)

ultimately show "r≤y"
by simp

next
case True
{
assume yr: "y < r"
then have "∃q. y<q ∧ q<r"
by (rule dense)
then obtain q where yq: "y<q" and q: "q<r"
by fast

from yr True have r0: "0<r"
by simp
with q have "q/r < 1"
by (simp add: pos_divide_less_eq)

also from True yq r0 have "0<q/r"
by (simp add: zero_less_divide_iff)

ultimately have "(q/r)*r≤y" using zr
by force

with r0 have "q≤y"
by simp
with yq have False
by simp
}
thus ?thesis
by force
qed(*>*)

lemma sfis_mon_conv_mono:
assumes uf: "u↑f" and xu: "⋀n. x n ∈ sfis (u n) M" and xy: "x↑y"
and sr: "r ∈ sfis s M" and sf: "s ≤ f" and ms: "measure_space M"
shows "r ≤ y" (*This is Satz 11.1 in Bauer*) using sr
proof cases
case (base a A S)
note base_a = this

{ fix z assume znn: "0<(z::real)" and z1: "z<1"
define B where "B n = {w. z*s w ≤ u n w}" for n

{ fix n
note ms also
from xu have xu: "x n ∈ sfis (u n) M" .
hence nnu: "nonnegative (u n)"
by (rule sfis_nn)
from ms xu have "u n ∈ rv M"
by (rule sfis_rv)
moreover from ms sr have "s ∈ rv M"
by (rule sfis_rv)
with ms have "(λw. z*s w) ∈ rv M"
by (simp add: const_rv rv_times_rv)
ultimately have "B n ∈ measurable_sets M"
by (simp add: B_def rv_le_rv_measurable)
with ms base have ABms: "∀i∈S. (A i ∩ B n) ∈ measurable_sets M"
by (auto simp add: measure_space_def sigma_algebra_inter)

from xu have "z*(∑i∈S. a i * measure M (A i ∩ B n)) ≤ x n"
proof (cases)
case (base c C R)
{ fix t
{ fix i
have "S=S" and "a i * χ (A i ∩ B n) t = χ (B n) t * (a i * χ (A i) t)"
by (auto simp add: characteristic_function_def) }
hence "(∑i∈S. a i * χ (A i ∩ B n) t) =
(∑i∈S. χ (B n) t * (a i * χ (A i) t))"
by (rule sum.cong)
hence "z*(∑i∈S. a i * χ (A i ∩ B n) t) =
z*(∑i∈S. χ (B n) t * (a i * χ (A i) t))"
by simp
also have "… = z * χ (B n) t * (∑i∈S. a i * χ (A i) t)"
by (simp add: sum_distrib_left[THEN sym])
also
from sr have "nonnegative s" by (simp add: sfis_nn)
with nnu B_def base_a
have "z * χ (B n) t * (∑i∈S. a i * χ (A i) t) ≤ u n t"
by (auto simp add: characteristic_function_def nonnegative_def)
finally have "z*(∑i∈S. a i * χ (A i ∩ B n) t) ≤ u n t" .
}

also
from ms base_a znn ABms have
"z*(∑i∈S. a i * measure M (A i ∩ B n)) ∈
sfis (λt. z*(∑i∈S. a i * χ (A i ∩ B n) t)) M"
by (simp add: sfis_intro sfis_times)
moreover note xu ms
ultimately show ?thesis
by (simp add: sfis_mono le_fun_def)
qed
note this ABms
}
hence 1: "⋀n. z * (∑i∈S. a i * measure M (A i ∩ B n)) ≤ x n"
and ABms: "⋀n. ∀i∈S. A i ∩ B n ∈ measurable_sets M" .

have Bun: "(λn. B n)↑UNIV"
proof (unfold mon_conv_set_def, rule)
{ fix n
from uf have um: "u n ≤ u (Suc n)"
by (simp add: mon_conv_real_fun_def)
{
fix w
assume "z*s w ≤ u n w"
also from um have "u n w ≤ u (Suc n) w"
by (simp add: le_fun_def)
finally have "z*s w ≤ u (Suc n) w" .
}
hence "B n ≤ B (Suc n)"
by (auto simp add: B_def)
}
thus " ∀n. B n ⊆ B (Suc n)"
by fast

{ fix t
have "∃n. z*s t ≤ u n t"
proof (cases "s t = 0")
case True
fix n
from True have "z*s t = 0"
by simp
also from xu have "nonnegative (u n)"
by (rule sfis_nn)
hence "0 ≤ u n t"
by (simp add: nonnegative_def)
finally show ?thesis
by rule

next
case False
from sr have "nonnegative s"
by(rule sfis_nn)
hence "0 ≤ s t"
by (simp add: nonnegative_def)
with False have "0 < s t"
by arith
with z1 have "z*s t < 1*s t"
by (simp only: mult_strict_right_mono)
also from sf have "… ≤ f t"
by (simp add: le_fun_def)
finally have "z * s t < f t" .
(*Next we have to prove that u grows beyond z*s t*)
also from uf have "(λm. u m t)↑f t"
by (simp add: realfun_mon_conv_iff)
ultimately have "∃n.∀m. n≤m ⟶ z*s t < u m t"
by (simp add: real_mon_conv_outgrow)
hence "∃n. z*s t < u n t"
by fast
thus ?thesis
by (auto simp add: order_less_le)
qed

hence "∃n. t ∈ B n"
by (simp add: B_def)
hence "t ∈ (⋃n. B n)"
by fast
}
thus "UNIV=(⋃n. B n)"
by fast
qed

{ fix j assume jS: "j ∈ S"
note ms
also
from jS ABms have "⋀n. A j ∩ B n ∈ measurable_sets M"
by auto
moreover
from Bun have "(λn. A j ∩ B n)↑(A j)"
by (auto simp add: mon_conv_set_def)
ultimately have "(λn. measure M (A j ∩ B n)) ⇢ measure M (A j)"
by (rule measure_mon_conv)

hence "(λn. a j * measure M (A j ∩ B n)) ⇢ a j * measure M (A j)"
by (simp add: tendsto_const tendsto_mult)
}
hence "(λn. ∑j∈S. a j * measure M (A j ∩ B n))
⇢ (∑j∈S. a j * measure M (A j))"
by (rule tendsto_sum)
hence "(λn. z* (∑j∈S. a j * measure M (A j ∩ B n)))
⇢ z*(∑j∈S. a j * measure M (A j))"
by (simp add: tendsto_const tendsto_mult)

with 1 xy base have "z*r ≤ y"
by (auto simp add: LIMSEQ_le mon_conv_real_def)
}
hence zr: "⋀z. 0 < z ⟹ z < 1 ⟹ z * r ≤ y" .
thus ?thesis by (rule real_le_mult_sustain)
qed

text ‹Now we are ready for the second step. The integral of a
monotone limit of functions is the limit of their
integrals. Note that this last limit has to exist in the
first place, since we decided not to use infinite values. Backed
by the last theorem and the preexisting knowledge about limits, the
usual basic properties are
straightforward.›

inductive_set
nnfis:: "('a ⇒ real) ⇒ ('a set set * ('a set ⇒ real)) ⇒ real set"
for f :: "'a ⇒ real" and M :: "'a set set * ('a set ⇒ real)"
where
base: "⟦u↑f; ⋀n. x n ∈ sfis (u n) M; x↑y⟧ ⟹ y ∈ nnfis f M"

lemma sfis_nnfis:
assumes s: "a ∈ sfis f M"
shows "a ∈ nnfis f M"
(*<*)proof -
{ fix t
have "(λn. f t)↑f t" by (simp add: mon_conv_real_def tendsto_const)
} hence "(λn. f)↑f" by (simp add: realfun_mon_conv_iff)
also
from s have "⋀n. a ∈ sfis f M" .
moreover have "(λn. a)↑a" by (simp add: mon_conv_real_def tendsto_const)

ultimately show ?thesis by (rule nnfis.base)
qed(*>*)

lemma nnfis_times:
assumes ms: "measure_space M" and a: "a ∈ nnfis f M" and nn: "0≤z"
shows "z*a ∈ nnfis (λw. z*f w) M" (*<*)using a
proof (cases)
case (base u x)
with nn have "(λm w. z*u m w)↑(λw. z*f w)" by (simp add: realfun_mon_conv_times)
also from nn base have "⋀m. z*x m ∈ sfis (λw. z*u m w) M" by (simp add: sfis_times)
moreover from a nn base have "(λm. z*x m)↑(z*a)" by (simp add: real_mon_conv_times)
ultimately have "z*a ∈ nnfis (λw. z*f w) M" by (rule nnfis.base)

with base show ?thesis by simp
qed(*>*)

assumes ms: "measure_space M" and a: "a ∈ nnfis f M" and b: "b ∈ nnfis g M"
shows "a+b ∈ nnfis (λw. f w + g w) M" (*<*)using a
proof (cases)
case (base u x)
note base_u = this
from b show ?thesis
proof cases
case (base v r)
with base_u have "(λm w. u m w + v m w)↑(λw. f w + g w)"
also
from ms base_u base have "⋀n. x n + r n ∈ sfis (λw. u n w + v n w) M" by (simp add: sfis_add)
moreover from ms base_u base have "(λm. x m + r m)↑(a+b)" by (simp add: real_mon_conv_add)

ultimately have "a+b ∈ nnfis (λw. f w + g w) M" by (rule nnfis.base)
with a b show ?thesis by simp
qed
qed(*>*)

lemma assumes ms: "measure_space M" and a: "a ∈ nnfis f M"
and b: "b ∈ nnfis g M" and fg: "f≤g"
shows nnfis_mono: "a ≤ b" using a
proof (cases)
case (base u x)
note base_u = this
from b show ?thesis
proof (cases)
case (base v r)
{ fix m
from base_u base have "u m ≤ f"
by (simp add: realfun_mon_conv_le)
also note fg finally have "u m ≤ g" .
with ms base_u base have "v↑g" and  "⋀n. r n ∈ sfis (v n) M" and "r↑b"
and "x m ∈ sfis (u m) M" and "u m ≤ g" and "measure_space M"
by simp_all
hence "x m ≤ b"
by (rule sfis_mon_conv_mono)
}
with ms base_u base show "a ≤ b"
by (auto simp add: mon_conv_real_def LIMSEQ_le_const2)
qed
qed

corollary nnfis_unique:
assumes ms: "measure_space M" and a: "a ∈ nnfis f M" and b: "b ∈ nnfis f M"
shows "a=b" (*<*)
proof -
have "f≤f" ..
with assms have "a≤b" and "b≤a"
by (auto simp add: nnfis_mono)
thus ?thesis by simp
qed(*>*)

text‹There is much more to prove about nonnegative integration. Next
up is a classic theorem by Beppo Levi, the monotone convergence
theorem. In essence, it says that the introduction rule for ‹nnfis› holds not only for sequences of simple functions, but for any
sequence of nonnegative integrable functions. It should be mentioned that this theorem cannot be
formulated for the Riemann integral. We prove it by
exhibiting a sequence of simple functions that converges to the same
limit as the original one and then applying the introduction
rule.

The construction and properties of the sequence are slightly intricate. By definition, for any $f_n$ in the original sequence,
there is a sequence $(u_{m n})_{m\in\mathbb{N}}$ of simple functions converging to it.
The $n$th element of the new sequence is the upper closure of the
$n$th elements of the first $n$ sequences.›

definition (*The upper closure?*)
upclose:: "('a ⇒ real) ⇒ ('a ⇒ real) ⇒ ('a ⇒ real)" where
"upclose f g = (λt. max (f t) (g t))"

primrec
mon_upclose_help :: "nat ⇒ (nat ⇒ nat ⇒ 'a ⇒ real) ⇒ nat ⇒ ('a ⇒ real)" ("muh") where
"muh 0 u m = u m 0"
| "muh (Suc n) u m = upclose (u m (Suc n)) (muh n u m)"

definition
mon_upclose (*See Bauer p. 68*) :: "(nat ⇒ nat ⇒ 'a ⇒ real) ⇒ nat ⇒ ('a ⇒ real)" ("mu") where
"mu u m = muh m u m"

lemma sf_norm_help:
assumes fin: "finite K" and jK: "j ∈ K" and tj: "t ∈ C j" and iK: "∀i∈K-{j}. t ∉ C i"
shows "(∑i∈K. (z i) * χ (C i) t) = z j"
(*<*)proof -
from jK have "K = insert j (K-{j})"  by blast
moreover
from fin have finat2: "finite (K-{j})" and "j ∉ (K-{j})"  by simp_all
hence "(∑i∈insert j (K-{j}). (z i) * χ (C i) t) = (z j * χ (C j) t) + (∑i∈K-{j}. (z i) * χ (C i) t)"
by (rule sum.insert)
moreover from tj have "… = z j + (∑i∈K-{j}. (z i) * χ (C i) t)"
by (simp add: characteristic_function_def)
moreover
{ from iK have "∀i∈K-{j}. (z i) * χ (C i) t = 0"
by (auto simp add: characteristic_function_def)
}
hence "… = z j"  by (simp add:sum.neutral)
ultimately show ?thesis by simp
qed(*>*)

lemma upclose_sfis:
assumes ms: "measure_space M" and f: "a ∈ sfis f M" and g: "b ∈ sfis g M"
shows "∃c. c ∈ sfis (upclose f g) M" (*<*)
proof -
from assms have
"∃ z1 z2 C K. f = (λt. ∑i∈(K::nat set). z1 i * χ (C i) t) ∧
g = (λt. ∑i∈K. z2 i * χ (C i) t) ∧ a = (∑i∈K. z1 i * measure M (C i))
∧ b = (∑i∈K. z2 i * measure M (C i))
∧ finite K ∧ (∀i∈K. ∀j∈K. i ≠ j ⟶ C i ∩ C j = {})
∧ (∀i ∈ K. C i ∈ measurable_sets M) ∧ (⋃i∈K. C i) = UNIV
∧ nonnegative z1 ∧ nonnegative z2"
by (rule sfis_present)

then obtain z1 z2 C K where f: "f = (λt. ∑i∈(K::nat set). z1 i * χ (C i) t)"
and g: "g = (λt. ∑i∈K. z2 i * χ (C i) t)"
and a2: "a = (∑i∈K. z1 i * measure M (C i))"
and b2: "b = (∑i∈K. z2 i * measure M (C i))"
and CK: "finite K ∧ (∀i∈K. ∀j∈K. i ≠ j ⟶ C i ∩ C j = {}) ∧
(∀i∈K. C i ∈ measurable_sets M) ∧ ⋃(C  K) = UNIV"
and z1: "nonnegative z1" and z2: "nonnegative z2"
by auto
{ fix t
from CK obtain j where jK: "j ∈ K" and tj: "t ∈ C j"
by force
with CK have iK: "∀i∈K-{j}. t ∉ C i"
by auto
from f and g have "max (f t) (g t) = max (∑i∈K. (z1 i) * χ (C i) t) (∑i∈K. (z2 i) * χ (C i) t)"
by simp
also
from CK jK iK tj have "… = max (z1 j) (z2 j)"
by (simp add: sf_norm_help)
also
from CK jK iK tj have "… = (∑i∈K. (max (z1 i) (z2 i)) * χ (C i) t)"
by (simp add: sf_norm_help)
finally have "max (f t) (g t) = (∑i∈K. max (z1 i) (z2 i) * χ (C i) t)" .
}
hence "upclose f g = (λt. (∑i∈K. max (z1 i) (z2 i) * χ (C i) t))"
by (simp add: upclose_def)
also
{ from z1 z2 have "nonnegative (λi. max (z1 i) (z2 i))"
by (simp add: nonnegative_def max_def)
}
with ms CK have "(∑i∈K. max (z1 i) (z2 i) * measure M (C i)) ∈ sfis … M"
by (simp add: sfis_intro)
ultimately show ?thesis
by auto
qed(*>*)

lemma mu_sfis:
assumes u: "⋀m n. ∃a. a ∈ sfis (u m n) M" and ms: "measure_space M"
shows "∃c. ∀m. c m ∈ sfis (mu u m) M"
(*<*)proof -
{ fix m
from u ms have "⋀n. ∃c. c ∈ sfis (muh m u n) M"
proof (induct m)
case 0
from u show ?case
by force
next
case (Suc m)
{ fix n
from Suc obtain a b where "a ∈ sfis (muh m u n) M" and "b ∈ sfis (u n (Suc m)) M"
by force
with ms u have "∃a. a ∈ sfis (muh (Suc m) u n) M"
by (simp add: upclose_sfis)
}
thus ?case
by force
qed
hence "∃c. c ∈ sfis (mu u m) M"
by (simp add: mon_upclose_def)
} hence "∀m. ∃c. c ∈ sfis (mu u m) M"
by simp
thus ?thesis
by (rule choice)
qed(*>*)

lemma mu_help:
assumes uf: "⋀n. (λm. u m n)↑(f n)" and fh: "f↑h"
shows "(mu u)↑h" and "⋀n. mu u n ≤ f n"
proof -
show mu_le: "⋀n. mu u n ≤ f n"
proof (unfold mon_upclose_def)
fix n
show "⋀m. muh n u m ≤ f n"
proof (induct n)
case (0 m)
from uf have "u m 0 ≤ f 0"
by (rule realfun_mon_conv_le)
thus ?case by simp
next
case (Suc n m)
{ fix t
from Suc have "muh n u m t ≤ f n t"
by (simp add: le_fun_def)
also from fh have "f n t ≤ f (Suc n) t"
by (simp add: realfun_mon_conv_iff mon_conv_real_def)
also from uf have "(λm. u m (Suc n) t)↑(f (Suc n) t)"
by (simp add: realfun_mon_conv_iff)
hence "u m (Suc n) t ≤ f (Suc n) t"
by (rule real_mon_conv_le)
ultimately have "muh (Suc n) u m t ≤ f (Suc n) t"
by (simp add: upclose_def)
}
thus ?case by (simp add: le_fun_def)
qed
qed
(*isotony (?) of mu u is next to prove*)
{ fix t
{ fix m n
have "muh n u m t ≤ muh (Suc n) u m t"
by (simp add: upclose_def)
}
hence pos1: "⋀m n. muh n u m t ≤ muh (Suc n) u m t" .

from uf have uiso: "⋀m n. u m n t ≤ u (Suc m) n t"
by (simp add: realfun_mon_conv_iff mon_conv_real_def)

have iso: "⋀n. mu u n t ≤ mu u (Suc n) t"
proof (unfold mon_upclose_def)
fix n
have "⋀m. muh n u m t ≤ muh n u (Suc m) t"
proof (induct n)
case 0 from uiso show ?case
by (simp add: upclose_def le_max_iff_disj)
next
case (Suc n m)

from Suc have "muh n u m t ≤ muh n u (Suc m) t" .
also from uiso have "u m (Suc n) t ≤ u (Suc m) (Suc n) t" .

ultimately show ?case
by (auto simp add: upclose_def le_max_iff_disj)
qed
note this [of n] also note pos1 [of n "Suc n"]
finally show "muh n u n t ≤ muh (Suc n) u (Suc n) t" .
qed

also

{ fix n
from mu_le [of n]
have "mu u n t ≤ f n t"
by (simp add: le_fun_def)
also
from fh have "(λn. f n t)↑h t"
by (simp add: realfun_mon_conv_iff)
hence "f n t ≤ h t"
by (rule real_mon_conv_le)
finally have "mu u n t ≤ h t" .
}

ultimately have "∃l. (λn. mu u n t)↑l ∧ l ≤ h t"
by (rule real_mon_conv_bound)
then obtain l where
conv: "(λn. mu u n t)↑l" and lh: "l ≤ h t"
by (force simp add: real_mon_conv_bound)

{ fix n::nat
{ fix m assume le: "n ≤ m"
hence "u m n t ≤ mu u m t"
proof (unfold mon_upclose_def)
have "u m n t ≤ muh n u m t"
by (induct n) (auto simp add: upclose_def le_max_iff_disj)
also
from pos1 have "incseq (λn. muh n u m t)"
by (simp add: incseq_Suc_iff)
hence "muh n u m t ≤ muh (n+(m-n)) u m t"
unfolding incseq_def by simp
with le have "muh n u m t ≤ muh m u m t"
by simp
finally show "u m n t ≤ muh m u m t" .
qed
}
hence "∃N. ∀m. N ≤ m ⟶ u m n t ≤ mu u m t"
by blast
also from uf have "(λm. u m n t) ⇢ f n t"
by (simp add: realfun_mon_conv_iff mon_conv_real_def)
moreover
from conv have "(λn. mu u n t) ⇢ l"
by (simp add: mon_conv_real_def)
ultimately have "f n t ≤ l"
by (simp add: LIMSEQ_le)
}
also from fh have "(λn. f n t) ⇢ h t"
by (simp add: realfun_mon_conv_iff mon_conv_real_def)
ultimately have "h t ≤ l"
by (simp add: LIMSEQ_le_const2)

with lh have "l = h t"
by simp
with conv have "(λn. mu u n t)↑(h t)"
by simp
}
with mon_upclose_def show "mu u↑h"
by (simp add: realfun_mon_conv_iff)
qed
(* The Beppo Levi - Theorem *)
theorem nnfis_mon_conv:
assumes fh: "f↑h" and xf: "⋀n. x n ∈ nnfis (f n) M" and xy: "x↑y"
and ms: "measure_space M"
shows "y ∈ nnfis h M"
proof -
define u where "u n = (SOME u. u↑(f n) ∧ (∀m. ∃a. a ∈ sfis (u m) M))" for n
{ fix n
from xf[of n] have "∃u. u↑(f n) ∧ (∀m. ∃a. a ∈ sfis (u m) M)" (is "∃x. ?P x")
proof (cases)
case (base r a)
hence "r↑(f n)" and "⋀m. ∃a. a ∈ sfis (r m) M" by auto
thus ?thesis by fast
qed
hence "?P (SOME x. ?P x)"
by (rule someI_ex)
with u_def have "?P (u n)"
by simp
} also
define urev where "urev m n = u n m" for m n
ultimately have uf: "⋀n. (λm. urev m n)↑(f n)"
and sf: "⋀n m. ∃a. a ∈ sfis (urev m n) M"
by auto

from uf fh have up: "mu urev↑h"
by (rule mu_help) (*Could split the mu_help lemma in two*)
from uf fh have le: "⋀n. mu urev n ≤ f n"
by (rule mu_help)
from sf ms obtain c where sf2: "⋀m. c m ∈ sfis (mu urev m) M"
by (force simp add: mu_sfis)

{ fix m
from sf2 have "c m ∈ nnfis (mu urev m) M"
by (rule sfis_nnfis)
with ms le[of m] xf[of m] have "c m ≤ x m"
by (simp add: nnfis_mono)
} hence "c ≤ x" by (simp add: le_fun_def)
also
{ fix m note ms also
from up have "mu urev m ≤ mu urev (Suc m)"
by (simp add: mon_conv_real_fun_def)
moreover from sf2 have "c m ∈ sfis (mu urev m) M"
and "c (Suc m) ∈ sfis (mu urev (Suc m)) M"
by fast+
ultimately have "c m ≤ c (Suc m)"
by (simp add: sfis_mono)
}
moreover note xy
ultimately have "∃l. c↑l ∧ l ≤ y"
by (simp add: real_mon_conv_dom)
then obtain l where cl: "c↑l" and ly: "l ≤ y"
by fast

from up sf2 cl have int: "l ∈ nnfis h M"
by (rule nnfis.base)

{ fix n
from fh have "f n ≤ h"
by (rule realfun_mon_conv_le)
with ms xf[of n] int have "x n ≤ l"
by (rule nnfis_mono)
} with xy have "y ≤ l"
by (auto simp add: mon_conv_real_def LIMSEQ_le_const2)

with ly have "l=y"
by simp
with int show ?thesis
by simp
qed

text‹Establishing that only nonnegative functions may arise this way
is a triviality.›

lemma nnfis_nn: assumes "a ∈ nnfis f M"
shows "nonnegative f" (*<*)using assms
proof cases
case (base u x)
{fix t
{ fix n
from base have "x n ∈ sfis (u n) M" by fast
hence "nonnegative (u n)" by (rule sfis_nn)
hence "0 ≤ u n t" by (simp add: nonnegative_def)
}
also from base have "(λn. u n t)⇢f t" by (simp add: realfun_mon_conv_iff mon_conv_real_def)
ultimately have "0 ≤ f t" by (simp add: LIMSEQ_le_const)
} thus ?thesis by (simp add: nonnegative_def)
qed(*>*)(*>*)

subsection ‹Integrable Functions›

text‹
Before we take the final step of defining integrability and the
integral operator, we should first clarify what kind of functions we
are able to integrate up to now. It is easy to see that all nonnegative integrable
functions are random variables.›

lemma assumes (*<*)ms:(*>*) "measure_space M" and (*<*)f:(*>*) "a ∈ nnfis f M"
shows nnfis_rv: "f ∈ rv M" (*<*)using f
proof (cases)
case (base u x)
{ fix n
from base have "x n ∈ sfis (u n) M"
by simp
with ms have "u n ∈ rv M"
by (simp add: sfis_rv)
}
also from base
have "u↑f"
by simp
ultimately show ?thesis
by (rule mon_conv_rv)
qed(*>*)

text‹The converse does not hold of course, since there are measurable
functions whose integral is infinite. Regardless, it is possible to
approximate any measurable function using simple
step-functions. This means that all nonnegative random variables are quasi
integrable, as the property is sometimes called, and brings forth the fundamental
insight that a nonnegative function is integrable if and only if it is
measurable and the integrals of the simple functions that
approximate it converge monotonically. Technically, the proof is rather
complex, involving many properties of real numbers.›(*<*)

declare zero_le_power [simp]
(*>*)
lemma assumes (*<*)ms:(*>*) "measure_space M" and (*<*)f(*>*): "f ∈ rv M" and (*<*)nn:(*>*) "nonnegative f"
shows rv_mon_conv_sfis: "∃u x. u↑f ∧ (∀n. x n ∈ sfis (u n) M)"
(*<*)proof (rule+)
(*We don't need the greater case in the book, since our functions are real*)
define A where "A n i = {w. real i/(2::real)^n ≤ f w} ∩ {w. f w < real (Suc i)/(2::real)^n}" for n i
define u where "u n t = (∑i∈{..<(n*2^n)}-{0}. (real i/(2::real)^n)*χ (A n i) t)"  for n t
define x where "x n = (∑i∈{..<(n*2^n)}-{0}. (real i/(2::real)^n)*measure M (A n i))" for n

{ fix n
note ms
also
{ fix i::nat
from ms f have "{w. real i/(2::real)^n ≤ f w} ∈ measurable_sets M"
by (simp_all add: rv_ge_iff)
also from ms f have "{w. f w < real (Suc i)/(2::real)^n} ∈ measurable_sets M"
by (simp add: rv_less_iff)
moreover note  ms
ultimately have "A n i ∈ measurable_sets M"
by (simp add: A_def measure_space_def sigma_algebra_inter)
} hence "∀i∈{..<(n*2^n)}-{0}. A n i ∈ measurable_sets M" by fast
moreover
{ fix i::nat
have "0 ≤ real i"
by simp
also have "0 ≤ (2::real)^n"
by simp
ultimately have "0 ≤ real i/(2::real)^n"
by (simp add: zero_le_divide_iff)
} hence "nonnegative (λi::nat. real i/(2::real)^n)"
by (simp add: nonnegative_def)
(*   This is a little stronger than it has to be, btw.. x i must only be nn for i in S *)

moreover have "finite ({..<(n*2^n)}-{0})"
by simp
ultimately have "x n ∈ sfis (u n) M"
by (simp only: u_def [abs_def] x_def sfis_intro)
} thus "∀n. x n ∈ sfis (u n) M"
by simp

show "u↑f"
proof -
{ fix t

{ fix m i assume tai: "t ∈ A m i" and iS: "i ∈ {..<(m*2^m)}"

have usum: "u m t = (∑j∈{..<(m*2^m)}-{0}. real j / (2::real)^m * χ (A m j) t)"
by (simp add: u_def)

{ fix j assume ne: "i ≠ j"
have "t ∉ A m j"
proof (cases "i < j")
case True
from tai have "f t < real (Suc i) / (2::real)^m"
by (simp add: A_def)
also
from True have "real (Suc i)/(2::real)^m ≤ real j/(2::real)^m"
by (simp add: divide_inverse)
finally
show ?thesis
by (simp add: A_def)

next
case False
with ne have no: "j<i"
by arith
hence "real (Suc j)/(2::real)^m ≤ real i/(2::real)^m"
by (simp add: divide_inverse)
also
from tai have "real i / (2::real)^m ≤ f t"
by (simp add: A_def)

finally show ?thesis
by (simp add: A_def order_less_le)
qed
}
hence "⋀j. i ≠ j ⟹ χ (A m j) t = 0"
by (simp add: characteristic_function_def)
hence "⋀j. j∈{..<(m*2^m)}-{0}-{i} ⟹  real j / (2::real)^m * χ (A m j) t = 0"
by force
with refl have "(∑j∈{..<(m*2^m)}-{0}-{i}. real j / (2::real)^m * χ (A m j) t) =
(∑j∈{..<(m*2^m)}-{0}-{i}. 0)"
by (rule sum.cong)
also have "… = 0"
by (rule sum.neutral_const)
finally have sum0: "(∑j∈{..<(m*2^m)}-{0}-{i}. real j / (2::real)^m * χ (A m j) t) = 0" .

have "u m t = real i / (2::real)^m"
proof (cases "i=0")
case True
hence "i ∉ {..<(m*2^m)}-{0}"
by simp
hence "{..<(m*2^m)}-{0} = {..<(m*2^m)}-{0}-{i}"
by simp
with usum sum0 have "u m t = 0"
by simp
also from True have "… = real i / (2::real)^m * χ (A m i) t"
by simp
finally show ?thesis using tai
by (simp add: characteristic_function_def)
next
case False
with iS have iS: "i ∈ {..<(m*2^m)}-{0}"
by simp
note usum
also
have fin: "finite ({..<(m*2^m)}-{0}-{i})"
by simp
from iS have ins: "{..<(m*2^m)}-{0} = insert i
({..<(m*2^m)}-{0}-{i})"
by auto
have "i ∉ ({..<(m*2^m)}-{0}-{i})"
by simp

with fin have "(∑j∈insert i ({..<(m*2^m)}-{0}-{i}). real j / (2::real)^m * χ (A m j) t)
= real i / (2::real)^m * χ (A m i) t +
(∑j∈{..<(m*2^m)}-{0}-{i}. real j / (2::real)^m * χ (A m j) t)"
by (rule sum.insert)
with ins tai have "(∑j∈{..<(m*2^m)}-{0}. real j / (2::real)^m * χ (A m j) t)
= real i / (2::real)^m +
(∑j∈{..<(m*2^m)}-{0}-{i}. real j / (2::real)^m * χ (A m j) t)"
by (simp add: characteristic_function_def)

also note sum0
finally show ?thesis
by simp
qed
}
hence disj: "⋀m i. ⟦t ∈ A m i; i ∈ {..<m * 2 ^ m}⟧
⟹ u m t = real i / (2::real)^m" .

{ fix n

define a where "a = (f t)*(2::real)^n"
define i where "i = (LEAST i. a < real (i::nat)) - 1"
from nn have "0 ≤ a"
by (simp add: zero_le_mult_iff a_def nonnegative_def)
also
have "∃i. a < real (i::nat)"
by (rule reals_Archimedean2)
then obtain k where "a < real (k::nat)"
by fast
hence less: "a < real (LEAST i. a < real (i::nat))"
by (rule LeastI)

finally
have "0 < (LEAST i. a < real (i::nat))"
by simp
hence min: "(LEAST i. a < real (i::nat)) - 1 < (LEAST i. a < real (i::nat))"
by arith
hence "¬ (a < real ((LEAST i. a < real (i::nat)) - 1))"
by (rule not_less_Least)
hence ia: "real i ≤ a"
by (auto simp add: i_def order_less_le)
from min less have ai: "a < real (Suc i)"
by (simp add: i_def)

from ia have ia2: "real i / (2::real)^n ≤ f t"
by (simp add: a_def pos_divide_le_eq)
also from ai have ai2: "f t < real (Suc i) / (2::real)^n"
by (simp add: a_def pos_less_divide_eq[THEN sym])
ultimately have tA: "t ∈ A n i"
by (simp add: A_def)

{ assume ftn: "f t < real n"

from ia a_def have "real i ≤ f t * (2::real)^n"
by simp
also from ftn have "f t * (2::real)^n < real n * (2::real)^n"
by simp
finally have ni: "i < n * 2 ^ n"
by (simp add: of_nat_less_iff[symmetric, where 'a=real])

with tA have un: "u n t = real i / (2::real)^n"
using disj by simp

with ia2 have lef: "u n t ≤ f t"
by simp

from un have "real (i+1) / (2::real)^n = (real i + real (1::nat))/(2::real)^n"
by (simp only: of_nat_add)
with un ai2 have fless: "f t < u n t + 1/(2::real)^n"

have uSuc: "u n t ≤ u (Suc n) t"
proof (cases "f t < real (2*i+1) / (2*(2::real)^n)")
case True
from ia2 have "real (2*i)/(2::real)^(n+1) ≤ f t"
by simp
with True have tA2: "t ∈ A (n+1) (2*i)"
by (simp add: A_def)

from ni have "2*i < (n+1)*(2^(n+1))"
by simp
with tA2 have "u (n+1) t = real i / (2::real)^n"
using disj by simp
with un show ?thesis
by simp
next
case False
have "(2::real) ≠ 0"
by simp
hence "real (2*(Suc i)) / ((2::real)^(Suc n)) = real (Suc i) / (2::real)^n"
by (metis mult_divide_mult_cancel_left_if power_Suc of_nat_mult of_nat_numeral)
with ai2 have "f t < real (2*(Suc i)) / (2::real)^(n+1)"
by simp
with False have tA2: "t ∈ A (n+1) (2*i+1)"
by (simp add: A_def)

from ni have "2*i+1 < (n+1)*(2^(n+1))"
by simp
with tA2 have "u (Suc n) t = real (2*i+1) / (2 * (2::real)^n)"
using disj by simp
also have "… = (real (2*i) + real (1::nat))/ (2 * (2::real)^n)"
by (simp only: of_nat_add)
also have "… = real i / (2::real)^n + real (1::nat) / (2 * (2::real)^n)"
finally show ?thesis using un
by (simp add: zero_le_divide_iff)
qed
note this lef fless
}
hence uSuc: "f t < real n ⟹ u n t ≤ u (Suc n) t"
and lef:  "f t < real n ⟹ u n t ≤ f t"
and fless:"f t < real n ⟹ f t < u n t + 1 / (2::real)^n"
by auto

have "u n t ≤ u (Suc n) t"
proof (cases "real n ≤ f t")
case True
{ fix i assume "i ∈ {..<(n*2^n)}-{0}"
hence "Suc i ≤ n*2^n" by simp
hence mult: "real (Suc i) ≤ real n * (2::real)^n"
by (simp add: of_nat_le_iff[symmetric, where 'a=real])
have "0 < (2::real)^n"
by simp
with mult have "real (Suc i) / (2::real)^n ≤ real n"
by (simp add: pos_divide_le_eq)
also note True
finally have "¬ f t <  real (Suc i) / (2::real)^n"
by (simp add: order_less_le)
hence "t ∉ A n i"
by (simp add: A_def)
hence "(real i/(2::real)^n)*χ (A n i) t = 0"
by (simp add: characteristic_function_def)
}
with refl have "(∑i∈{..<n * 2 ^ n} - {0}. real i / (2::real)^n * χ (A n i) t)
= (∑i∈{..<n * 2 ^ n} - {0}. 0)"
by (rule sum.cong)
hence "u n t = 0"  by (simp add: u_def)

also
{ fix m
have "0 ≤ u m t"
by (simp add: u_def characteristic_function_def zero_le_divide_iff sum_nonneg)
}
hence "0 ≤ u (Suc n) t" .

finally show ?thesis .

next
case False
with uSuc show ?thesis  by simp
qed
note this lef fless
}
hence uSuc: "⋀n. u n t ≤ u (Suc n) t"
and lef:  "⋀n. f t < real n ⟹ u n t ≤ f t"
and fless:"⋀n. f t < real n ⟹ f t < u n t + 1 / (2::real)^n"
by auto

have "∃n0::nat. f t < real n0"  by (rule reals_Archimedean2)
then obtain n0::nat where "f t < real n0" ..
also have "⋀n. real n0 ≤ real (n+n0)"  by simp
finally
have pro: "⋀n. f t < real (n + n0)" .
hence 2: "⋀n. u (n+n0) t ≤ f t" using lef by simp
from uSuc have 1: "⋀n. u (n+n0) t ≤ u (Suc n + n0) t" by simp
from 1 2 have "∃c. (λn. u (n+n0) t)↑c ∧ c ≤ f t"
by (rule real_mon_conv_bound)
with uSuc obtain c where n0mc: "(λn. u (n+n0) t)↑c" and cle: "c ≤ f t"
by fast

from n0mc have "(λn. u (n+n0) t) ⇢ c"
by (simp add: mon_conv_real_def)
hence lim: "(λn. u n t) ⇢ c"
by (subst limseq_shift_iff[THEN sym])

have "∀y. ∃N. ∀n. N ≤ n ⟶ y < (2::real)^n"
proof
fix y::real
have "∃N::nat. y < real N"
by (rule reals_Archimedean2)
then obtain N::nat where 1: "y < real N"
by fast
{ fix n::nat
note 1
also assume "N ≤ n"
also have "real n < (2::real)^n"
by (rule of_nat_less_two_power)
finally
have "y < 2 ^ n"
by simp
}
thus "∃N. ∀n. N ≤ n ⟶ y < (2::real)^n"
by blast
qed
hence "(λn. inverse ((2::real)^n)) ⇢ 0"
by (intro LIMSEQ_inverse_zero) auto
with lim have "(λn. u n t + inverse ((2::real)^n)) ⇢ c+0"
hence "(λn. u n t + 1/(2::real)^n) ⇢ c"
by (simp add: divide_inverse)
hence "(λn. u (n+n0) t + 1/(2::real)^(n+n0)) ⇢ c"
by (subst limseq_shift_iff)
also from pro fless have "⋀n. f t ≤ u (n+n0) t + 1 / 2 ^ (n+n0)"
by (simp add: order_le_less)
ultimately have "f t ≤ c"
by (simp add: LIMSEQ_le_const)
with cle have "c = f t"
by simp

with lim have "(λn. u n t) ⇢ f t"
by simp

with uSuc have "(λn. u n t)↑ f t"
by (simp add: mon_conv_real_def)
}
thus ?thesis
by (simp add: realfun_mon_conv_iff)
qed
qed(*>*)

text‹The following dominated convergence theorem is an easy
corollary. It can be effectively applied to show integrability.›

corollary assumes ms: "measure_space M" and f: "f ∈ rv M"
and b: "b ∈ nnfis g M" and fg: "f≤g" and nn: "nonnegative f"
shows nnfis_dom_conv: "∃a. a ∈ nnfis f M ∧ a ≤ b" using b
proof (cases)
case (base v r)
from ms f nn have "∃u x. u↑f ∧ (∀n. x n ∈ sfis (u n) M)"
by (rule rv_mon_conv_sfis)
then obtain u x where uf: "u↑f" and xu: "⋀n. x n ∈ sfis (u n) M"
by fast

{ fix n
from uf have "u n ≤ f"
by (rule realfun_mon_conv_le)
also note fg
also
from xu have "x n ∈ nnfis (u n) M"
by (rule sfis_nnfis)
moreover note b ms
ultimately  have le: "x n ≤ b"
by (simp add: nnfis_mono)

from uf have "u n ≤ u (Suc n)"
by (simp only: mon_conv_real_fun_def)
with ms xu[of n] xu[of "Suc n"] have "x n ≤ x (Suc n)"
by (simp add: sfis_mono)
note this le
}
hence "∃a. x↑a ∧ a ≤ b"
by (rule real_mon_conv_bound)
then obtain a where xa: "x↑a" and ab: "a ≤ b"
by auto

from uf xu xa have "a ∈ nnfis f M"
by (rule nnfis.base)
with ab show ?thesis
by fast
qed

text‹Speaking all the time about integrability, it is time to define
it at last.›

definition
integrable:: "('a ⇒ real) ⇒ ('a set set * ('a set ⇒ real)) ⇒ bool" where
(*We could also demand that f be in rv M, but measurability is already ensured
by construction of the integral/nn_integrable functions*)
"integrable f M ⟷ measure_space M ∧
(∃x. x ∈ nnfis (pp f) M) ∧ (∃y. y ∈ nnfis (np f) M)"

definition
integral:: "('a ⇒ real) ⇒ ('a set set * ('a set ⇒ real)) ⇒ real" ("∫ _ ∂_"(*<*)[60,61] 110(*>*)) where
"integrable f M ⟹ ∫ f ∂M = (THE i. i ∈ nnfis (pp f) M) -
(THE j. j ∈ nnfis (np f) M)"

text‹So the final step is done, the integral defined. The theorems
we are already used to prove from the
earlier stages are still missing. Only now there are always two properties to be
shown: integrability and the value of the integral. Isabelle makes
it possible two have both goals in a single theorem, so that the
user may derive the statement he desires. Two useful lemmata follow. They
help lifting nonnegative function integral sets to integrals
proper. Notice how the dominated convergence theorem from above is
employed in the latter.›

lemma nnfis_integral:
assumes nn: "a ∈ nnfis f M" and ms: "measure_space M"
shows "integrable f M" and "∫ f ∂ M = a"
proof -
from nn have "nonnegative f"
by (rule nnfis_nn)
hence "pp f = f" and 0: "np f = (λt. 0)"
by (auto simp add: nn_pp_np)
with nn have a: "a ∈ nnfis (pp f) M"
by simp
have "0≤(0::real)"
by (rule order_refl)
with ms nn have "0*a ∈ nnfis (λt. 0*f t) M"
by (rule nnfis_times)
with 0 have 02: "0 ∈ nnfis (np f) M"
by simp
with ms a show "integrable f M"
by (auto simp add: integrable_def)
also
from a ms have "(THE i. i ∈ nnfis (pp f) M) = a"
by (auto simp add: nnfis_unique)
moreover
from 02 ms have "(THE i. i ∈ nnfis (np f) M) = 0"
by (auto simp add: nnfis_unique)
ultimately show "∫ f ∂ M = a"
by (simp add: integral_def)
qed

lemma nnfis_minus_nnfis_integral:
assumes a: "a ∈ nnfis f M" and b: "b ∈ nnfis g M"
and ms: "measure_space M"
shows "integrable (λt. f t - g t) M" and "∫ (λt. f t - g t) ∂ M = a - b"
proof -
from ms a b have "(λt. f t - g t) ∈ rv M"
by (auto simp only: nnfis_rv rv_minus_rv)
hence prv: "pp (λt. f t - g t) ∈ rv M" and nrv: " np (λt. f t - g t) ∈ rv M"
by (auto simp only: pp_np_rv)

have nnp: "nonnegative (pp (λt. f t - g t))"
and nnn: "nonnegative (np (λt. f t - g t))"
by (simp_all add: nonnegative_def positive_part_def negative_part_def)

from ms a b have fg: "a+b ∈ nnfis (λt. f t + g t) M"

from a b have nnf: "nonnegative f" and nng: "nonnegative g"
by (simp_all only: nnfis_nn)

{ fix t
from nnf nng have "0 ≤ f t" and "0 ≤ g t"
by (simp_all add: nonnegative_def)
hence "(pp (λt. f t - g t)) t ≤ f t + g t" and "(np (λt. f t - g t)) t ≤ f t + g t"
by (simp_all add: positive_part_def negative_part_def)
}
hence "(pp (λt. f t - g t)) ≤ (λt. f t + g t)"
and "(np (λt. f t - g t)) ≤ (λt. f t + g t)"
by (simp_all add: le_fun_def)
with fg nnf nng prv nrv nnp nnn ms
have "∃l. l ∈ nnfis (pp (λt. f t - g t)) M ∧ l ≤ a+b"
and "∃k. k ∈ nnfis (np (λt. f t - g t)) M ∧ k ≤ a+b"
by (auto simp only: nnfis_dom_conv)
then obtain l k where l: "l ∈ nnfis (pp (λt. f t - g t)) M"
and k: "k ∈ nnfis (np (λt. f t - g t)) M"
by auto
with ms show i: "integrable (λt. f t - g t) M"
by (auto simp add: integrable_def)

{ fix t
have "f t - g t = (pp (λt. f t - g t)) t - (np (λt. f t - g t)) t"
by (rule f_plus_minus)

hence "f t + (np (λt. f t - g t)) t = g t + (pp (λt. f t - g t)) t"
by arith
}
hence "(λt. f t + (np (λt. f t - g t)) t) =
(λt. g t + (pp (λt. f t - g t)) t)"
by (rule ext)
also
from ms a k b l have "a+k ∈ nnfis (λt. f t + (np (λt. f t - g t)) t) M"
and "b+l ∈ nnfis (λt. g t + (pp (λt. f t - g t)) t) M"
moreover note ms
ultimately have "a+k = b+l"
by (simp add: nnfis_unique)
hence "l-k=a-b" by arith
also
from k l ms have "(THE i. i ∈ nnfis (pp (λt. f t - g t)) M) = l"
and "(THE i. i ∈ nnfis (np (λt. f t - g t)) M) = k"
by (auto simp add: nnfis_unique)
moreover note i
ultimately show "∫ (λt. f t - g t) ∂ M = a - b"
by (simp add: integral_def)
qed

text‹Armed with these, the standard integral behavior should not be
hard to derive. Mind that integrability always implies a
measure space, just like random variables did in \ref{sec:realrandvar}.›

theorem assumes (*<*)int:(*>*) "integrable f M"
shows integrable_rv: "f ∈ rv M"
(*<*)proof -
from int have "pp f ∈ rv M ∧ np f ∈ rv M"
by (auto simp add: integrable_def nnfis_rv)
thus ?thesis
by (simp add: pp_np_rv_iff[THEN sym])
qed(*>*)

theorem integral_char:
assumes ms: "measure_space M" and mA: "A ∈ measurable_sets M"
shows "∫ χ A ∂ M = measure M A" and "integrable χ A M"
(*<*)proof -
from ms mA have "measure M A ∈ sfis χ A M"
by (rule sfis_char)
hence nnfis: "measure M A ∈ nnfis χ A M"
by (rule sfis_nnfis)
from this and ms show "∫ χ A ∂ M = measure M A"
by (rule nnfis_integral)
from nnfis and ms show "integrable χ A M"
by (rule nnfis_integral)
qed(*>*)

assumes f: "integrable f M" and g: "integrable g M"
shows "integrable (λt. f t + g t) M"
and "∫ (λt. f t + g t) ∂M = ∫ f ∂M + ∫ g ∂M"
proof -
define u where "u = (λt. pp f t + pp g t)"
define v where "v = (λt. np f t + np g t)"

from f obtain pf nf where pf: "pf ∈ nnfis (pp f) M"
and nf: "nf ∈ nnfis (np f) M" and ms: "measure_space M"
by (auto simp add: integrable_def)
from g obtain pg ng where pg: "pg ∈ nnfis (pp g) M"
and ng: "ng ∈ nnfis (np g) M"
by (auto simp add: integrable_def)

from ms pf pg u_def have
u: "pf+pg ∈ nnfis u M"

from ms nf ng v_def have
v: "nf+ng ∈ nnfis v M"

{ fix  t
from u_def v_def have "f t + g t = u t - v t"
by (simp add: positive_part_def negative_part_def)
}
hence uvf: "(λt. u t - v t) = (λt. f t + g t)"
by (simp add: ext)

from u v ms have "integrable (λt. u t - v t) M"
by (rule nnfis_minus_nnfis_integral)
with u_def v_def uvf  show "integrable (λt. f t + g t) M"
by simp

from pf nf ms have "∫ (λt. pp f t - np f t) ∂M = pf-nf"
by (rule nnfis_minus_nnfis_integral)
hence "∫ f ∂M = pf-nf"
by (simp add: f_plus_minus[THEN sym])
also
from pg ng ms have "∫ (λt. pp g t - np g t) ∂M = pg-ng"
by (rule nnfis_minus_nnfis_integral)
hence "∫ g ∂M = pg-ng"
by (simp add: f_plus_minus[THEN sym])
moreover
from u v ms have "∫ (λt. u t - v t) ∂M = pf + pg - (nf + ng)"
by (rule nnfis_minus_nnfis_integral)
with uvf have "∫ (λt. f t + g t) ∂M = pf-nf + pg-ng"
by simp
ultimately
show "∫ (λt. f t + g t) ∂M = ∫ f ∂M + ∫ g ∂M"
by simp
qed

theorem integral_mono:
assumes f: "integrable f M"
and g: "integrable g M"  and fg: "f≤g"
shows "∫ f ∂M ≤ ∫ g ∂M"
proof -
from f obtain pf nf where pf: "pf ∈ nnfis (pp f) M"
and nf: "nf ∈ nnfis (np f) M" and ms: "measure_space M"
by (auto simp add: integrable_def)

from g obtain pg ng where pg: "pg ∈ nnfis (pp g) M"
and ng: "ng ∈ nnfis (np g) M"
by (auto simp add: integrable_def)

{ fix t
from fg have "f t ≤ g t"
by (simp add: le_fun_def)
hence "pp f t ≤ pp g t" and "np g t ≤ np f t"
by (auto simp add: positive_part_def negative_part_def)
}
hence "pp f ≤ pp g" and "np g ≤ np f"
by (simp_all add: le_fun_def)
with ms pf pg ng nf have "pf ≤ pg" and "ng ≤ nf"
by (simp_all add: nnfis_mono)

also
from ms pf pg ng nf have "(THE i. i ∈ nnfis (pp f) M) = pf"
and "(THE i. i ∈ nnfis (np f) M) = nf"
and "(THE i. i ∈ nnfis (pp g) M) = pg"
and "(THE i. i ∈ nnfis (np g) M) = ng"
by (auto simp add: nnfis_unique)
with f g have "∫ f ∂M = pf - nf"
and "∫ g ∂M = pg - ng"
by (auto simp add: integral_def)

ultimately show ?thesis
by simp
qed

theorem integral_times:
assumes int: "integrable f M"
shows "integrable (λt. a*f t) M" and "∫ (λt. a*f t) ∂M = a*∫ f ∂M"
(*<*)proof -
from int have "∫ f ∂M = (THE i. i ∈ nnfis (pp f) M) -
(THE j. j ∈ nnfis (np f) M)" by (simp only: integral_def)
also from int obtain k l where k: "k ∈ nnfis (pp f) M"
and l: "l ∈ nnfis (np f) M" and ms: "measure_space M"
by (auto simp add: integrable_def)

from k l ms have "(THE i. i ∈ nnfis (pp f) M) = k"
and "(THE i. i ∈ nnfis (np f) M) = l" by (auto simp add: nnfis_unique)
with int have uni: "k-l = ∫ f ∂M" by (simp add: integral_def)

have "integrable (λt. a*f t) M ∧ ∫ (λt. a*f t) ∂M = a*∫ f ∂M"
proof (cases "0≤a")
case True
hence pp: "pp (λt. a * f t) = (λt. a * pp f t)" and np: "np (λt. a * f t) = (λt. a * np f t)"
by (auto simp add: real_pp_np_pos_times)

from ms k True have "a*k ∈ nnfis (λt. a * pp f t) M" by (rule nnfis_times)
with pp have 1: "a*k ∈ nnfis (pp (λt. a * f t)) M" by simp

from np ms l True have 2: "a*l ∈ nnfis (np (λt. a * f t)) M"
by (simp add: nnfis_times)

from ms 1 2 have i: "integrable (λt. a*f t) M" by (auto simp add: integrable_def)
also
from 1 ms have "(THE i. i ∈ nnfis (pp (λt. a * f t)) M) = a*k" by (auto simp add: nnfis_unique)
moreover
from 2 ms have "(THE i. i ∈ nnfis (np (λt. a * f t)) M) = a*l" by (auto simp add: nnfis_unique)
ultimately
have "∫ (λt. a*f t) ∂M = a*k-a*l" by (simp add: integral_def)
also have "… = a*(k-l)" by (simp add: right_diff_distrib)
also note uni also note i
ultimately show ?thesis by simp
next
case False
hence pp: "pp (λt. a*f t) = (λt. -a*np f t)" and np: "np (λt. a*f t) = (λt. -a*pp f t)"
by (auto simp add: real_pp_np_neg_times)

from False have le: "0 ≤ -a" by simp
with ms l have "-a*l ∈ nnfis (λt. -a * np f t) M" by (rule nnfis_times)
with pp have 1: "-a*l ∈ nnfis (pp (λt. a * f t)) M" by simp

from ms k le have "-a*k ∈ nnfis (λt. -a * pp f t) M" by (rule nnfis_times)
with np have 2: "-a*k ∈ nnfis (np (λt. a * f t)) M" by simp

from ms 1 2 have i: "integrable (λt. a*f t) M" by (auto simp add: integrable_def)
also
from 1 ms have "(THE i. i ∈ nnfis (pp (λt. a * f t)) M) = -a*l" by (auto simp add: nnfis_unique)
moreover
from 2 ms have "(THE i. i ∈ nnfis (np (λt. a * f t)) M) = -a*k" by (auto simp add: nnfis_unique)
ultimately
have "∫ (λt. a*f t) ∂M = -a*l-(-a*k)" by (simp add: integral_def)
also have "… = a*(k-l)" by (simp add: right_diff_distrib)
also note uni also note i
ultimately show ?thesis by simp
qed
thus "integrable (λt. a*f t) M" and "∫ (λt. a*f t) ∂M = a*∫ f ∂M" by simp_all
qed(*>*)

(* Left out for lack of time

theorem sf_integral:
assumes M: "measure_space M" and f: "f = (λt. ∑i∈(S::nat set). x i * χ (A i) t)"
and A: "∀i∈S. A i ∈ measurable_sets M" and S: "finite S"
shows "∫ f ∂ M = (∑i∈S. x i * measure M (A i))"
and "integrable f M"
oops

constdefs
The probabilistic Quantifiers as in Hurd: p. 53 could be defined as a special case of this
almost_everywhere:: "('a set set * ('a set ⇒ real)) ⇒ ('a ⇒ bool) ⇒ bool" ("_-a.e. _")
"M-a.e. P == measure_space M ∧ (∃N. N ∈ measurable_sets M ∧ measure M N = 0 ∧ (∀w ∈ -N. P w))"

theorem assumes ae0: "M-a.e. (λw. f w = 0)"
shows ae0_nn_integ: "∫ f ∂ M = 0"
oops

theorem  assumes "integrable f M" and "integrable g M" and "M-a.e. (λw. f w ≤ g w)"
shows ae_integ_monotone: "∫ f ∂ M ≤ ∫ g ∂ M"
oops

theorem assumes aeq: "M-a.e. (λw. f w = g w)"
shows aeq_nn_integ: "integrable f M ⟹ ∫ f ∂ M = ∫ g ∂ M"
oops
*)

text‹To try out our definitions in an application, only one more
theorem is missing. The famous Markov--Chebyshev inequation is not
difficult to arrive at using the basic integral properties.›

theorem assumes int: "integrable f M" and a: "0<a" and intp: "integrable (λx. ¦f x¦ ^ n) M"
shows markov_ineq: "law M f {a..} ≤  ∫ (λx. ¦f x¦ ^ n) ∂M / (a^n)"
proof -
from int have rv: "f ∈ rv M"
by (rule integrable_rv)
hence ms: "measure_space M"
by (simp add: rv_def)
from ms rv have ams: "{w. a ≤ f w} ∈ measurable_sets M"
by (simp add: rv_ge_iff)

from rv have "(a^n)*law M f {a..} = (a^n)*measure M {w. a ≤ f w}"
by (simp add: distribution_def vimage_def)
also
from ms ams have int2: "integrable χ {w. a ≤ f w} M"
and eq2: "… = (a^n)*∫ χ {w. a ≤ f w} ∂ M"
by (auto simp add: integral_char)
note eq2 also
from int2 have int3: "integrable (λt. (a^n)*χ {w. a ≤ f w} t) M"
and eq3: "… = ∫ (λt. (a^n)*χ {w. a ≤ f w} t) ∂ M"
by (auto simp add: integral_times)
note eq3 also
{ fix t
from a have "(a^n)*χ {w. a ≤ f w} t ≤ ¦f t¦ ^ n"
proof (cases "a ≤ f t")
case False
thus ?thesis
by (simp add: characteristic_function_def)
next
case True
with a have "a ^ n ≤ (f t)^ n"
by (simp add: power_mono)
also
have "(f t)^ n ≤ ¦(f t) ^ n¦"
by arith
hence "(f t)^ n ≤ ¦f t¦ ^ n"
by (simp add: power_abs)
finally
show ?thesis
by (simp add: characteristic_function_def)
qed
}
with int3 intp have "… ≤ ∫ (λx. ¦f x¦ ^ n) ∂M"
by (simp add: le_fun_def integral_mono)

also
from a have "0 < a^n"
by (rule zero_less_power)
ultimately show ?thesis
by (simp add: pos_le_divide_eq mult.commute)
qed

end