Up to index of Isabelle/HOL/Integration
theory RealRandVarheader {*Real-Valued Random Variables*}
theory RealRandVar
imports Measure "~~/src/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 @{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 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) 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)
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) \<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" .
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 "(\<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 .
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 @{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 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} = (\<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 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)
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² ≤ 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 simp
qed(*>*)
lemma realpow_two_binomial_iff: "(f+g::real)² = f² + 2*(f*g) + g²"
(*<*)
by (simp add: power2_eq_square left_distrib right_distrib)(*>*)
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: real_diff_def)
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 real_diff_def)
qed txt{*\nopagebreak*}
ultimately show ?thesis by simp
qed
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: real_diff_def)
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)
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 real_le_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: real_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