Theory RealRandVar

theory RealRandVar
imports Measure Countable
section ‹Real-Valued random variables \label{sec:realrandvar}›

theory RealRandVar
imports Measure "HOL-Library.Countable"
begin

text ‹While most of the above material was modeled after Hurd's work
  (but still proved independently),
  the original content basically starts here\footnote{There are two
  main reasons why the above has not been imported using Sebastian
Skalberg's import tool \cite{Skalberg}. Firstly, there are
  inconveniences caused by different conventions in HOL, meaning
  predicates instead of sets foremost, that make the consistent use of
  such basic definitions impractical. What is more, the import tool
  simply was not available at the time these theories were
  written.}. From now
  on, we will specialize in functions that map into
  the real numbers and are measurable with respect to the canonical sigma
  algebra on the reals, the Borel sigma algebra. These functions will
  be called real-valued random variables. The terminology is slightly
  imprecise, as random variables hint at a probability space, which
  usually requires ‹measure M UNIV = 1›. Notwithstanding, as we regard
  only finite measures (cf. \ref{sec:measure-spaces}), this condition can
  easily be achieved by normalization. After all, the other standard
  name, ``measurable functions'', is even less precise.

  A lot of the theory in this and the preceding section has also been
  formalized within the Mizar project \cite{mesfunc1,mesfunc2}. The
  abstract of the second source hints that it was also planned as a
  stepping stone for Lebesgue integration, though further results in
  this line could not be found. The main difference lies in the use of
  extended real numbers --- the reals together with ‹±∞› --- in
  those documents. It is established practice in measure theory
  to allow infinite values, but ``($\ldots$) we felt that the complications
  that this generated ($\ldots$) more than canceled out the gain in
  uniformity ($\ldots$), and that a simpler theory resulted from sticking to
  the standard real numbers.'' \cite[p.~32f]{hurd2002}. Hurd also advocates
  going directly to the hyper-reals, should the need for infinite
  measures arise. I agree, nevertheless sticking to his example for the reasons
  mentioned in the prologue.›
  
(*First of all, for the definition of a real valued random variable,
we need the Borel-σ-Algebra on the Reals*)
(*The smallest σ-Algebra containing {..u} for all rational u is
  sufficient, but we use all real u for simplicity!*)

definition
  Borelsets:: "real set set" ("𝔹") where
  "𝔹 = sigma {S. ∃u. S={..u}}"

definition
(*We use Joe Hurd's formalism of a measure space (which assumes that 
  the universe is always the whole type universe)*)
  rv:: "('a set set * ('a set ⇒ real)) ⇒ ('a ⇒ real) set" where
  "rv M = {f. measure_space M ∧ f ∈ measurable (measurable_sets M) 𝔹}"

text ‹As explained in the first paragraph, the preceding
  definitions\footnote{The notation $‹{..u}›$ signifies the
  interval from negative infinity to $u$ included.}
  determine the rest of this section. There are many ways to define
  the Borel sets. For example, taking into account only rationals for
  $u$ would also have worked out above, but we can take the reals to
  simplify things. The smallest sigma algebra containing all the open
  (or closed) sets is another alternative; the multitude of
  possibilities testifies to the relevance of the concept.  

  The latter path leads the way to the fact that any continuous function is
  measurable. Generalization for $‹ℝ›^n$ brings another unified way to
  prove all the measurability theorems in this theory plus, for instance,
  measurability of the trigonometric and exponential functions. This approach is detailed in another influential textbook
  by Billingsley \cite{Billingsley86}. It requires some concepts of
  topologic spaces, which made the following elementary
  course, based on Bauer's excellent book \cite{Bauer}, seem more feasible.
   
  Two more definitions go next. The image measure, law, or
  distribution --- the last term being specific to probability --- of a  
  measure with respect to a measurable function is calculated as the measure of the
  inverse image of a set. Characteristic functions will
  be frequently needed in the rest of the development. 
›
(*Perhaps one day we will need distributions, this might be the right
time to define them*)

definition
  distribution:: 
  "('a set set * ('a set ⇒ real)) ⇒ ('a ⇒ real) ⇒ (real set ⇒ real)" ("law") where
  "f ∈ rv M ⟹ law M f ≡ (measure M) ∘ (vimage f)"

definition
  characteristic_function:: "'a set ⇒ ('a ⇒ real)" ("χ _"(*<*)[1000](*>*)) where
  "χ A x ≡ if x ∈ A then 1 else 0" 

lemma char_empty: "χ {} = (λt. 0)"
proof (rule ext)
  fix t
  show "χ {} t = 0" by (simp add: characteristic_function_def)
qed

text ‹Now that random variables are defined, we aim to show that a
  broad class of functions belongs to them. For a constant function
  this is easy, as there are only two possible preimages.›
  (*measurability lemmata*)

lemma assumes sigma: "sigma_algebra S"
  shows const_measurable: "(λx. (c::real)) ∈ measurable S X"
proof (unfold measurable_def, rule, rule)
  fix g
  show "(λx. c) -` g ∈ S"
  proof (cases "c ∈ g")
    case True 
    hence "(λx::'a. c) -` g = UNIV" 
      by blast
    moreover from sigma have "UNIV ∈ S" 
      by (rule sigma_algebra_UNIV)
    ultimately show ?thesis by simp
  next
    case False
    hence "(λx::'a. c) -` g = {}" 
      by blast
    moreover from sigma have "{} ∈ S" 
      by (simp only: sigma_algebra_def)
    ultimately show ?thesis by simp
    txt‹\nopagebreak›   
  qed                     
qed                       

theorem assumes ms: "measure_space M"
  shows const_rv: "(λx. c) ∈ rv M" using ms
  by (auto simp only: measure_space_def const_measurable rv_def)

text‹Characteristic functions produce four cases already, so the
  details are glossed over.›

lemma assumes a: "a ∈ S" and sigma: "sigma_algebra S" shows 
char_measurable : "χ a ∈ measurable S x"
(*<*)proof -
  {fix g
    have "χ a -` g ∈ S"
    proof (cases "1 ∈ g")
      case True
      show ?thesis
      proof (cases "0 ∈ g") 
        case True
        with ‹1 ∈ g› have "χ a -` g = UNIV" by (auto simp add: vimage_def characteristic_function_def)
        with sigma show ?thesis by (auto simp add: sigma_algebra_UNIV) 
      next
        case False 
        with ‹1 ∈ g› have "χ a -` g = a" 
          by (auto simp add: vimage_def characteristic_function_def)
        with a show ?thesis by simp
      qed
      
    next
      case False
      show ?thesis
      proof (cases "0 ∈ g")
        case True
        with ‹1 ∉ g› have "χ a -` g = -a" 
          by (auto simp add: vimage_def characteristic_function_def)
        with a sigma show ?thesis by (simp add: sigma_algebra_def)
      next
        case False
        with ‹1 ∉ g› have "χ a -` g = {}" by (auto simp add: vimage_def characteristic_function_def)
        moreover from sigma have "{} ∈ S" by  (simp only: sigma_algebra_def)
        ultimately show ?thesis by simp
      qed
    qed}
  thus ?thesis by (unfold measurable_def) blast
qed(*>*)


theorem assumes ms: "measure_space M" and A: "A ∈ measurable_sets M"
  shows char_rv: "χ A ∈ rv M" using ms A
  by (auto simp only: measure_space_def char_measurable rv_def)  

text ‹For more intricate functions, the following application of the
  measurability lifting theorem from \ref{sec:measure-spaces} gives a
  useful characterization.›

theorem assumes ms: "measure_space M" shows 
  rv_le_iff: "(f ∈ rv M) = (∀a. {w. f w ≤ a} ∈ measurable_sets M)"
proof - 
  
  have "f ∈ rv M ⟹ ∀a. {w. f w ≤ a} ∈ measurable_sets M"
  proof 
    { fix a 
      assume "f ∈ measurable (measurable_sets M) 𝔹"
      hence "∀b∈𝔹. f -` b ∈ measurable_sets M"
        by (unfold measurable_def) blast
      also have "{..a} ∈ 𝔹" 
        by (simp only: Borelsets_def) (rule sigma.basic, blast)
      ultimately have "{w. f w ≤ a} ∈ measurable_sets M" 
        by (auto simp add: vimage_def) 
    }
    thus "⋀a. f ∈ rv M ⟹ {w. f w ≤ a} ∈ measurable_sets M" 
      by (simp add: rv_def)
  qed
  
  also have "∀a. {w. f w ≤ a} ∈ measurable_sets M ⟹ f ∈ rv M"
  proof -
    assume "∀a. {w. f w ≤ a} ∈ measurable_sets M"
    hence "f ∈ measurable (measurable_sets M){S. ∃u. S={..u}}" 
      by (auto simp add: measurable_def vimage_def)
    with ms have "f ∈ measurable (measurable_sets M) 𝔹" 
      by (simp only: Borelsets_def measure_space_def measurable_lift)
    with ms show ?thesis 
      by (auto simp add: rv_def)
   txt‹\nopagebreak›                            
  qed
  ultimately show ?thesis by rule 
qed 

 
text ‹The next four lemmata allow for a ring deduction that helps establish
  this fact for all of the signs ‹<›, ‹>› and ‹≥› as well.›

lemma assumes sigma: "sigma_algebra A" and le: "∀a. {w. f w ≤ a} ∈ A" 
  shows le_less: "∀a. {w. f w < (a::real)} ∈ A"
proof 
  fix a::real
  from le sigma have "(⋃n::nat. {w. f w ≤ a - inverse (real (Suc n))}) ∈ A" 
    by (simp add: sigma_algebra_def) 
  also
  have "(⋃n::nat. {w. f w ≤ a - inverse (real (Suc n))}) = {w. f w < a}" 
  proof -
    {
      fix w n 
      have "0 < inverse (real (Suc (n::nat)))" 
        by simp                                
      hence "f w ≤ a - inverse (real (Suc n)) ⟹ f w < a" 
        by arith                                           
    }
    also
    { fix w
      have "(λn. inverse (real (Suc n))) ⇢ 0" 
        by (rule LIMSEQ_inverse_real_of_nat)

      also assume "f w < a"
      hence "0 < a - f w" by simp
     
      ultimately have 
        "∃n0. ∀n. n0 ≤ n ⟶ abs (inverse (real (Suc n))) < a - f w" 
        by (auto simp add: lim_sequentially dist_real_def) 
      then obtain n where  "abs (inverse (real (Suc n))) < a - f w" 
        by blast
      hence "f w ≤ a - inverse (real (Suc n))" 
        by arith
      hence "∃n. f w ≤ a - inverse (real (Suc n))" ..
    }
    ultimately show ?thesis by auto
  qed
  finally show "{w. f w < a} ∈ A" .
qed

lemma assumes sigma: "sigma_algebra A" and less: "∀a. {w. f w < a} ∈ A" 
  shows less_ge: "∀a. {w. (a::real) ≤ f w} ∈ A"  
proof 
  fix a::real
  from less sigma have "-{w. f w < a} ∈ A" 
    by (simp add: sigma_algebra_def)
  also
  have "-{w. f w < a} = {w. a ≤ f w}" 
    by auto 
  
  finally show "{w. a ≤ f w} ∈ A" .
qed

lemma assumes sigma: "sigma_algebra A" and ge: "∀a. {w. a ≤ f w} ∈ A" 
  shows ge_gr: "∀a. {w. (a::real) < f w} ∈ A"
(*<*)proof 
  fix a::real
  from ge sigma have "(⋃n::nat. {w. a + inverse (real (Suc n)) ≤ f w}) ∈ A" 
    by (simp add: sigma_algebra_def) 
  also
  have "(⋃n::nat. {w. a + inverse (real (Suc n)) ≤ f w}) = {w. a < f w}" 
  proof -
    {
      fix w n 
      have "0 < inverse (real (Suc (n::nat)))" by simp
      hence "a + inverse (real (Suc n)) ≤ f w ⟹ a < f w" by arith
    }
    also
    { fix w
      have "(λn. inverse (real (Suc n))) ⇢ 0" by (rule LIMSEQ_inverse_real_of_nat)
      
      also assume "a < f w"
      hence "0 < f w - a" by simp

      ultimately have "∃n0. ∀n. n0 ≤ n ⟶ abs (inverse (real (Suc n))) < f w - a" 
        by (auto simp add: lim_sequentially dist_real_def) 
      then obtain n where  "abs (inverse (real (Suc n))) < f w - a" by blast      
      hence "a + inverse (real (Suc n)) ≤ f w" by arith
      hence "∃n. a + inverse (real (Suc n)) ≤ f w" ..
    }
    ultimately show ?thesis by auto
  qed
    
  finally show "{w. a < f w} ∈ A" .
qed(*>*)


lemma assumes sigma: "sigma_algebra A" and gr: "∀a. {w. a < f w} ∈ A" 
  shows gr_le: "∀a. {w. f w ≤ (a::real)} ∈ A"
(*<*)proof 
  fix a::real
  from gr sigma have "-{w. a < f w} ∈ A" by (simp add: sigma_algebra_def)
  also
  have "-{w. a < f w} = {w. f w ≤ a}" by auto 
  
  finally show "{w. f w ≤ a} ∈ A" .
qed(*>*)   

theorem assumes ms: "measure_space M" shows 
  rv_ge_iff: "(f ∈ rv M) = (∀a. {w. a ≤ f w} ∈ measurable_sets M)"
proof -
  from ms have "(f ∈ rv M) = (∀a. {w. f w ≤ a} ∈ measurable_sets M)" 
    by (rule rv_le_iff)
  also have "… = (∀a. {w. a ≤ f w} ∈ measurable_sets M)" (is "?lhs = ?rhs")
  proof -
    from ms have sigma: "sigma_algebra (measurable_sets M)" 
      by (simp only: measure_space_def)
    also note less_ge le_less 
    ultimately have "?lhs ⟹ ?rhs" by blast 
    also 
    from sigma gr_le ge_gr have "?rhs ⟹ ?lhs" by blast
    ultimately 
    show ?thesis ..
  qed
  finally show ?thesis .
qed

theorem assumes ms: "measure_space M" shows 
  rv_gr_iff: "(f ∈ rv M) = (∀a. {w. a < f w} ∈ measurable_sets M)"
(*<*)proof -
  from ms have "(f ∈ rv M) = (∀a. {w.  a ≤ f w} ∈ measurable_sets M)" by (rule rv_ge_iff)
  also have "… = (∀a. {w.  a < f w} ∈ measurable_sets M)" (is "?lhs = ?rhs")
  proof -
    from ms have sigma: "sigma_algebra (measurable_sets M)" by (simp only: measure_space_def)
    also note ge_gr ultimately have "?lhs ⟹ ?rhs" by blast 
    also from sigma less_ge le_less gr_le have "?rhs ⟹ ?lhs" by blast
    ultimately show ?thesis ..
  qed 
  finally show ?thesis .
qed(*>*)


theorem assumes ms: "measure_space M" shows 
  rv_less_iff: "(f ∈ rv M) = (∀a. {w. f w < a} ∈ measurable_sets M)"
(*<*)proof -
  from ms have "(f ∈ rv M) = (∀a. {w. a ≤ f w} ∈ measurable_sets M)" by (rule rv_ge_iff)
  also have "… = (∀a. {w. f w < a} ∈ measurable_sets M)" (is "?lhs = ?rhs")
  proof -
    from ms have sigma: "sigma_algebra (measurable_sets M)" by (simp only: measure_space_def)
    also note le_less gr_le ge_gr ultimately have "?lhs ⟹ ?rhs" by blast 
    also from sigma less_ge have "?rhs ⟹ ?lhs" by blast
    ultimately show ?thesis ..
  qed 
  finally show ?thesis .
qed(*>*)


text ‹As a first application we show that addition and multiplication
  with constants preserve measurability. This is a precursor to the
  more general addition and multiplication theorems later on. You can see that
  quite a few properties of the real numbers are employed.›

lemma assumes g: "g ∈ rv M" 
  shows affine_rv: "(λx. (a::real) + (g x) * b) ∈ rv M"
proof (cases "b=0")
  from g have ms: "measure_space M" 
    by (simp add: rv_def)
  case True
  hence "(λx. a + (g x) * b) = (λx. a)" 
    by simp
  also 
  from g have "(λx. a) ∈ rv M" 
    by (simp add: const_measurable rv_def measure_space_def)
  ultimately show ?thesis by simp

next
  from g have ms: "measure_space M" 
    by (simp add: rv_def)
  case False
  have calc: "⋀x c. (a + g x * b ≤ c) = (g x * b  ≤ c - a)" 
    by arith
  have "∀c. {w.  a + g w * b ≤ c} ∈ measurable_sets M"
  proof (cases "b<0")    
    case False
    with ‹b ≠ 0› have "0<b" by arith
    hence "⋀x c.  (g x * b  ≤ c - a) = (g x ≤ (c - a) / b)"  
      by (rule pos_le_divide_eq [THEN sym])
    with calc have "⋀c. {w.  a + g w * b ≤ c} = {w. g w ≤ (c - a) / b}" 
      by simp
  
    also from ms g  have "∀a. {w. g w ≤ a} ∈ measurable_sets M"  
      by (simp add: rv_le_iff)
    
    ultimately show ?thesis by simp
    
  next
    case True
    hence "⋀x c. (g x * b ≤ c-a) = ((c-a)/b ≤ g x)"  
      by (rule neg_divide_le_eq [THEN sym])
    with calc have "⋀c. {w.  a + g w * b ≤ c} = {w. (c-a)/b ≤ g w}" 
      by simp

    also from ms g have "∀a. {w. a ≤ g w } ∈ measurable_sets M"  
      by (simp add: rv_ge_iff)
    
    ultimately show ?thesis by simp
  qed

  with ms show ?thesis 
    by (simp only: rv_le_iff [THEN sym])
qed
  
text ‹For the general case of addition, we need one more set to be
  measurable, namely ‹{w. f w ≤ g w}›. This follows from a
  like statement for $<$. A dense and countable
  subset of the reals is needed to establish it. 

  Of course, the rationals come to
  mind. They were not available in Isabelle/HOL\footnote{At least not
  as a subset of the reals, to the definition of which a type of
  positive rational numbers contributed \cite{Fleuriot:2000:MNR}.}, so
  I built a theory with the necessary properties on my own. [Meanwhile
  Isabelle has proper rationals and SR's development of the rationals has been
  moved to and merged with Isabelle's rationals.›

(*For this theorem, we need some properties of the rational numbers
(or any other dense and countable set in the reals - so why not use
the rationals?).*)


lemma assumes f: "f ∈ rv M" and g: "g ∈ rv M"
  shows rv_less_rv_measurable: "{w. f w < g w} ∈ measurable_sets M"
proof -
  let "?I i" = "let s::real = of_rat(nat_to_rat_surj i) in {w. f w < s} ∩ {w. s < g w}"
  from g have ms: "measure_space M" by (simp add: rv_def)
  have "{w. f w < g w} = (⋃i. ?I i)"
  proof
    { fix w assume "w ∈ {w. f w < g w}"
      hence "f w < g w" ..
      hence "∃s∈ℚ. f w < s ∧ s < g w" by (rule Rats_dense_in_real)
      hence "∃s∈ℚ. w ∈ {w. f w < s} ∩ {w. s < g w}" by simp
      hence "∃i. w ∈ ?I i"
        by(simp add:Let_def)(metis surj_of_rat_nat_to_rat_surj)
      hence "w ∈ (⋃i. ?I i)" by simp
    }
    thus "{w. f w < g w} ⊆ (⋃i. ?I i)" ..
    
    show "(⋃i. ?I i) ⊆ {w. f w < g w}" by (force simp add: Let_def)
  qed
  moreover have "(⋃i. ?I i) ∈ measurable_sets M"
  proof -
    from ms have sig: "sigma_algebra (measurable_sets M)" 
      by (simp only: measure_space_def)    
    { fix s
      note sig
      also from ms f have "{w. f w < s} ∈ measurable_sets M" (is "?a∈?M") 
        by (simp add: rv_less_iff)
      moreover from ms g have "{w. s < g w} ∈ ?M" (is "?b ∈ ?M") 
        by (simp add: rv_gr_iff)
      ultimately have "?a ∩ ?b ∈ ?M" by (rule sigma_algebra_inter)
    }
    hence "∀i. ?I i ∈ measurable_sets M" by (simp add: Let_def)
    with sig show ?thesis by (auto simp only: sigma_algebra_def Let_def)
  qed
  ultimately show ?thesis by simp
qed

(*The preceding theorem took me about 1 month to establish through its deep dependencies*)
lemma assumes f: "f ∈ rv M" and g: "g ∈ rv M"
  shows rv_le_rv_measurable: "{w. f w ≤ g w} ∈ measurable_sets M" (is "?a ∈ ?M")
proof -
  from g have ms: "measure_space M" 
    by (simp add: rv_def)
  from g f have "{w. g w < f w} ∈ ?M" 
    by (rule rv_less_rv_measurable)
  also from ms have "sigma_algebra ?M" 
    by (simp only: measure_space_def)
  
  ultimately have "-{w. g w < f w} ∈ ?M" 
    by (simp only: sigma_algebra_def)
  also have "-{w. g w < f w} = ?a" 
    by auto
txt‹\nopagebreak›  
  finally show ?thesis .
qed

lemma assumes f: "f ∈ rv M" and g: "g ∈ rv M" 
  shows f_eq_g_measurable: "{w. f w = g w} ∈ measurable_sets M" (*<*)(is "?a ∈ ?M")
proof -
  from g have ms: "measure_space M" by (simp add: rv_def)
  hence "sigma_algebra ?M" by (simp only: measure_space_def)
  also from f g ms have "{w. f w ≤ g w} ∈ ?M" and "{w. g w ≤ f w} ∈ ?M" 
    by (auto simp only: rv_le_rv_measurable)
  
  ultimately have "{w. f w ≤ g w} ∩ {w. g w ≤ f w} ∈ ?M" (is "?b ∈ ?M") 
    by (rule sigma_algebra_inter)
  also have "?b = ?a" by auto
  
  finally show ?thesis .
qed(*>*)


lemma assumes f: "f ∈ rv M" and g: "g ∈ rv M" 
  shows f_noteq_g_measurable: "{w. f w ≠ g w} ∈ measurable_sets M" (*<*)(is "?a ∈ ?M")
proof -
  from g have ms: "measure_space M" by (simp add: rv_def)
  hence "sigma_algebra ?M" by (simp only: measure_space_def)
  also from f g have "{w. f w = g w} ∈ ?M" by (rule f_eq_g_measurable)
  
  ultimately have "-{w. f w = g w} ∈ ?M" by (simp only: sigma_algebra_def)
  also have "-{w. f w = g w} = ?a" by auto

  finally show ?thesis .
qed(*>*)

text ‹With these tools, a short proof for the addition theorem is
  possible.›

theorem assumes f: "f ∈ rv M" and g: "g ∈ rv M" 
  shows rv_plus_rv: "(λw. f w + g w) ∈ rv M"
proof -
  from g have ms: "measure_space M" by (simp add: rv_def)
  { fix a 
    have "{w. a ≤ f w + g w} = {w. a + (g w)*(-1) ≤ f w}" 
      by auto
    moreover from g have "(λw. a + (g w)*(-1)) ∈ rv M" 
      by (rule affine_rv) 
    with f have "{w. a + (g w)*(-1) ≤ f w} ∈ measurable_sets M"  
      by (simp add: rv_le_rv_measurable)
    ultimately have "{w. a ≤ f w + g w} ∈ measurable_sets M" by simp
  }
  with ms show ?thesis 
    by (simp add: rv_ge_iff)
  thm rv_ge_iff
qed

text ‹To show preservation of measurability by multiplication, it is
  expressed by addition and squaring. This requires a few technical
  lemmata including the one stating measurability for squares, the proof of which is skipped.›

(*This lemma should probably be in the RealPow Theory or a special Sqroot-Theory*)
lemma pow2_le_abs: "(a2 ≤ b2) = (¦a¦ ≤ ¦b::real¦)"
(*<*)proof -
  have "(a2 ≤ b2) = (¦a¦2 ≤ ¦b¦2)" by (simp add: numeral_2_eq_2)
  also have "… = (¦a¦ ≤ ¦b¦)" 
  proof
    assume "¦a¦ ≤ ¦b¦"
    thus "¦a¦2 ≤ ¦b¦2"
      by (rule power_mono) simp
  next
    assume "¦a¦2 ≤ ¦b¦2" hence "¦a¦^(Suc 1) ≤ ¦b¦^(Suc 1)" by (simp add: numeral_2_eq_2)
    moreover have "0 ≤ ¦b¦" by auto
    ultimately show "¦a¦ ≤ ¦b¦" by (rule power_le_imp_le_base)
  qed
  finally show ?thesis .
qed(*>*)

lemma assumes f: "f ∈ rv M" 
  shows rv_square: "(λw. (f w)2) ∈ rv M"
(*<*)proof -
  from f have ms: "measure_space M" by (simp add: rv_def)
  hence "?thesis = (∀a. {w. (f w)2 ≤ a} ∈ measurable_sets M)" (is "_ = (∀a. ?F a ∈ ?M)") by (rule rv_le_iff)
  also {
    fix a
    from ms have sig: "sigma_algebra ?M" by (simp only: measure_space_def)
    have "?F a ∈ ?M"
    proof (cases "a < 0")
      
      case True
      { fix w
        note True
        also have "0 ≤ (f w)2" by simp
        finally have "((f w)2 ≤ a) = False" by simp
      } hence "?F a = {}" by simp
      thus ?thesis using sig by (simp only: sigma_algebra_def)
      
    next
      case False
      show ?thesis
      proof (cases "a = 0")
        
        case True also
        { fix w
          have "0 ≤ (f w)2" by simp
          hence "((f w)2 ≤ 0) ⟹ ((f w)2 = 0)" by (simp only: order_antisym)
          hence "((f w)2 ≤ 0) = ((f w)2 = 0)" by (force simp add: numeral_2_eq_2)
          also have "… = (f w = 0)" by simp     
          finally have "((f w)2 ≤ 0) = …" .
        }
        
        ultimately have "?F a = {w. f w = 0}" by simp
        moreover have "… = {w. f w ≤ 0} ∩ {w. 0 ≤ f w}" by auto
        moreover have "… ∈ ?M"
        proof - 
          from ms f have "{w. f w ≤ 0} ∈ ?M" by (simp only: rv_le_iff)
          also from ms f have "{w. 0 ≤ f w} ∈ ?M" by (simp only: rv_ge_iff)
          ultimately show ?thesis using sig by (simp only: sigma_algebra_inter)
        qed
        
        ultimately show ?thesis by simp
   
      next
        case False
        with ‹¬ a < 0› have "0<a" by (simp add: order_less_le)
        then have "∃ sqra. 0<sqra ∧ sqra2 = a" by (simp only: realpow_pos_nth2 numeral_2_eq_2)
        then have "⋀w. ∃ sqra. ?F a = {w. -sqra ≤ f w} ∩ {w. f w ≤ sqra}"
          by (force simp only: pow2_le_abs abs_le_iff)
        then obtain sqra where "?F a = {w. -sqra ≤ f w} ∩ {w. f w ≤ sqra}" by fast
        moreover have "… ∈ ?M" 
        proof - 
          from ms f have "{w. f w ≤ sqra} ∈ ?M" by (simp only: rv_le_iff)
          also from ms f have "{w. -sqra ≤ f w} ∈ ?M" by (simp only: rv_ge_iff)
          ultimately show ?thesis using sig by (simp only: sigma_algebra_inter)
        qed
        
        ultimately show ?thesis by simp
      
      qed 
    qed
  }
  
  ultimately show ?thesis by simp

qed(*>*)

lemma realpow_two_binomial_iff: "(f+g::real)2 = f2 + 2*(f*g) + g2"
  (*<*) 
  by (simp add: power2_eq_square distrib_right distrib_left)(*>*) 

lemma times_iff_sum_squares: "f*g = (f+g)2/4 - (f-g)2/(4::real)"
  by (simp add: power2_eq_square field_simps)

theorem assumes f: "f ∈ rv M" and g: "g ∈ rv M" 
  shows rv_times_rv: "(λw. f w * g w) ∈ rv M" 
proof -
  have "(λw. f w * g w) = (λw. (f w + g w)2/4 - (f w - g w)2/4)" 
    by (simp only: times_iff_sum_squares)
  also have "… = (λw. (f w + g w)2*inverse 4 - (f w + - g w)2*inverse 4)"  
    by simp
  also from f g have "… ∈ rv M" 
  proof -
    from f g have "(λw. (f w + g w)2)  ∈ rv M" 
      by (simp add: rv_plus_rv rv_square)
    hence "(λw. 0+(f w + g w)2*inverse 4) ∈ rv M" 
      by (rule affine_rv)
    also from g have "(λw. 0 + (g w)*-1 ) ∈ rv M" 
      by (rule affine_rv)
    with f have "(λw. (f w - g w)2)  ∈ rv M" 
      by (simp add: rv_plus_rv rv_square diff_conv_add_uminus del: add_uminus_conv_diff)
    hence "(λw. 0+(f w - g w)2*-inverse 4) ∈ rv M" 
      by (rule affine_rv)
    ultimately show ?thesis 
      by (simp add: rv_plus_rv diff_conv_add_uminus del: add_uminus_conv_diff)
  qed txt‹\nopagebreak›
  ultimately show ?thesis by simp
qed 
 
text‹The case of substraction is an easy consequence of ‹rv_plus_rv› and
  ‹rv_times_rv›.›
 
theorem rv_minus_rv:
  assumes f: "f ∈ rv M" and g: "g ∈ rv M"
  shows "(λt. f t - g t) ∈ rv M" 
(*<*)proof - 
  from f have ms: "measure_space M" by (simp add: rv_def)
  hence "(λt. -1) ∈ rv M" by (simp add: const_rv)
  from this g have "(λt. -1*g t) ∈ rv M" by (rule rv_times_rv)
  hence "(λt. -g t) ∈ rv M" by simp
  with f have "(λt. f t +-g t) ∈ rv M" by (rule rv_plus_rv)
  thus ?thesis by simp
qed(*>*)
text‹Measurability for limit functions of
    monotone convergent series is also surprisingly straightforward.›

theorem assumes u: "⋀n. u n ∈ rv M" and mon_conv: "u↑f"
  shows mon_conv_rv: "f ∈ rv M"
proof -
  from u have ms: "measure_space M" 
    by (simp add: rv_def)
  
  { 
    fix a 
    { 
      fix w
      from mon_conv have up: "(λn. u n w)↑f w" 
        by (simp only: realfun_mon_conv_iff)
      { 
        fix i
        from up have "u i w ≤ f w" 
          by (rule real_mon_conv_le)
        also assume "f w ≤ a"
        finally have  "u i w ≤ a" . 
      }                              
                                     
      also 
      { assume "⋀i. u i w ≤ a"
        also from up have "(λn. u n w) ⇢ f w" 
          by (simp only: mon_conv_real_def)
        ultimately have "f w ≤ a" 
          by (simp add: LIMSEQ_le_const2)
      }
      ultimately have "(f w ≤ a) = (∀i. u i w ≤ a)" by fast
    }
    hence "{w. f w ≤ a} = (⋂i. {w. u i w ≤ a})" by fast
    moreover
    from ms u have "⋀i. {w. u i w ≤ a} ∈ sigma(measurable_sets M)"
      by (simp add: rv_le_iff sigma.intros)
    hence "(⋂i. {w. u i w ≤ a}) ∈ sigma(measurable_sets M)" 
      by (rule sigma_Inter)
    with ms have "(⋂i. {w. u i w ≤ a}) ∈ measurable_sets M" 
      by (simp only: measure_space_def sigma_sigma_algebra)
    ultimately have "{w. f w ≤ a} ∈ measurable_sets M" by simp
  }
  with ms show ?thesis 
    by (simp add: rv_le_iff)
qed

text ‹Before we end this chapter to start the formalization of the
  integral proper, there is one more concept missing: The
  positive and negative part of a function. Their definition is quite intuitive,
  and some useful properties are given right away, including the fact
  that they are random variables, provided that their argument
  functions are measurable.›

definition
  nonnegative:: "('a ⇒ ('b::{ord,zero})) ⇒ bool" where
  "nonnegative f ⟷ (∀x. 0 ≤ f x)"

definition
  positive_part:: "('a ⇒ ('b::{ord,zero})) ⇒ ('a ⇒ 'b)" ("pp") where
  "pp f x = (if 0≤f(x) then f x else 0)"

definition
  negative_part:: "('a ⇒ ('b::{ord,zero,uminus,minus})) ⇒ ('a ⇒ 'b)" ("np") where
  "np f x = (if 0≤f(x) then 0 else -f(x))"
  (*useful lemmata about positive and negative parts*)
lemma f_plus_minus: "((f x)::real) = pp f x - np f x" 
  by (simp add:positive_part_def negative_part_def)

lemma f_plus_minus2: "(f::'a ⇒ real) = (λt. pp f t - np f t)"
  using f_plus_minus
  by (rule ext)

lemma f_abs_plus_minus: "(¦f x¦::real) = pp f x + np f x"
  by  (auto simp add:positive_part_def negative_part_def)

lemma nn_pp_np: assumes "nonnegative f"
  shows "pp f = f" and "np f = (λt. 0)" using assms
  by (auto simp add: positive_part_def negative_part_def nonnegative_def ext)

lemma pos_pp_np_help: "⋀x. 0≤f x ⟹ pp f x = f x ∧ np f x = 0"
  by (simp add: positive_part_def negative_part_def)

lemma real_neg_pp_np_help: "⋀x. f x ≤ (0::real) ⟹ np f x = -f x ∧ pp f x = 0"
(*<*)proof -
  fix x
  assume le: "f x ≤ 0"
  hence "pp f x = 0 " 
    by (cases "f x < 0") (auto simp add: positive_part_def)
  also from le have "np f x = -f x"
    by (cases "f x < 0") (auto simp add: negative_part_def)
  ultimately show "np f x = -f x ∧ pp f x = 0" by fast
qed(*>*)

lemma real_neg_pp_np: assumes "f ≤ (λt. (0::real))"
 shows "np f = (λt. -f t)" and "pp f = (λt. 0)" using assms
  by (auto simp add: real_neg_pp_np_help ext le_fun_def)

lemma assumes a: "0≤(a::real)" 
  shows real_pp_np_pos_times: 
  "pp (λt. a*f t) = (λt. a*pp f t) ∧  np (λt. a*f t) = (λt. a*np f t)"
(*<*)proof -
  { fix t
    have "pp (λt. a*f t) t = a*pp f t ∧ np (λt. a*f t) t = a*np f t"
    proof (cases "0 ≤ f t")
      case True
      from a this a order_refl[of 0] have le: "0*0≤a*f t" 
        by (rule mult_mono)
      hence "pp (λt. a*f t) t = a*f t" by (simp add: positive_part_def)
      also from True have "… = a*pp f t" by (simp add: positive_part_def)
      finally have 1: "pp (λt. a*f t) t = a*pp f t" .
      
      from le have "np (λt. a*f t) t = 0" by (simp add: negative_part_def)
      also from True have "… = a*np f t" by (simp add: negative_part_def)
      finally show ?thesis using 1 by fast
    next
      case False
      hence "f t ≤ 0" by simp
      from this a have "(f t)*a ≤ 0*a" by (rule mult_right_mono)
      hence le: "a*f t ≤ 0" by (simp add: mult.commute)
      hence "pp (λt. a*f t) t = 0" 
        by (cases "a*f t<0") (auto simp add: positive_part_def order_le_less ) 
      also from False have "… = a*pp f t" by (simp add: positive_part_def)
      finally have 1: "pp (λt. a*f t) t = a*pp f t" .
      
      from le have "np (λt. a*f t) t = -a*f t" 
        by (cases "a*f t=0") (auto simp add: negative_part_def order_le_less)
      also from False have "… = a*np f t" by (simp add: negative_part_def)
      finally show ?thesis using 1 by fast
    qed
  } thus ?thesis by (simp add: ext)
qed(*>*)

lemma assumes a: "(a::real)≤0" 
  shows real_pp_np_neg_times: 
  "pp (λt. a*f t) = (λt. -a*np f t) ∧  np (λt. a*f t) = (λt. -a*pp f t)"
(*<*)proof -
  { fix t
    have "pp (λt. a*f t) t = -a*np f t ∧ np (λt. a*f t) t = -a*pp f t"
    proof (cases "0 ≤ f t")
      case True 
      with a have le: "a*f t≤0*f t" 
        by (rule mult_right_mono)
      hence "pp (λt. a*f t) t = 0" by (simp add: real_neg_pp_np_help)
      also from True have "… = -a*np f t" by (simp add: negative_part_def)
      finally have 1: "pp (λt. a*f t) t = -a*np f t" .
      
      from le have "np (λt. a*f t) t = -a*f t" by (simp add: real_neg_pp_np_help)
      also from True have "… = -a*pp f t" by (simp add: positive_part_def)
      finally show ?thesis using 1 by fast
    next
      case False
      hence "f t ≤ 0" by simp 
      with a have le: "0≤a*(f t)" by (simp add: zero_le_mult_iff)
      hence "pp (λt. a*f t) t = a*f t" by (simp add: positive_part_def) 
      also from False have "… = -a*np f t" by (simp add: negative_part_def)
      finally have 1: "pp (λt. a*f t) t = -a*np f t" .
      
      from le have "np (λt. a*f t) t = 0" by (simp add: negative_part_def)
      also from False have "… = -a*pp f t" by (simp add: positive_part_def)
      finally show ?thesis using 1 by fast
    qed
  } thus ?thesis by (simp add: ext)
qed(*>*)


lemma pp_np_rv:
  assumes f: "f ∈ rv M" 
  shows "pp f ∈ rv M" and "np f ∈ rv M"
proof -
  from f have ms: "measure_space M" by (simp add: rv_def)
  
  { fix a
    from ms f have fm: "{w. f w ≤ a} ∈ measurable_sets M" 
      by (simp add: rv_le_iff)
    have 
      "{w. pp f w ≤ a} ∈ measurable_sets M ∧ 
      {w. np f w ≤ a} ∈ measurable_sets M"
    proof (cases "0≤a")
      case True
      hence "{w. pp f w ≤ a} = {w. f w ≤ a}" 
        by (auto simp add: positive_part_def)
      moreover note fm moreover
      from True have "{w. np f w ≤ a} = {w. -a ≤ f w}" 
        by (auto simp add: negative_part_def)
      moreover from ms f have "… ∈ measurable_sets M" 
        by (simp add: rv_ge_iff)
      ultimately show ?thesis by simp
    next
      case False
      hence "{w. pp f w ≤ a} = {}" 
        by (auto simp add: positive_part_def)
      also from False have "{w. np f w ≤ a} = {}" 
        by (auto simp add: negative_part_def)
      moreover from ms have "{} ∈ measurable_sets M" 
        by (simp add: measure_space_def sigma_algebra_def)
      ultimately show ?thesis by simp
    qed
  } with ms show "pp f ∈ rv M" and "np f ∈ rv M" 
    by (auto simp add: rv_le_iff)
qed


theorem pp_np_rv_iff: "(f::'a ⇒ real) ∈ rv M = (pp f ∈ rv M ∧ np f ∈ rv M)"
(*<*)proof -
  { assume "pp f ∈ rv M" and "np f ∈ rv M" 
    hence "(λt. pp f t - np f t) ∈ rv M" by (rule rv_minus_rv)
    also have "f = (λt. pp f t - np f t)" by (rule f_plus_minus2)
    ultimately have "f ∈ rv M" by simp
  } also
  have "f ∈ rv M ⟹ (pp f ∈ rv M ∧ np f ∈ rv M)" by (simp add: pp_np_rv)
  ultimately show ?thesis by fast
qed(*>*)


text‹This completes the chapter about measurable functions. As we
  will see in the next one, measurability is the prime condition on
  Lebesgue integrable functions; and the theorems and lemmata
  established here suffice --- at least in principle --- to show it holds for any
  function that is to be integrated there.›

end