# Theory Integral

Up to index of Isabelle/HOL/Integration

theory Integral
imports RealRandVar
(* The Lebesgue Integral     Stefan Richter 2002 *)header {*The Lebesgue Integral*}theory Integralimports RealRandVarbegin  (*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}  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 = {}; (\<Union>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 @{text 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: "(\<Union>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: setsum_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 setsum_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)qedlemma 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 (\<Union>i∈R. B i)" (*<*)proof -  have "(\<Union>i∈R. B i) = \<Union>(B  R)"    by simp  also have "… = \<Union>((λx. if x ∈ R then B x else {})  UNIV)"    by simp  also have "…  = (\<Union>x. if x ∈ R then B x else {})"    by (rule Union_image_eq)  finally have eq: "(\<Union>i∈R. B i) = (\<Union>i. if i∈R then B i else {})" .    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 "(\<Union>i. if i∈R then B i else {}) ∈ measurable_sets M"    by (simp add: measure_space_def sigma_algebra_def)    with meas2 dis2 have "(λn. measure M (if n ∈ R then B n else {}))    sums measure M (\<Union>i. if i∈R then B i else {})"    using ms by (simp add: measure_space_def countably_additive_def)  with eq show ?thesis      by simpqed(*>*)lemma sumr_setsum: "(∑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_setsum: "measure M (\<Union>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_setsum[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 (rule series_zero)  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 (\<Union>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: "(\<Union>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 (\<Union>i∈R. A ∩ B i) = (∑j∈R. measure M (A ∩ B j))"    by (rule measure_setsum)  also  from un have "A = (\<Union>i∈R. A ∩ B i)"    by auto  ultimately show ?thesis     by simpqed(*>*)lemma prod_encode_fst_inj: "inj (λi. prod_encode(i,j))" using inj_prod_encode  by (unfold inj_on_def) blastlemma 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) ∧ (\<Union>i∈K. C i) = UNIV   ∧ nonnegative z1 ∧ nonnegative z2"  using aproof 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: "(\<Union>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: "(\<Union>i∈S. B i) = UNIV"       and x: "nonnegative x" and y: "nonnegative y"      by simp_alltxt{*\nopagebreak*}    def "C" ≡ "(λ(i,j). A i ∩ B j) o prod_decode"    def "z1" ≡ "(λk. x (fst (prod_decode k)))"    def "z2" ≡ "(λk. y (snd (prod_decode k)))"    def "K" ≡ "{k. ∃i∈R. ∃j∈S. k = prod_encode (i,j)}"    def "G" ≡ "(λi. (λj. prod_encode (i,j))  S)"                                                def "H" ≡ "(λj. (λi. prod_encode (i,j))  R)"    { 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: setsum_right_distrib)        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 setsum_cong)        also from S have "… = (∑k∈(G i). z1 k * χ (C k) t)"          by (simp add: G_def Let_def o_def                setsum_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)"                by (rule inj_on_contraD)              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: setsum_right_distrib)                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 setsum_cong)                also from S have "… = (∑k∈(G i). z1 k * measure M (C k))"          by (simp add: G_def Let_def o_def                setsum_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 setsum_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 = (\<Union>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: setsum_UN_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: setsum_right_distrib 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 setsum_cong)        also from R have "… = (∑k∈(H j). z2 k * χ (C k) t)"           by (simp add: H_def Let_def o_def                setsum_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)"                by (rule inj_on_contraD)              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: setsum_right_distrib 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 setsum_cong)        also from R have "… = (∑k∈(H j). z2 k * measure M (C k))"          by (simp add: H_def Let_def o_def                setsum_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 setsum_cong)      with b have "b = (∑j∈S. (∑k∈(H j). z2 k * measure M (C k)))"         by simp      moreover have "K = (\<Union>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: setsum_UN_disjoint)            { fix i         from Bun have "(\<Union>k∈G i. C k) = A i"           by (simp add: G_def C_def)      }      with Aun have "(\<Union>i∈R. (\<Union>k∈G i. C k)) = UNIV"         by simp      hence "(\<Union>k∈(\<Union>i∈R. G i). C k) = UNIV"         by simp      with KG have Kun: "(\<Union>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: "UNION K C = 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  qedqedtext{*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) ∧ (\<Union>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) ∧ UNION K C = 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 setsum_addf[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"       by (rule add_nonneg_nonneg)  }     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: setsum_addf[THEN sym] distrib_right)  ultimately show ?thesis by simpqedlemma 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) ∧ (\<Union>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: "UNION K C = 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: setsum_0 setsum_cong)      with K iK have "z1 i * χ (C i) t = (∑k∈K. z1 k * χ (C k) t)"         by (simp add: setsum_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: setsum_0 setsum_cong)      with K iK have "(∑k∈K. z2 k * χ (C k) t) = z2 i * χ (C i) t"         by (simp add: setsum_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: setsum_mono)qedlemma 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 simpqedtext {*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 setsums, 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 -  def "R" ≡ "(λi::nat. if i = 0 then A else if i=1 then -A else {})::(nat=>'a set)"  def "x" ≡ "(λi::nat. if i = 0 then 1 else 0)::(nat => real)"  def "K" ≡ "{0,1::nat}"    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: "(\<Union>i∈K. R i) = UNIV" by (simp add: R_def K_def) fast  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 setsum_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 setsum_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 aproof 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: setsum_right_distrib)    also have "… = (∑i∈S. (z * x i) * χ (A i) t)"    proof (rule setsum_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 setsum_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: setsum_right_distrib)  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_setsum: "(∑i∈S. a i) ∈ sfis (λt. ∑i∈S. f i t) M" (*<*)using S aproof 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: setsum_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_setsum)qedtext{*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 fproof (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: setsum_0 setsum_constant add: setsum_mono)    hence "0 ≤ f t" by simp  }  thus ?thesis by (simp add: nonnegative_def)qed(*>*)lemma setsum_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 add: setsum_def)  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)  qedqed(*>*)lemma sfis_rv:   assumes ms: "measure_space M" and f: "a ∈ sfis f M"  shows "f ∈ rv M" using fproof (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: setsum_rv)  ultimately show ?thesis     by simpqed(*>*)(*>*)(*nonnegative function integral set*)(*>*)text{*\subsection {Nonnegative Functions}  \label{nnfis}There is one more important fact about @{text sfis}, easily the  hardest one to see. It is about the relationship with monotone  convergence and paves the way for a sensible definition of @{text  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  @{text 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 forceqed(*>*)    lemma sfis_mon_conv_mono:   assumes uf: "u\<up>f" and xu: "!!n. x n ∈ sfis (u n) M" and xy: "x\<up>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"    def B ≡ "(λn. {w. z*s w ≤ u n w})"     { 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 setsum_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: setsum_right_distrib[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)\<up>UNIV"    proof (unfold set_mon_conv, rule)      { fix n        from uf have um: "u n ≤ u (Suc n)"           by (simp add: realfun_mon_conv)        {           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)\<up>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 ∈ (\<Union>n. B n)"           by fast      }      thus "UNIV=(\<Union>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)\<up>(A j)"         by (auto simp add: set_mon_conv)      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_setsum)    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 real_mon_conv)   }  hence zr: "!!z. 0 < z ==> z < 1 ==> z * r ≤ y" .  thus ?thesis by (rule real_le_mult_sustain)qedtext {*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\<up>f; !!n. x n ∈ sfis (u n) M; x\<up>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)\<up>f t" by (simp add: real_mon_conv tendsto_const)  } hence "(λn. f)\<up>f" by (simp add: realfun_mon_conv_iff)  also   from s have "!!n. a ∈ sfis f M" .  moreover have "(λn. a)\<up>a" by (simp add: real_mon_conv 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 aproof (cases)  case (base u x)  with nn have "(λm w. z*u m w)\<up>(λ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)\<up>(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 simpqed(*>*)lemma nnfis_add:  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 aproof (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)\<up>(λw. f w + g w)"      by (simp add: realfun_mon_conv_add)    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)\<up>(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  qedqed(*>*)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 aproof (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\<up>g" and  "!!n. r n ∈ sfis (v n) M" and "r\<up>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: real_mon_conv LIMSEQ_le_const2)  qedqedcorollary 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 simpqed(*>*)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 @{text  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 setsum_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:setsum_0')  ultimately show ?thesis by simpqed(*>*)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) ∧ (\<Union>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) ∧ UNION K C = 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 autoqed(*>*)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)\<up>(f n)" and fh: "f\<up>h"  shows "(mu u)\<up>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 real_mon_conv)        also from uf have "(λm. u m (Suc n) t)\<up>(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 real_mon_conv)    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)\<up>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)\<up>l ∧ l ≤ h t"       by (rule real_mon_conv_bound)    then obtain l where       conv: "(λn. mu u n t)\<up>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 "∀n. muh n u m t ≤ muh (Suc n) u m t"             by simp          hence "muh n u m t ≤ muh (n+(m-n)) u m t"             by (rule lemma_f_mono_add)           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 real_mon_conv)      moreover       from conv have "(λn. mu u n t) ----> l"        by (simp add: real_mon_conv)      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 real_mon_conv)    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)\<up>(h t)"       by simp  }  with mon_upclose_def show "mu u\<up>h"     by (simp add: realfun_mon_conv_iff)qed(* The Beppo Levi - Theorem *)theorem nnfis_mon_conv:  assumes fh: "f\<up>h" and xf: "!!n. x n ∈ nnfis (f n) M" and xy: "x\<up>y"  and ms: "measure_space M"  shows "y ∈ nnfis h M"proof -  def u ≡ "(λn. SOME u. u\<up>(f n) ∧ (∀m. ∃a. a ∈ sfis (u m) M))"  { fix n    from xf[of n] have "∃u. u\<up>(f n) ∧ (∀m. ∃a. a ∈ sfis (u m) M)" (is "∃x. ?P x")    proof (cases)      case (base r a)      hence "r\<up>(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  def urev ≡ "(λm n. u n m)"  ultimately have uf: "!!n. (λm. urev m n)\<up>(f n)"     and sf: "!!n m. ∃a. a ∈ sfis (urev m n) M"    by auto    from uf fh have up: "mu urev\<up>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: realfun_mon_conv)    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\<up>l ∧ l ≤ y"     by (simp add: real_mon_conv_dom)  then obtain l where cl: "c\<up>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: real_mon_conv LIMSEQ_le_const2)  with ly have "l=y"     by simp  with int show ?thesis     by simpqedtext{*Establishing that only nonnegative functions may arise this way  is a triviality. *}lemma nnfis_nn: assumes "a ∈ nnfis f M"  shows "nonnegative f" (*<*)using assmsproof 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 real_mon_conv)    ultimately have "0 ≤ f t" by (simp add: LIMSEQ_le_const)  } thus ?thesis by (simp add: nonnegative_def)qed(*>*)(*>*)text{*\subsection{Integrable Functions}        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 fproof (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\<up>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\<up>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*)  def A ≡ "(λn i. {w. real i/(2::real)^n ≤ f w} ∩ {w. f w < real (Suc i)/(2::real)^n})"  def u ≡ "(λn t. ∑i∈{..<(n*2^n)}-{0}. (real i/(2::real)^n)*χ (A n i) t)"   def x ≡ "(λn. ∑i∈{..<(n*2^n)}-{0}. (real i/(2::real)^n)*measure M (A n i))"     { 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 x_def sfis_intro)  } thus "∀n. x n ∈ sfis (u n) M"     by simp    show "u\<up>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 setsum_cong)        also have "… = 0"          by (rule setsum_0)        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 setsum_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                def a ≡ "(f t)*(2::real)^n"        def 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: real_of_nat_less_iff[THEN sym])                    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: real_of_nat_add)          with un ai2 have fless: "f t < u n t + 1/(2::real)^n"            by (simp add: add_divide_distrib)                    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 (simp only: real_of_nat_mult power.simps) (simp add: mult_div_cancel)            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: real_of_nat_add)            also have "… = real i / (2::real)^n + real (1::nat) / (2 * (2::real)^n)"              by (simp add: add_divide_distrib)            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: real_of_nat_le_iff[THEN sym])            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 setsum_cong)          hence "u n t = 0"  by (simp add: u_def)                      also           { fix m            { fix i assume "i ∈ {..<(m*2^m)}-{0}"              hence  "0 ≤ real i / (2::real)^m * χ (A m i) t"                by (simp add: characteristic_function_def zero_le_divide_iff)            } hence "∀i∈{..<(m*2^m)}-{0}. 0 ≤ real i / (2::real)^m * χ (A m i) t"              by fast            hence "0 ≤ u m t"  by (simp add: u_def setsum_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)\<up>c ∧ c ≤ f t"        by (rule real_mon_conv_bound)      with uSuc obtain c where n0mc: "(λn. u (n+n0) t)\<up>c" and cle: "c ≤ f t"        by fast      from n0mc have "(λn. u (n+n0) t) ----> c"        by (simp add: real_mon_conv)      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 simp          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 (rule LIMSEQ_inverse_zero)      with lim have "(λn. u n t + inverse ((2::real)^n)) ----> c+0"        by (rule tendsto_add)      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)\<up> f t"        by (simp add: real_mon_conv)    }    thus ?thesis       by (simp add: realfun_mon_conv_iff)  qedqed(*>*)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 bproof (cases)  case (base v r)  from ms f nn have "∃u x. u\<up>f ∧ (∀n. x n ∈ sfis (u n) M)"     by (rule rv_mon_conv_sfis)  then obtain u x where uf: "u\<up>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: realfun_mon_conv)    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\<up>a ∧ a ≤ b"     by (rule real_mon_conv_bound)  then obtain a where xa: "x\<up>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 fastqedtext{* 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" ("\<integral> _ ∂_"(*<*)[60,61] 110(*>*)) where  "integrable f M ==> \<integral> 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 "\<integral> 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 "\<integral> f ∂ M = a"     by (simp add: integral_def)qedlemma 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 "\<integral> (λ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"     by (rule nnfis_add)  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"     by (auto simp add: nnfis_add)  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 "\<integral> (λt. f t - g t) ∂ M = a - b"     by (simp add: integral_def)qedtext{*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 "\<integral> χ 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 "\<integral> χ A ∂ M = measure M A"     by (rule nnfis_integral)  from nnfis and ms show "integrable χ A M"     by (rule nnfis_integral) qed(*>*)theorem integral_add:  assumes f: "integrable f M" and g: "integrable g M"  shows "integrable (λt. f t + g t) M"  and "\<integral> (λt. f t + g t) ∂M = \<integral> f ∂M + \<integral> g ∂M"proof -  def u ≡ "(λt. pp f t + pp g t)"  def 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"     by (simp add: nnfis_add)   from ms nf ng v_def have    v: "nf+ng ∈ nnfis v M"     by (simp add: nnfis_add)    { 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 "\<integral> (λt. pp f t - np f t) ∂M = pf-nf"    by (rule nnfis_minus_nnfis_integral)  hence "\<integral> f ∂M = pf-nf"    by (simp add: f_plus_minus[THEN sym])  also   from pg ng ms have "\<integral> (λt. pp g t - np g t) ∂M = pg-ng"    by (rule nnfis_minus_nnfis_integral)  hence "\<integral> g ∂M = pg-ng"    by (simp add: f_plus_minus[THEN sym])  moreover  from u v ms have "\<integral> (λt. u t - v t) ∂M = pf + pg - (nf + ng)"    by (rule nnfis_minus_nnfis_integral)  with uvf have "\<integral> (λt. f t + g t) ∂M = pf-nf + pg-ng"    by simp  ultimately  show "\<integral> (λt. f t + g t) ∂M = \<integral> f ∂M + \<integral> g ∂M"    by simpqed  theorem integral_mono:  assumes f: "integrable f M"      and g: "integrable g M"  and fg: "f≤g"  shows "\<integral> f ∂M ≤ \<integral> 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 "\<integral> f ∂M = pf - nf"    and "\<integral> g ∂M = pg - ng"    by (auto simp add: integral_def)    ultimately show ?thesis    by simpqedtheorem integral_times:  assumes int: "integrable f M"  shows "integrable (λt. a*f t) M" and "\<integral> (λt. a*f t) ∂M = a*\<integral> f ∂M"(*<*)proof -  from int have "\<integral> 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 = \<integral> f ∂M" by (simp add: integral_def)  have "integrable (λt. a*f t) M ∧ \<integral> (λt. a*f t) ∂M = a*\<integral> 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 "\<integral> (λ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 "\<integral> (λ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 "\<integral> (λt. a*f t) ∂M = a*\<integral> f ∂M" by simp_allqed(*>*) (* 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 "\<integral> f ∂ M = (∑i∈S. x i * measure M (A i))"   and "integrable f M"  sorry  constdefs  The probabilistic Quantifiers as in Hurd: p. 53 could be defined as a special case of thisalmost_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: "\<integral> f ∂ M = 0"  sorrytheorem  assumes "integrable f M" and "integrable g M" and "M-a.e. (λw. f w ≤ g w)"  shows ae_integ_monotone: "\<integral> f ∂ M ≤ \<integral> g ∂ M"  sorrytheorem assumes aeq: "M-a.e. (λw. f w = g w)"   shows aeq_nn_integ: "integrable f M ==> \<integral> f ∂ M = \<integral> g ∂ M"  sorry    *)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..} ≤  \<integral> (λ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)*\<integral> χ {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: "… = \<integral> (λ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 "… ≤ \<integral> (λ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)qedend