# Theory RealRandVar

Up to index of Isabelle/HOL/Integration

theory RealRandVar
imports Measure Countable
header {*Real-Valued Random Variables*}theory RealRandVarimports Measure "~~/src/HOL/Library/Countable"begintext {*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 SebastianSkalberg'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 @{text "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 @{text "±∞"} --- 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" ("\<bool>") where  "\<bool> = 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) \<bool>}"text {* As explained in the first paragraph, the preceding  definitions\footnote{The notation $@{text"{..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 $@{text \<real>}^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 righttime 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) o (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)qedtext {* 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) blastqed(*>*)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) \<bool>"      hence "∀b∈\<bool>. f - b ∈ measurable_sets M"        by (unfold measurable_def) blast      also have "{..a} ∈ \<bool>"         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) \<bool>"       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 @{text "<"}, @{text ">"} and @{text "≥"} 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 "(\<Union>n::nat. {w. f w ≤ a - inverse (real (Suc n))}) ∈ A"     by (simp add: sigma_algebra_def)   also  have "(\<Union>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: LIMSEQ_def 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" .qedlemma 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" .qedlemma 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 "(\<Union>n::nat. {w. a + inverse (real (Suc n)) ≤ f w}) ∈ A"     by (simp add: sigma_algebra_def)   also  have "(\<Union>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: LIMSEQ_def 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 .qedtheorem 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 simpnext  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 @{text "{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 usethe 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} = (\<Union>i. ?I i)"  proof    { fix w assume "w ∈ {w. f w < g w}"      hence "f w < g w" ..      hence "∃s∈\<rat>. f w < s ∧ s < g w" by (rule Rats_dense_in_real)      hence "∃s∈\<rat>. 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 ∈ (\<Union>i. ?I i)" by simp    }    thus "{w. f w < g w} ⊆ (\<Union>i. ?I i)" ..        show "(\<Union>i. ?I i) ⊆ {w. f w < g w}" by (force simp add: Let_def)  qed  moreover have "(\<Union>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 simpqed(*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 autotxt{*\nopagebreak*}    finally show ?thesis .qedlemma 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)qedtext {*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: "(a² ≤ b²) = (¦a¦ ≤ ¦b::real¦)"(*<*)proof -  have "(a² ≤ b²) = (¦a¦² ≤ ¦b¦²)" by (simp add: numeral_2_eq_2)  also have "… = (¦a¦ ≤ ¦b¦)"   proof    assume "¦a¦ ≤ ¦b¦"    thus "¦a¦² ≤ ¦b¦²"      by (rule power_mono) simp  next    assume "¦a¦² ≤ ¦b¦²" 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)²) ∈ rv M"(*<*)proof -  from f have ms: "measure_space M" by (simp add: rv_def)  hence "?thesis = (∀a. {w. (f w)² ≤ 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)²" by simp        finally have "((f w)² ≤ 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)²" by simp          hence "((f w)² ≤ 0) ==> ((f w)² = 0)" by (simp only: order_antisym)          hence "((f w)² ≤ 0) = ((f w)² = 0)" by (force simp add: numeral_2_eq_2)          also have "… = (f w = 0)" by simp               finally have "((f w)² ≤ 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 ∧ sqra² = 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 (auto simp only: pow2_le_abs abs_le_interval_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 simpqed(*>*)lemma realpow_two_binomial_iff: "(f+g::real)² = f² + 2*(f*g) + g²"  (*<*)   by (simp add: power2_eq_square distrib_right distrib_left)(*>*) lemma times_iff_sum_squares: "f*g = (f+g)²/4 - (f-g)²/(4::real)"(*<*)proof -  have a: "f-g = f+(-g)" by simp  hence "(f+g)²/4 - (f-g)²/4 = ((f+g)² + - (f+(-g))²)/4"     by (simp add: add_divide_distrib[THEN sym] a)  also have "… = f*g"     by (simp add: realpow_two_binomial_iff)   finally show ?thesis by (rule sym)qed(*>*)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)²/4 - (f w - g w)²/4)"     by (simp only: times_iff_sum_squares)  also have "… = (λw. (f w + g w)²*inverse 4 - (f w + - g w)²*inverse 4)"      by (simp add: diff_minus)  also from f g have "… ∈ rv M"   proof -    from f g have "(λw. (f w + g w)²)  ∈ rv M"       by (simp add: rv_plus_rv rv_square)    hence "(λw. 0+(f w + g w)²*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)²)  ∈ rv M"       by (simp add: rv_plus_rv rv_square)    hence "(λw. 0+(f w + - g w)²*-inverse 4) ∈ rv M"       by (rule affine_rv)    ultimately show ?thesis       by (simp add: rv_plus_rv diff_minus)  qed txt{*\nopagebreak*}  ultimately show ?thesis by simpqed  text{*The case of substraction is an easy consequence of @{text rv_plus_rv} and  @{text 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 add: diff_minus)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\<up>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)\<up>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: real_mon_conv)        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} = (\<Inter>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 "(\<Inter>i. {w. u i w ≤ a}) ∈ sigma(measurable_sets M)"       by (rule sigma_Inter)    with ms have "(\<Inter>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)qedtext {* 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 fastqed(*>*)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)qedtheorem 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 fastqed(*>*)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`