Quellcode-Bibliothek Integral.thy

(* 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 \<in> 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 \<in> sfis f M" and (*<*)b:(*>*) "b \<in> 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 inj_on_subset[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: 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 inj_on_subset[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 inj_on_subset[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: 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 inj_on_subset[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" 
      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: 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(*>*)


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 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)"
      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)↑(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 \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> real) \<Rightarrow> nat \<Rightarrow> ('a \<Rightarrow> real)" (\<open>mu\<close>) 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 \<in> 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.\<close>(*<*)



declare zero_le_power [simp]
(*>*)
lemma assumes (*<*)ms:(*>*) "measure_space M" and (*<*)f(*>*): "f \<in> 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"
            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 (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)"
              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: 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"
        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)↑ 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" 
    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 "∫ (λ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(*>*)


theorem integral_add:
  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" 
    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 "∫ (λ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 = (\<lambda>t. \<Sum>i\<in>(S::nat set). x i * \<chi> (A i) t)"
  and A: "\<forall>i\<in>S. A i \<in> measurable_sets M" and S: "finite S"
  shows "\<integral> f \<partial> M = (\<Sum>i\<in>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 \<Rightarrow> real)) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" ("_-a.e. _")
"M-a.e. P == measure_space M \<and> (\<exists>N. N \<in> measurable_sets M \<and> measure M N = 0 \<and> (\<forall>w \<in> -N. P w))"

theorem assumes ae0: "M-a.e. (\<lambda>w. f w = 0)" 
  shows ae0_nn_integ: "\<integral> f \<partial> M = 0"
  oops

theorem  assumes "integrable f M" and "integrable g M" and "M-a.e. (\<lambda>w. f w \<le> g w)"
  shows ae_integ_monotone: "\<integral> f \<partial> M \<le> \<integral> g \<partial> M"
  oops

theorem assumes aeq: "M-a.e. (\<lambda>w. f w = g w)" 
  shows aeq_nn_integ: "integrable f M \<Longrightarrow> \<integral> f \<partial> M = \<integral> g \<partial> 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