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: "(a⇧^{2}≤ b⇧^{2}) = (¦a¦ ≤ ¦b::real¦)" (*<*)proof - have "(a⇧^{2}≤ b⇧^{2}) = (¦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 ∧ sqra⇧^{2}= 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}= f⇧^{2}+ 2*(f*g) + g⇧^{2}" (*<*) 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