Theory HOL-Probability.Conditional_Expectation
section ‹Conditional Expectation›
theory Conditional_Expectation
imports Probability_Measure
begin
subsection ‹Restricting a measure to a sub-sigma-algebra›
definition subalgebra::"'a measure ⇒ 'a measure ⇒ bool" where
"subalgebra M F = ((space F = space M) ∧ (sets F ⊆ sets M))"
lemma sub_measure_space:
assumes i: "subalgebra M F"
shows "measure_space (space M) (sets F) (emeasure M)"
proof -
have "sigma_algebra (space M) (sets F)"
by (metis i measure_space measure_space_def subalgebra_def)
moreover have "positive (sets F) (emeasure M)"
using Sigma_Algebra.positive_def by auto
moreover have "countably_additive (sets F) (emeasure M)"
by (meson countably_additive_def emeasure_countably_additive i order_trans subalgebra_def subsetCE)
ultimately show ?thesis unfolding measure_space_def by simp
qed
definition restr_to_subalg::"'a measure ⇒ 'a measure ⇒ 'a measure" where
"restr_to_subalg M F = measure_of (space M) (sets F) (emeasure M)"
lemma space_restr_to_subalg:
"space (restr_to_subalg M F) = space M"
unfolding restr_to_subalg_def by (simp add: space_measure_of_conv)
lemma sets_restr_to_subalg [measurable_cong]:
assumes "subalgebra M F"
shows "sets (restr_to_subalg M F) = sets F"
unfolding restr_to_subalg_def by (metis sets.sets_measure_of_eq assms subalgebra_def)
lemma emeasure_restr_to_subalg:
assumes "subalgebra M F"
"A ∈ sets F"
shows "emeasure (restr_to_subalg M F) A = emeasure M A"
unfolding restr_to_subalg_def
by (metis assms subalgebra_def emeasure_measure_of_conv sub_measure_space sets.sigma_sets_eq)
lemma null_sets_restr_to_subalg:
assumes "subalgebra M F"
shows "null_sets (restr_to_subalg M F) = null_sets M ∩ sets F"
proof
have "x ∈ null_sets M ∩ sets F" if "x ∈ null_sets (restr_to_subalg M F)" for x
by (metis that Int_iff assms emeasure_restr_to_subalg null_setsD1 null_setsD2 null_setsI
sets_restr_to_subalg subalgebra_def subsetD)
then show "null_sets (restr_to_subalg M F) ⊆ null_sets M ∩ sets F" by auto
next
have "x ∈ null_sets (restr_to_subalg M F)" if "x ∈ null_sets M ∩ sets F" for x
by (metis that Int_iff assms null_setsD1 null_setsI sets_restr_to_subalg emeasure_restr_to_subalg[OF assms])
then show "null_sets M ∩ sets F ⊆ null_sets (restr_to_subalg M F)" by auto
qed
lemma AE_restr_to_subalg:
assumes "subalgebra M F"
"AE x in (restr_to_subalg M F). P x"
shows "AE x in M. P x"
proof -
obtain A where A: "⋀x. x ∈ space (restr_to_subalg M F) - A ⟹ P x" "A ∈ null_sets (restr_to_subalg M F)"
using AE_E3[OF assms(2)] by auto
then have "A ∈ null_sets M" using null_sets_restr_to_subalg[OF assms(1)] by auto
moreover have "⋀x. x ∈ space M - A ⟹ P x"
using space_restr_to_subalg A(1) by fastforce
ultimately show ?thesis
unfolding eventually_ae_filter by auto
qed
lemma AE_restr_to_subalg2:
assumes "subalgebra M F"
"AE x in M. P x" and [measurable]: "P ∈ measurable F (count_space UNIV)"
shows "AE x in (restr_to_subalg M F). P x"
proof -
define U where "U = {x ∈ space M. ¬(P x)}"
then have *: "U = {x ∈ space F. ¬(P x)}" using assms(1) by (simp add: subalgebra_def)
then have "U ∈ sets F" by simp
then have "U ∈ sets M" using assms(1) by (meson subalgebra_def subsetD)
then have "U ∈ null_sets M" unfolding U_def using assms(2) using AE_iff_measurable by blast
then have "U ∈ null_sets (restr_to_subalg M F)" using null_sets_restr_to_subalg[OF assms(1)] ‹U ∈ sets F› by auto
then show ?thesis using * by (metis (no_types, lifting) Collect_mono U_def eventually_ae_filter space_restr_to_subalg)
qed
lemma prob_space_restr_to_subalg:
assumes "subalgebra M F"
"prob_space M"
shows "prob_space (restr_to_subalg M F)"
by (metis (no_types, lifting) assms(1) assms(2) emeasure_restr_to_subalg prob_space.emeasure_space_1 prob_spaceI
sets.top space_restr_to_subalg subalgebra_def)
lemma finite_measure_restr_to_subalg:
assumes "subalgebra M F"
"finite_measure M"
shows "finite_measure (restr_to_subalg M F)"
by (metis (no_types, lifting) assms emeasure_restr_to_subalg finite_measure.finite_emeasure_space
finite_measureI sets.top space_restr_to_subalg subalgebra_def infinity_ennreal_def)
lemma measurable_in_subalg:
assumes "subalgebra M F"
"f ∈ measurable F N"
shows "f ∈ measurable (restr_to_subalg M F) N"
by (metis measurable_cong_sets assms(2) sets_restr_to_subalg[OF assms(1)])
lemma measurable_in_subalg':
assumes "subalgebra M F"
"f ∈ measurable (restr_to_subalg M F) N"
shows "f ∈ measurable F N"
by (metis measurable_cong_sets assms(2) sets_restr_to_subalg[OF assms(1)])
lemma measurable_from_subalg:
assumes "subalgebra M F"
"f ∈ measurable F N"
shows "f ∈ measurable M N"
using assms unfolding measurable_def subalgebra_def by auto
text‹The following is the direct transposition of \verb+nn_integral_subalgebra+
(from \verb+Nonnegative_Lebesgue_Integration+) in the
current notations, with the removal of the useless assumption $f \geq 0$.›
lemma nn_integral_subalgebra2:
assumes "subalgebra M F" and [measurable]: "f ∈ borel_measurable F"
shows "(∫⇧+ x. f x ∂(restr_to_subalg M F)) = (∫⇧+ x. f x ∂M)"
proof (rule nn_integral_subalgebra)
show "f ∈ borel_measurable (restr_to_subalg M F)"
by (rule measurable_in_subalg[OF assms(1)]) simp
show "sets (restr_to_subalg M F) ⊆ sets M" by (metis sets_restr_to_subalg[OF assms(1)] assms(1) subalgebra_def)
fix A assume "A ∈ sets (restr_to_subalg M F)"
then show "emeasure (restr_to_subalg M F) A = emeasure M A"
by (metis sets_restr_to_subalg[OF assms(1)] emeasure_restr_to_subalg[OF assms(1)])
qed (auto simp add: assms space_restr_to_subalg sets_restr_to_subalg[OF assms(1)])
text‹The following is the direct transposition of \verb+integral_subalgebra+
(from \verb+Bochner_Integration+) in the current notations.›
lemma integral_subalgebra2:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
assumes "subalgebra M F" and
[measurable]: "f ∈ borel_measurable F"
shows "(∫x. f x ∂(restr_to_subalg M F)) = (∫x. f x ∂M)"
by (rule integral_subalgebra,
metis measurable_in_subalg[OF assms(1)] assms(2),
auto simp add: assms space_restr_to_subalg sets_restr_to_subalg emeasure_restr_to_subalg,
meson assms(1) subalgebra_def subset_eq)
lemma integrable_from_subalg:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
assumes "subalgebra M F"
"integrable (restr_to_subalg M F) f"
shows "integrable M f"
proof (rule integrableI_bounded)
have [measurable]: "f ∈ borel_measurable F" using assms by auto
then show "f ∈ borel_measurable M" using assms(1) measurable_from_subalg by blast
have "(∫⇧+ x. ennreal (norm (f x)) ∂M) = (∫⇧+ x. ennreal (norm (f x)) ∂(restr_to_subalg M F))"
by (rule nn_integral_subalgebra2[symmetric], auto simp add: assms)
also have "... < ∞" using integrable_iff_bounded assms by auto
finally show "(∫⇧+ x. ennreal (norm (f x)) ∂M) < ∞" by simp
qed
lemma integrable_in_subalg:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
assumes [measurable]: "subalgebra M F"
"f ∈ borel_measurable F"
"integrable M f"
shows "integrable (restr_to_subalg M F) f"
proof (rule integrableI_bounded)
show "f ∈ borel_measurable (restr_to_subalg M F)" using assms(2) assms(1) by auto
have "(∫⇧+ x. ennreal (norm (f x)) ∂(restr_to_subalg M F)) = (∫⇧+ x. ennreal (norm (f x)) ∂M)"
by (rule nn_integral_subalgebra2, auto simp add: assms)
also have "... < ∞" using integrable_iff_bounded assms by auto
finally show "(∫⇧+ x. ennreal (norm (f x)) ∂(restr_to_subalg M F)) < ∞" by simp
qed
subsection ‹Nonnegative conditional expectation›
text ‹The conditional expectation of a function $f$, on a measure space $M$, with respect to a
sub sigma algebra $F$, should be a function $g$ which is $F$-measurable whose integral on any
$F$-set coincides with the integral of $f$.
Such a function is uniquely defined almost everywhere.
The most direct construction is to use the measure $f dM$, restrict it to the sigma-algebra $F$,
and apply the Radon-Nikodym theorem to write it as $g dM_{|F}$ for some $F$-measurable function $g$.
Another classical construction for $L^2$ functions is done by orthogonal projection on $F$-measurable
functions, and then extending by density to $L^1$. The Radon-Nikodym point of view avoids the $L^2$
machinery, and works for all positive functions.
In this paragraph, we develop the definition and basic properties for nonnegative functions,
as the basics of the general case. As in the definition of integrals, the nonnegative case is done
with ennreal-valued functions, without any integrability assumption.
›
definition nn_cond_exp :: "'a measure ⇒ 'a measure ⇒ ('a ⇒ ennreal) ⇒ ('a ⇒ ennreal)"
where
"nn_cond_exp M F f =
(if f ∈ borel_measurable M ∧ subalgebra M F
then RN_deriv (restr_to_subalg M F) (restr_to_subalg (density M f) F)
else (λ_. 0))"
lemma
shows borel_measurable_nn_cond_exp [measurable]: "nn_cond_exp M F f ∈ borel_measurable F"
and borel_measurable_nn_cond_exp2 [measurable]: "nn_cond_exp M F f ∈ borel_measurable M"
by (simp_all add: nn_cond_exp_def)
(metis borel_measurable_RN_deriv borel_measurable_subalgebra sets_restr_to_subalg space_restr_to_subalg subalgebra_def)
text ‹The good setting for conditional expectations is the situation where the subalgebra $F$
gives rise to a sigma-finite measure space. To see what goes wrong if it is not sigma-finite,
think of $\mathbb{R}$ with the trivial sigma-algebra $\{\emptyset, \mathbb{R}\}$. In this case,
conditional expectations have to be constant functions, so they have integral $0$ or $\infty$.
This means that a positive integrable function can have no meaningful conditional expectation.›
locale sigma_finite_subalgebra =
fixes M F::"'a measure"
assumes subalg: "subalgebra M F"
and sigma_fin_subalg: "sigma_finite_measure (restr_to_subalg M F)"
lemma sigma_finite_subalgebra_is_sigma_finite:
assumes "sigma_finite_subalgebra M F"
shows "sigma_finite_measure M"
proof
have subalg: "subalgebra M F"
and sigma_fin_subalg: "sigma_finite_measure (restr_to_subalg M F)"
using assms unfolding sigma_finite_subalgebra_def by auto
obtain A where Ap: "countable A ∧ A ⊆ sets (restr_to_subalg M F) ∧ ⋃A = space (restr_to_subalg M F) ∧ (∀a∈A. emeasure (restr_to_subalg M F) a ≠ ∞)"
using sigma_finite_measure.sigma_finite_countable[OF sigma_fin_subalg] by fastforce
have "A ⊆ sets F" using Ap sets_restr_to_subalg[OF subalg] by fastforce
then have "A ⊆ sets M" using subalg subalgebra_def by force
moreover have "⋃A = space M" using Ap space_restr_to_subalg by simp
moreover have "∀a∈A. emeasure M a ≠ ∞" by (metis subsetD emeasure_restr_to_subalg[OF subalg] ‹A ⊆ sets F› Ap)
ultimately show "∃A. countable A ∧ A ⊆ sets M ∧ ⋃A = space M ∧ (∀a∈A. emeasure M a ≠ ∞)" using Ap by auto
qed
sublocale sigma_finite_subalgebra ⊆ sigma_finite_measure
using sigma_finite_subalgebra_is_sigma_finite sigma_finite_subalgebra_axioms by blast
text ‹Conditional expectations are very often used in probability spaces. This is a special case
of the previous one, as we prove now.›
locale finite_measure_subalgebra = finite_measure +
fixes F::"'a measure"
assumes subalg: "subalgebra M F"
lemma finite_measure_subalgebra_is_sigma_finite:
assumes "finite_measure_subalgebra M F"
shows "sigma_finite_subalgebra M F"
proof -
interpret finite_measure_subalgebra M F using assms by simp
have "finite_measure (restr_to_subalg M F)"
using finite_measure_restr_to_subalg subalg finite_emeasure_space finite_measureI unfolding infinity_ennreal_def by blast
then have "sigma_finite_measure (restr_to_subalg M F)"
unfolding finite_measure_def by simp
then show "sigma_finite_subalgebra M F" unfolding sigma_finite_subalgebra_def using subalg by simp
qed
sublocale finite_measure_subalgebra ⊆ sigma_finite_subalgebra
proof -
have "finite_measure (restr_to_subalg M F)"
using finite_measure_restr_to_subalg subalg finite_emeasure_space finite_measureI unfolding infinity_ennreal_def by blast
then have "sigma_finite_measure (restr_to_subalg M F)"
unfolding finite_measure_def by simp
then show "sigma_finite_subalgebra M F" unfolding sigma_finite_subalgebra_def using subalg by simp
qed
context sigma_finite_subalgebra
begin
text‹The next lemma is arguably the most fundamental property of conditional expectation:
when computing an expectation against an $F$-measurable function, it is equivalent to work
with a function or with its $F$-conditional expectation.
This property (even for bounded test functions) characterizes conditional expectations, as the second lemma below shows.
From this point on, we will only work with it, and forget completely about
the definition using Radon-Nikodym derivatives.
›
lemma nn_cond_exp_intg:
assumes [measurable]: "f ∈ borel_measurable F" "g ∈ borel_measurable M"
shows "(∫⇧+ x. f x * nn_cond_exp M F g x ∂M) = (∫⇧+ x. f x * g x ∂M)"
proof -
have [measurable]: "f ∈ borel_measurable M"
by (meson assms subalg borel_measurable_subalgebra subalgebra_def)
have ac: "absolutely_continuous (restr_to_subalg M F) (restr_to_subalg (density M g) F)"
unfolding absolutely_continuous_def
proof -
have "null_sets (restr_to_subalg M F) = null_sets M ∩ sets F" by (rule null_sets_restr_to_subalg[OF subalg])
moreover have "null_sets M ⊆ null_sets (density M g)"
by (rule absolutely_continuousI_density[unfolded absolutely_continuous_def]) auto
ultimately have "null_sets (restr_to_subalg M F) ⊆ null_sets (density M g) ∩ sets F" by auto
moreover have "null_sets (density M g) ∩ sets F = null_sets (restr_to_subalg (density M g) F)"
by (rule null_sets_restr_to_subalg[symmetric]) (metis subalg sets_density space_density subalgebra_def)
ultimately show "null_sets (restr_to_subalg M F) ⊆ null_sets (restr_to_subalg (density M g) F)" by auto
qed
have "(∫⇧+ x. f x * nn_cond_exp M F g x ∂M) = (∫⇧+ x. f x * nn_cond_exp M F g x ∂(restr_to_subalg M F))"
by (rule nn_integral_subalgebra2[symmetric]) (simp_all add: assms subalg)
also have "... = (∫⇧+ x. f x * RN_deriv (restr_to_subalg M F) (restr_to_subalg (density M g) F) x ∂(restr_to_subalg M F))"
unfolding nn_cond_exp_def using assms subalg by simp
also have "... = (∫⇧+ x. RN_deriv (restr_to_subalg M F) (restr_to_subalg (density M g) F) x * f x ∂(restr_to_subalg M F))"
by (simp add: mult.commute)
also have "... = (∫⇧+ x. f x ∂(restr_to_subalg (density M g) F))"
proof (rule sigma_finite_measure.RN_deriv_nn_integral[symmetric])
show "sets (restr_to_subalg (density M g) F) = sets (restr_to_subalg M F)"
by (metis subalg restr_to_subalg_def sets.sets_measure_of_eq space_density subalgebra_def)
qed (auto simp add: assms measurable_restrict ac measurable_in_subalg subalg sigma_fin_subalg)
also have "... = (∫⇧+ x. f x ∂(density M g))"
by (metis nn_integral_subalgebra2 subalg assms(1) sets_density space_density subalgebra_def)
also have "... = (∫⇧+ x. g x * f x ∂M)"
by (rule nn_integral_density) (simp_all add: assms)
also have "... = (∫⇧+ x. f x * g x ∂M)"
by (simp add: mult.commute)
finally show ?thesis by simp
qed
lemma nn_cond_exp_charact:
assumes "⋀A. A ∈ sets F ⟹ (∫⇧+ x ∈ A. f x ∂M) = (∫⇧+ x ∈ A. g x ∂M)" and
[measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable F"
shows "AE x in M. g x = nn_cond_exp M F f x"
proof -
let ?MF = "restr_to_subalg M F"
{
fix A assume "A ∈ sets ?MF"
then have [measurable]: "A ∈ sets F" using sets_restr_to_subalg[OF subalg] by simp
have "(∫⇧+ x ∈ A. g x ∂ ?MF) = (∫⇧+ x ∈ A. g x ∂M)"
by (simp add: nn_integral_subalgebra2 subalg)
also have "... = (∫⇧+ x ∈ A. f x ∂M)" using assms(1) by simp
also have "... = (∫⇧+ x. indicator A x * f x ∂M)" by (simp add: mult.commute)
also have "... = (∫⇧+ x. indicator A x * nn_cond_exp M F f x ∂M)"
by (rule nn_cond_exp_intg[symmetric]) (auto simp add: assms)
also have "... = (∫⇧+ x ∈ A. nn_cond_exp M F f x ∂M)" by (simp add: mult.commute)
also have "... = (∫⇧+ x ∈ A. nn_cond_exp M F f x ∂ ?MF)"
by (simp add: nn_integral_subalgebra2 subalg)
finally have "(∫⇧+ x ∈ A. g x ∂ ?MF) = (∫⇧+ x ∈ A. nn_cond_exp M F f x ∂ ?MF)" by simp
} note * = this
have "AE x in ?MF. g x = nn_cond_exp M F f x"
by (rule sigma_finite_measure.density_unique2)
(auto simp add: assms subalg sigma_fin_subalg AE_restr_to_subalg2 *)
then show ?thesis using AE_restr_to_subalg[OF subalg] by simp
qed
lemma nn_cond_exp_F_meas:
assumes "f ∈ borel_measurable F"
shows "AE x in M. f x = nn_cond_exp M F f x"
by (rule nn_cond_exp_charact) (auto simp add: assms measurable_from_subalg[OF subalg])
lemma nn_cond_exp_prod:
assumes [measurable]: "f ∈ borel_measurable F" "g ∈ borel_measurable M"
shows "AE x in M. f x * nn_cond_exp M F g x = nn_cond_exp M F (λx. f x * g x) x"
proof (rule nn_cond_exp_charact)
have [measurable]: "f ∈ borel_measurable M" by (rule measurable_from_subalg[OF subalg assms(1)])
show "(λx. f x * g x) ∈ borel_measurable M" by measurable
fix A assume "A ∈ sets F"
then have [measurable]: "(λx. f x * indicator A x) ∈ borel_measurable F" by measurable
have "(∫⇧+x∈A. (f x * g x) ∂M) = ∫⇧+x. (f x * indicator A x) * g x ∂M"
by (simp add: mult.commute mult.left_commute)
also have "... = ∫⇧+x. (f x * indicator A x) * nn_cond_exp M F g x ∂M"
by (rule nn_cond_exp_intg[symmetric]) (auto simp add: assms)
also have "... = (∫⇧+x∈A. (f x * nn_cond_exp M F g x)∂M)"
by (simp add: mult.commute mult.left_commute)
finally show "(∫⇧+x∈A. (f x * g x) ∂M) = (∫⇧+x∈A. (f x * nn_cond_exp M F g x)∂M)" by simp
qed (auto simp add: assms)
lemma nn_cond_exp_sum:
assumes [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable M"
shows "AE x in M. nn_cond_exp M F f x + nn_cond_exp M F g x = nn_cond_exp M F (λx. f x + g x) x"
proof (rule nn_cond_exp_charact)
fix A assume [measurable]: "A ∈ sets F"
then have "A ∈ sets M" by (meson subalg subalgebra_def subsetD)
have "(∫⇧+x∈A. (nn_cond_exp M F f x + nn_cond_exp M F g x)∂M) = (∫⇧+x∈A. nn_cond_exp M F f x ∂M) + (∫⇧+x∈A. nn_cond_exp M F g x ∂M)"
by (rule nn_set_integral_add) (auto simp add: assms ‹A ∈ sets M›)
also have "... = (∫⇧+x. indicator A x * nn_cond_exp M F f x ∂M) + (∫⇧+x. indicator A x * nn_cond_exp M F g x ∂M)"
by (metis (no_types, lifting) mult.commute nn_integral_cong)
also have "... = (∫⇧+x. indicator A x * f x ∂M) + (∫⇧+x. indicator A x * g x ∂M)"
by (simp add: nn_cond_exp_intg)
also have "... = (∫⇧+x∈A. f x ∂M) + (∫⇧+x∈A. g x ∂M)"
by (metis (no_types, lifting) mult.commute nn_integral_cong)
also have "... = (∫⇧+x∈A. (f x + g x)∂M)"
by (rule nn_set_integral_add[symmetric]) (auto simp add: assms ‹A ∈ sets M›)
finally show "(∫⇧+x∈A. (f x + g x)∂M) = (∫⇧+x∈A. (nn_cond_exp M F f x + nn_cond_exp M F g x)∂M)"
by simp
qed (auto simp add: assms)
lemma nn_cond_exp_cong:
assumes "AE x in M. f x = g x"
and [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable M"
shows "AE x in M. nn_cond_exp M F f x = nn_cond_exp M F g x"
proof (rule nn_cond_exp_charact)
fix A assume [measurable]: "A ∈ sets F"
have "(∫⇧+x∈A. nn_cond_exp M F f x ∂M) = ∫⇧+x. indicator A x * nn_cond_exp M F f x ∂M"
by (simp add: mult.commute)
also have "... = ∫⇧+x. indicator A x * f x ∂M" by (simp add: nn_cond_exp_intg assms)
also have "... = (∫⇧+x∈A. f x ∂M)" by (simp add: mult.commute)
also have "... = (∫⇧+x∈A. g x ∂M)" by (rule nn_set_integral_cong[OF assms(1)])
finally show "(∫⇧+x∈A. g x ∂M) = (∫⇧+x∈A. nn_cond_exp M F f x ∂M)" by simp
qed (auto simp add: assms)
lemma nn_cond_exp_mono:
assumes "AE x in M. f x ≤ g x"
and [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable M"
shows "AE x in M. nn_cond_exp M F f x ≤ nn_cond_exp M F g x"
proof -
define h where "h = (λx. g x - f x)"
have [measurable]: "h ∈ borel_measurable M" unfolding h_def by simp
have *: "AE x in M. g x = f x + h x" unfolding h_def using assms(1) by (auto simp: ennreal_ineq_diff_add)
have "AE x in M. nn_cond_exp M F g x = nn_cond_exp M F (λx. f x + h x) x"
by (rule nn_cond_exp_cong) (auto simp add: * assms)
moreover have "AE x in M. nn_cond_exp M F f x + nn_cond_exp M F h x = nn_cond_exp M F (λx. f x + h x) x"
by (rule nn_cond_exp_sum) (auto simp add: assms)
ultimately have "AE x in M. nn_cond_exp M F g x = nn_cond_exp M F f x + nn_cond_exp M F h x" by auto
then show ?thesis by force
qed
lemma nested_subalg_is_sigma_finite:
assumes "subalgebra M G" "subalgebra G F"
shows "sigma_finite_subalgebra M G"
unfolding sigma_finite_subalgebra_def
proof (auto simp add: assms)
have "∃A. countable A ∧ A ⊆ sets (restr_to_subalg M F) ∧ ⋃A = space (restr_to_subalg M F) ∧ (∀a∈A. emeasure (restr_to_subalg M F) a ≠ ∞)"
using sigma_fin_subalg sigma_finite_measure_def by auto
then obtain A where A:"countable A ∧ A ⊆ sets (restr_to_subalg M F) ∧ ⋃A = space (restr_to_subalg M F) ∧ (∀a∈A. emeasure (restr_to_subalg M F) a ≠ ∞)"
by auto
have "sets F ⊆ sets M"
by (meson assms order_trans subalgebra_def)
then have "countable A ∧ A ⊆ sets (restr_to_subalg M G) ∧ ⋃A = space (restr_to_subalg M F) ∧ (∀a∈A. emeasure (restr_to_subalg M G) a ≠ ∞)"
by (metis (no_types) A assms basic_trans_rules(31) emeasure_restr_to_subalg order_trans sets_restr_to_subalg subalgebra_def)
then show "sigma_finite_measure (restr_to_subalg M G)"
by (metis sigma_finite_measure.intro space_restr_to_subalg)
qed
lemma nn_cond_exp_nested_subalg:
assumes "subalgebra M G" "subalgebra G F"
and [measurable]: "f ∈ borel_measurable M"
shows "AE x in M. nn_cond_exp M F f x = nn_cond_exp M F (nn_cond_exp M G f) x"
proof (rule nn_cond_exp_charact, auto)
interpret G: sigma_finite_subalgebra M G by (rule nested_subalg_is_sigma_finite[OF assms(1) assms(2)])
fix A assume [measurable]: "A ∈ sets F"
then have [measurable]: "A ∈ sets G" using assms(2) by (meson subsetD subalgebra_def)
have "set_nn_integral M A (nn_cond_exp M G f) = (∫⇧+ x. indicator A x * nn_cond_exp M G f x∂M)"
by (metis (no_types) mult.commute)
also have "... = (∫⇧+ x. indicator A x * f x ∂M)" by (rule G.nn_cond_exp_intg, auto simp add: assms)
also have "... = (∫⇧+ x. indicator A x * nn_cond_exp M F f x ∂M)" by (rule nn_cond_exp_intg[symmetric], auto simp add: assms)
also have "... = set_nn_integral M A (nn_cond_exp M F f)" by (metis (no_types) mult.commute)
finally show "set_nn_integral M A (nn_cond_exp M G f) = set_nn_integral M A (nn_cond_exp M F f)".
qed
end
subsection ‹Real conditional expectation›
text ‹Once conditional expectations of positive functions are defined, the definition for real-valued functions
follows readily, by taking the difference of positive and negative parts.
One could also define a conditional expectation of vector-space valued functions, as in
\verb+Bochner_Integral+, but since the real-valued case is the most important, and quicker to formalize, I
concentrate on it. (It is also essential for the case of the most general Pettis integral.)
›
definition real_cond_exp :: "'a measure ⇒ 'a measure ⇒ ('a ⇒ real) ⇒ ('a ⇒ real)" where
"real_cond_exp M F f =
(λx. enn2real(nn_cond_exp M F (λx. ennreal (f x)) x) - enn2real(nn_cond_exp M F (λx. ennreal (-f x)) x))"
lemma
shows borel_measurable_cond_exp [measurable]: "real_cond_exp M F f ∈ borel_measurable F"
and borel_measurable_cond_exp2 [measurable]: "real_cond_exp M F f ∈ borel_measurable M"
unfolding real_cond_exp_def by auto
context sigma_finite_subalgebra
begin
lemma real_cond_exp_abs:
assumes [measurable]: "f ∈ borel_measurable M"
shows "AE x in M. abs(real_cond_exp M F f x) ≤ nn_cond_exp M F (λx. ennreal (abs(f x))) x"
proof -
define fp where "fp = (λx. ennreal (f x))"
define fm where "fm = (λx. ennreal (- f x))"
have [measurable]: "fp ∈ borel_measurable M" "fm ∈ borel_measurable M" unfolding fp_def fm_def by auto
have eq: "⋀x. ennreal ¦f x¦ = fp x + fm x" unfolding fp_def fm_def by (simp add: abs_real_def ennreal_neg)
{
fix x assume H: "nn_cond_exp M F fp x + nn_cond_exp M F fm x = nn_cond_exp M F (λx. fp x + fm x) x"
have "¦real_cond_exp M F f x¦ ≤ ¦enn2real(nn_cond_exp M F fp x)¦ + ¦enn2real(nn_cond_exp M F fm x)¦"
unfolding real_cond_exp_def fp_def fm_def by (auto intro: abs_triangle_ineq4 simp del: enn2real_nonneg)
from ennreal_leI[OF this]
have "abs(real_cond_exp M F f x) ≤ nn_cond_exp M F fp x + nn_cond_exp M F fm x"
by simp (metis add.commute ennreal_enn2real le_iff_add not_le top_unique)
also have "... = nn_cond_exp M F (λx. fp x + fm x) x" using H by simp
finally have "abs(real_cond_exp M F f x) ≤ nn_cond_exp M F (λx. fp x + fm x) x" by simp
}
moreover have "AE x in M. nn_cond_exp M F fp x + nn_cond_exp M F fm x = nn_cond_exp M F (λx. fp x + fm x) x"
by (rule nn_cond_exp_sum) (auto simp add: fp_def fm_def)
ultimately have "AE x in M. abs(real_cond_exp M F f x) ≤ nn_cond_exp M F (λx. fp x + fm x) x"
by auto
then show ?thesis using eq by simp
qed
text‹The next lemma shows that the conditional expectation
is an $F$-measurable function whose average against an $F$-measurable
function $f$ coincides with the average of the original function against $f$.
It is obtained as a consequence of the same property for the positive conditional
expectation, taking the difference of the positive and the negative part. The proof
is given first assuming $f \geq 0$ for simplicity, and then extended to the general case in
the subsequent lemma. The idea of the proof is essentially trivial, but the implementation
is slightly tedious as one should check all the integrability properties of the different parts, and go
back and forth between positive integral and signed integrals, and between real-valued
functions and ennreal-valued functions.
Once this lemma is available, we will use it to characterize the conditional expectation,
and never come back to the original technical definition, as we did in the case of the
nonnegative conditional expectation.
›
lemma real_cond_exp_intg_fpos:
assumes "integrable M (λx. f x * g x)" and f_pos[simp]: "⋀x. f x ≥ 0" and
[measurable]: "f ∈ borel_measurable F" "g ∈ borel_measurable M"
shows "integrable M (λx. f x * real_cond_exp M F g x)"
"(∫ x. f x * real_cond_exp M F g x ∂M) = (∫ x. f x * g x ∂M)"
proof -
have [measurable]: "f ∈ borel_measurable M" by (rule measurable_from_subalg[OF subalg assms(3)])
define gp where "gp = (λx. ennreal (g x))"
define gm where "gm = (λx. ennreal (- g x))"
have [measurable]: "gp ∈ borel_measurable M" "gm ∈ borel_measurable M" unfolding gp_def gm_def by auto
define h where "h = (λx. ennreal(abs(g x)))"
have hgpgm: "⋀x. h x = gp x + gm x" unfolding gp_def gm_def h_def by (simp add: abs_real_def ennreal_neg)
have [measurable]: "h ∈ borel_measurable M" unfolding h_def by simp
have pos[simp]: "⋀x. h x ≥ 0" "⋀x. gp x ≥ 0" "⋀x. gm x ≥ 0" unfolding h_def gp_def gm_def by simp_all
have gp_real: "⋀x. enn2real(gp x) = max (g x) 0"
unfolding gp_def by (simp add: max_def ennreal_neg)
have gm_real: "⋀x. enn2real(gm x) = max (-g x) 0"
unfolding gm_def by (simp add: max_def ennreal_neg)
have "(∫⇧+ x. norm(f x * max (g x) 0) ∂M) ≤ (∫⇧+ x. norm(f x * g x) ∂M)"
by (simp add: nn_integral_mono)
also have "... < ∞" using assms(1) by (simp add: integrable_iff_bounded)
finally have "(∫⇧+ x. norm(f x * max (g x) 0) ∂M) < ∞" by simp
then have int1: "integrable M (λx. f x * max (g x) 0)" by (simp add: integrableI_bounded)
have "(∫⇧+ x. norm(f x * max (-g x) 0) ∂M) ≤ (∫⇧+ x. norm(f x * g x) ∂M)"
by (simp add: nn_integral_mono)
also have "... < ∞" using assms(1) by (simp add: integrable_iff_bounded)
finally have "(∫⇧+ x. norm(f x * max (-g x) 0) ∂M) < ∞" by simp
then have int2: "integrable M (λx. f x * max (-g x) 0)" by (simp add: integrableI_bounded)
have "(∫⇧+x. f x * nn_cond_exp M F h x ∂M) = (∫⇧+x. f x * h x ∂M)"
by (rule nn_cond_exp_intg) auto
also have "… = ∫⇧+ x. ennreal (f x * max (g x) 0 + f x * max (- g x) 0) ∂M"
unfolding h_def
by (intro nn_integral_cong)(auto simp: ennreal_mult[symmetric] abs_mult split: split_max)
also have "... < ∞"
using Bochner_Integration.integrable_add[OF int1 int2, THEN integrableD(2)] by (auto simp add: less_top)
finally have *: "(∫⇧+x. f x * nn_cond_exp M F h x ∂M) < ∞" by simp
have "(∫⇧+x. norm(f x * real_cond_exp M F g x) ∂M) = (∫⇧+x. f x * abs(real_cond_exp M F g x) ∂M)"
by (simp add: abs_mult)
also have "... ≤ (∫⇧+x. f x * nn_cond_exp M F h x ∂M)"
proof (rule nn_integral_mono_AE)
{
fix x assume *: "abs(real_cond_exp M F g x) ≤ nn_cond_exp M F h x"
have "ennreal (f x * ¦real_cond_exp M F g x¦) = f x * ennreal(¦real_cond_exp M F g x¦)"
by (simp add: ennreal_mult)
also have "... ≤ f x * nn_cond_exp M F h x"
using * by (auto intro!: mult_left_mono)
finally have "ennreal (f x * ¦real_cond_exp M F g x¦) ≤ f x * nn_cond_exp M F h x"
by simp
}
then show "AE x in M. ennreal (f x * ¦real_cond_exp M F g x¦) ≤ f x * nn_cond_exp M F h x"
using real_cond_exp_abs[OF assms(4)] h_def by auto
qed
finally have **: "(∫⇧+x. norm(f x * real_cond_exp M F g x) ∂M) < ∞" using * by auto
show "integrable M (λx. f x * real_cond_exp M F g x)"
using ** by (intro integrableI_bounded) auto
have "(∫⇧+x. f x * nn_cond_exp M F gp x ∂M) ≤ (∫⇧+x. f x * nn_cond_exp M F h x ∂M)"
proof (rule nn_integral_mono_AE)
have "AE x in M. nn_cond_exp M F gp x ≤ nn_cond_exp M F h x"
by (rule nn_cond_exp_mono) (auto simp add: hgpgm)
then show "AE x in M. f x * nn_cond_exp M F gp x ≤ f x * nn_cond_exp M F h x"
by (auto simp: mult_left_mono)
qed
then have a: "(∫⇧+x. f x * nn_cond_exp M F gp x ∂M) < ∞"
using * by auto
have "ennreal(norm(f x * enn2real(nn_cond_exp M F gp x))) ≤ f x * nn_cond_exp M F gp x" for x
by (auto simp add: ennreal_mult intro!: mult_left_mono)
(metis enn2real_ennreal enn2real_nonneg le_cases le_ennreal_iff)
then have "(∫⇧+x. norm(f x * enn2real(nn_cond_exp M F gp x)) ∂M) ≤ (∫⇧+x. f x * nn_cond_exp M F gp x ∂M)"
by (simp add: nn_integral_mono)
then have "(∫⇧+x. norm(f x * enn2real(nn_cond_exp M F gp x)) ∂M) < ∞" using a by auto
then have gp_int: "integrable M (λx. f x * enn2real(nn_cond_exp M F gp x))" by (simp add: integrableI_bounded)
have gp_fin: "AE x in M. f x * nn_cond_exp M F gp x ≠ ∞"
apply (rule nn_integral_PInf_AE) using a by auto
have "(∫ x. f x * enn2real(nn_cond_exp M F gp x) ∂M) = enn2real (∫⇧+ x. f x * enn2real(nn_cond_exp M F gp x) ∂M)"
by (rule integral_eq_nn_integral) auto
also have "... = enn2real(∫⇧+ x. ennreal(f x * enn2real(gp x)) ∂M)"
proof -
{
fix x assume "f x * nn_cond_exp M F gp x ≠ ∞"
then have "ennreal (f x * enn2real (nn_cond_exp M F gp x)) = ennreal (f x) * nn_cond_exp M F gp x"
by (auto simp add: ennreal_mult ennreal_mult_eq_top_iff less_top intro!: ennreal_mult_left_cong)
}
then have "AE x in M. ennreal (f x * enn2real (nn_cond_exp M F gp x)) = ennreal (f x) * nn_cond_exp M F gp x"
using gp_fin by auto
then have "(∫⇧+ x. f x * enn2real(nn_cond_exp M F gp x) ∂M) = (∫⇧+ x. f x * nn_cond_exp M F gp x ∂M)"
by (rule nn_integral_cong_AE)
also have "... = (∫⇧+ x. f x * gp x ∂M)"
by (rule nn_cond_exp_intg) (auto simp add: gp_def)
also have "... = (∫⇧+ x. ennreal(f x * enn2real(gp x)) ∂M)"
by (rule nn_integral_cong_AE) (auto simp: ennreal_mult gp_def)
finally have "(∫⇧+ x. f x * enn2real(nn_cond_exp M F gp x) ∂M) = (∫⇧+ x. ennreal(f x * enn2real(gp x)) ∂M)" by simp
then show ?thesis by simp
qed
also have "... = (∫ x. f x * enn2real(gp x) ∂M)"
by (rule integral_eq_nn_integral[symmetric]) (auto simp add: gp_def)
finally have gp_expr: "(∫ x. f x * enn2real(nn_cond_exp M F gp x) ∂M) = (∫ x. f x * enn2real(gp x) ∂M)" by simp
have "(∫⇧+x. f x * nn_cond_exp M F gm x ∂M) ≤ (∫⇧+x. f x * nn_cond_exp M F h x ∂M)"
proof (rule nn_integral_mono_AE)
have "AE x in M. nn_cond_exp M F gm x ≤ nn_cond_exp M F h x"
by (rule nn_cond_exp_mono) (auto simp add: hgpgm)
then show "AE x in M. f x * nn_cond_exp M F gm x ≤ f x * nn_cond_exp M F h x"
by (auto simp: mult_left_mono)
qed
then have a: "(∫⇧+x. f x * nn_cond_exp M F gm x ∂M) < ∞"
using * by auto
have "⋀x. ennreal(norm(f x * enn2real(nn_cond_exp M F gm x))) ≤ f x * nn_cond_exp M F gm x"
by (auto simp add: ennreal_mult intro!: mult_left_mono)
(metis enn2real_ennreal enn2real_nonneg le_cases le_ennreal_iff)
then have "(∫⇧+x. norm(f x * enn2real(nn_cond_exp M F gm x)) ∂M) ≤ (∫⇧+x. f x * nn_cond_exp M F gm x ∂M)"
by (simp add: nn_integral_mono)
then have "(∫⇧+x. norm(f x * enn2real(nn_cond_exp M F gm x)) ∂M) < ∞" using a by auto
then have gm_int: "integrable M (λx. f x * enn2real(nn_cond_exp M F gm x))" by (simp add: integrableI_bounded)
have gm_fin: "AE x in M. f x * nn_cond_exp M F gm x ≠ ∞"
apply (rule nn_integral_PInf_AE) using a by auto
have "(∫ x. f x * enn2real(nn_cond_exp M F gm x) ∂M) = enn2real (∫⇧+ x. f x * enn2real(nn_cond_exp M F gm x) ∂M)"
by (rule integral_eq_nn_integral) auto
also have "... = enn2real(∫⇧+ x. ennreal(f x * enn2real(gm x)) ∂M)"
proof -
{
fix x assume "f x * nn_cond_exp M F gm x ≠ ∞"
then have "ennreal (f x * enn2real (nn_cond_exp M F gm x)) = ennreal (f x) * nn_cond_exp M F gm x"
by (auto simp add: ennreal_mult ennreal_mult_eq_top_iff less_top intro!: ennreal_mult_left_cong)
}
then have "AE x in M. ennreal (f x * enn2real (nn_cond_exp M F gm x)) = ennreal (f x) * nn_cond_exp M F gm x"
using gm_fin by auto
then have "(∫⇧+ x. f x * enn2real(nn_cond_exp M F gm x) ∂M) = (∫⇧+ x. f x * nn_cond_exp M F gm x ∂M)"
by (rule nn_integral_cong_AE)
also have "... = (∫⇧+ x. f x * gm x ∂M)"
by (rule nn_cond_exp_intg) (auto simp add: gm_def)
also have "... = (∫⇧+ x. ennreal(f x * enn2real(gm x)) ∂M)"
by (rule nn_integral_cong_AE) (auto simp: ennreal_mult gm_def)
finally have "(∫⇧+ x. f x * enn2real(nn_cond_exp M F gm x) ∂M) = (∫⇧+ x. ennreal(f x * enn2real(gm x)) ∂M)" by simp
then show ?thesis by simp
qed
also have "... = (∫ x. f x * enn2real(gm x) ∂M)"
by (rule integral_eq_nn_integral[symmetric]) (auto simp add: gm_def)
finally have gm_expr: "(∫ x. f x * enn2real(nn_cond_exp M F gm x) ∂M) = (∫ x. f x * enn2real(gm x) ∂M)" by simp
have "(∫ x. f x * real_cond_exp M F g x ∂M) = (∫ x. f x * enn2real(nn_cond_exp M F gp x) - f x * enn2real(nn_cond_exp M F gm x) ∂M)"
unfolding real_cond_exp_def gp_def gm_def by (simp add: right_diff_distrib)
also have "... = (∫ x. f x * enn2real(nn_cond_exp M F gp x) ∂M) - (∫ x. f x * enn2real(nn_cond_exp M F gm x) ∂M)"
by (rule Bochner_Integration.integral_diff) (simp_all add: gp_int gm_int)
also have "... = (∫ x. f x * enn2real(gp x) ∂M) - (∫ x. f x * enn2real(gm x) ∂M)"
using gp_expr gm_expr by simp
also have "... = (∫ x. f x * max (g x) 0 ∂M) - (∫ x. f x * max (-g x) 0 ∂M)"
using gp_real gm_real by simp
also have "... = (∫ x. f x * max (g x) 0 - f x * max (-g x) 0 ∂M)"
by (rule Bochner_Integration.integral_diff[symmetric]) (simp_all add: int1 int2)
also have "... = (∫x. f x * g x ∂M)"
by (metis (mono_tags, opaque_lifting) diff_0 diff_zero eq_iff max.cobounded2 max_def minus_minus neg_le_0_iff_le right_diff_distrib)
finally show "(∫ x. f x * real_cond_exp M F g x ∂M) = (∫x. f x * g x ∂M)"
by simp
qed
lemma real_cond_exp_intg:
assumes "integrable M (λx. f x * g x)" and
[measurable]: "f ∈ borel_measurable F" "g ∈ borel_measurable M"
shows "integrable M (λx. f x * real_cond_exp M F g x)"
"(∫ x. f x * real_cond_exp M F g x ∂M) = (∫ x. f x * g x ∂M)"
proof -
have [measurable]: "f ∈ borel_measurable M" by (rule measurable_from_subalg[OF subalg assms(2)])
define fp where "fp = (λx. max (f x) 0)"
define fm where "fm = (λx. max (-f x) 0)"
have [measurable]: "fp ∈ borel_measurable M" "fm ∈ borel_measurable M"
unfolding fp_def fm_def by simp_all
have [measurable]: "fp ∈ borel_measurable F" "fm ∈ borel_measurable F"
unfolding fp_def fm_def by simp_all
have "(∫⇧+ x. norm(fp x * g x) ∂M) ≤ (∫⇧+ x. norm(f x * g x) ∂M)"
by (simp add: fp_def nn_integral_mono)
also have "... < ∞" using assms(1) by (simp add: integrable_iff_bounded)
finally have "(∫⇧+ x. norm(fp x * g x) ∂M) < ∞" by simp
then have intp: "integrable M (λx. fp x * g x)" by (simp add: integrableI_bounded)
moreover have "⋀x. fp x ≥ 0" unfolding fp_def by simp
ultimately have Rp: "integrable M (λx. fp x * real_cond_exp M F g x)"
"(∫ x. fp x * real_cond_exp M F g x ∂M) = (∫ x. fp x * g x ∂M)"
using real_cond_exp_intg_fpos by auto
have "(∫⇧+ x. norm(fm x * g x) ∂M) ≤ (∫⇧+ x. norm(f x * g x) ∂M)"
by (simp add: fm_def nn_integral_mono)
also have "... < ∞" using assms(1) by (simp add: integrable_iff_bounded)
finally have "(∫⇧+ x. norm(fm x * g x) ∂M) < ∞" by simp
then have intm: "integrable M (λx. fm x * g x)" by (simp add: integrableI_bounded)
moreover have "⋀x. fm x ≥ 0" unfolding fm_def by simp
ultimately have Rm: "integrable M (λx. fm x * real_cond_exp M F g x)"
"(∫ x. fm x * real_cond_exp M F g x ∂M) = (∫ x. fm x * g x ∂M)"
using real_cond_exp_intg_fpos by auto
have "integrable M (λx. fp x * real_cond_exp M F g x - fm x * real_cond_exp M F g x)"
using Rp(1) Rm(1) integrable_diff by simp
moreover have *: "⋀x. f x * real_cond_exp M F g x = fp x * real_cond_exp M F g x - fm x * real_cond_exp M F g x"
unfolding fp_def fm_def by (simp add: max_def)
ultimately show "integrable M (λx. f x * real_cond_exp M F g x)"
by simp
have "(∫ x. f x * real_cond_exp M F g x ∂M) = (∫ x. fp x * real_cond_exp M F g x - fm x * real_cond_exp M F g x ∂M)"
using * by simp
also have "... = (∫ x. fp x * real_cond_exp M F g x ∂M) - (∫ x. fm x * real_cond_exp M F g x ∂M)"
using Rp(1) Rm(1) by simp
also have "... = (∫ x. fp x * g x ∂M) - (∫ x. fm x * g x ∂M)"
using Rp(2) Rm(2) by simp
also have "... = (∫ x. fp x * g x - fm x * g x ∂M)"
using intm intp by simp
also have "... = (∫ x. f x * g x ∂M)"
unfolding fp_def fm_def by (metis (no_types, opaque_lifting) diff_0 diff_zero max.commute
max_def minus_minus mult.commute neg_le_iff_le right_diff_distrib)
finally show "(∫ x. f x * real_cond_exp M F g x ∂M) = (∫ x. f x * g x ∂M)" by simp
qed
lemma real_cond_exp_intA:
assumes [measurable]: "integrable M f" "A ∈ sets F"
shows "(∫ x ∈ A. f x ∂M) = (∫x ∈ A. real_cond_exp M F f x ∂M)"
proof -
have "A ∈ sets M" by (meson assms(2) subalg subalgebra_def subsetD)
have "integrable M (λx. indicator A x * f x)" using integrable_mult_indicator[OF ‹A ∈ sets M› assms(1)] by auto
then show ?thesis using real_cond_exp_intg(2)[where ?f = "indicator A" and ?g = f, symmetric]
unfolding set_lebesgue_integral_def by auto
qed
lemma real_cond_exp_int [intro]:
assumes "integrable M f"
shows "integrable M (real_cond_exp M F f)" "(∫x. real_cond_exp M F f x ∂M) = (∫x. f x ∂M)"
using real_cond_exp_intg[where ?f = "λx. 1" and ?g = f] assms by auto
lemma real_cond_exp_charact:
assumes "⋀A. A ∈ sets F ⟹ (∫ x ∈ A. f x ∂M) = (∫ x ∈ A. g x ∂M)"
and [measurable]: "integrable M f" "integrable M g"
"g ∈ borel_measurable F"
shows "AE x in M. real_cond_exp M F f x = g x"
proof -
let ?MF = "restr_to_subalg M F"
have "AE x in ?MF. real_cond_exp M F f x = g x"
proof (rule AE_symmetric[OF density_unique_real])
fix A assume "A ∈ sets ?MF"
then have [measurable]: "A ∈ sets F" using sets_restr_to_subalg[OF subalg] by simp
then have a [measurable]: "A ∈ sets M" by (meson subalg subalgebra_def subsetD)
have "(∫x ∈ A. g x ∂ ?MF) = (∫x ∈ A. g x ∂M)"
unfolding set_lebesgue_integral_def by (simp add: integral_subalgebra2 subalg)
also have "... = (∫x ∈ A. f x ∂M)" using assms(1) by simp
also have "... = (∫x. indicator A x * f x ∂M)" by (simp add: mult.commute set_lebesgue_integral_def)
also have "... = (∫x. indicator A x * real_cond_exp M F f x ∂M)"
apply (rule real_cond_exp_intg(2)[symmetric]) using integrable_mult_indicator[OF a assms(2)] by (auto simp add: assms)
also have "... = (∫x ∈ A. real_cond_exp M F f x ∂M)" by (simp add: mult.commute set_lebesgue_integral_def)
also have "... = (∫x ∈ A. real_cond_exp M F f x ∂ ?MF)"
by (simp add: integral_subalgebra2 subalg set_lebesgue_integral_def)
finally show "(∫x ∈ A. g x ∂ ?MF) = (∫x ∈ A. real_cond_exp M F f x ∂ ?MF)" by simp
next
have "integrable M (real_cond_exp M F f)" by (rule real_cond_exp_int(1)[OF assms(2)])
then show "integrable ?MF (real_cond_exp M F f)" by (metis borel_measurable_cond_exp integrable_in_subalg[OF subalg])
show "integrable (restr_to_subalg M F) g" by (simp add: assms(3) integrable_in_subalg[OF subalg])
qed
then show ?thesis using AE_restr_to_subalg[OF subalg] by auto
qed
lemma real_cond_exp_F_meas [intro, simp]:
assumes "integrable M f"
"f ∈ borel_measurable F"
shows "AE x in M. real_cond_exp M F f x = f x"
by (rule real_cond_exp_charact, auto simp add: assms measurable_from_subalg[OF subalg])
lemma real_cond_exp_mult:
assumes [measurable]:"f ∈ borel_measurable F" "g ∈ borel_measurable M" "integrable M (λx. f x * g x)"
shows "AE x in M. real_cond_exp M F (λx. f x * g x) x = f x * real_cond_exp M F g x"
proof (rule real_cond_exp_charact)
fix A assume "A ∈ sets F"
then have [measurable]: "(λx. f x * indicator A x) ∈ borel_measurable F" by measurable
have [measurable]: "A ∈ sets M" using subalg by (meson ‹A ∈ sets F› subalgebra_def subsetD)
have "(∫x∈A. (f x * g x) ∂M) = ∫x. (f x * indicator A x) * g x ∂M"
by (simp add: mult.commute mult.left_commute set_lebesgue_integral_def)
also have "... = ∫x. (f x * indicator A x) * real_cond_exp M F g x ∂M"
apply (rule real_cond_exp_intg(2)[symmetric], auto simp add: assms)
using integrable_mult_indicator[OF ‹A ∈ sets M› assms(3)] by (simp add: mult.commute mult.left_commute)
also have "... = (∫x∈A. (f x * real_cond_exp M F g x)∂M)"
by (simp add: mult.commute mult.left_commute set_lebesgue_integral_def)
finally show "(∫x∈A. (f x * g x) ∂M) = (∫x∈A. (f x * real_cond_exp M F g x)∂M)" by simp
qed (auto simp add: real_cond_exp_intg(1) assms)
lemma real_cond_exp_add [intro]:
assumes [measurable]: "integrable M f" "integrable M g"
shows "AE x in M. real_cond_exp M F (λx. f x + g x) x = real_cond_exp M F f x + real_cond_exp M F g x"
proof (rule real_cond_exp_charact)
have "integrable M (real_cond_exp M F f)" "integrable M (real_cond_exp M F g)"
using real_cond_exp_int(1) assms by auto
then show "integrable M (λx. real_cond_exp M F f x + real_cond_exp M F g x)"
by auto
fix A assume [measurable]: "A ∈ sets F"
then have "A ∈ sets M" by (meson subalg subalgebra_def subsetD)
have intAf: "integrable M (λx. indicator A x * f x)"
using integrable_mult_indicator[OF ‹A ∈ sets M› assms(1)] by auto
have intAg: "integrable M (λx. indicator A x * g x)"
using integrable_mult_indicator[OF ‹A ∈ sets M› assms(2)] by auto
have "(∫x∈A. (real_cond_exp M F f x + real_cond_exp M F g x)∂M) = (∫x∈A. real_cond_exp M F f x ∂M) + (∫x∈A. real_cond_exp M F g x ∂M)"
apply (rule set_integral_add, auto simp add: assms set_integrable_def)
using integrable_mult_indicator[OF ‹A ∈ sets M› real_cond_exp_int(1)[OF assms(1)]]
integrable_mult_indicator[OF ‹A ∈ sets M› real_cond_exp_int(1)[OF assms(2)]] by simp_all
also have "... = (∫x. indicator A x * real_cond_exp M F f x ∂M) + (∫x. indicator A x * real_cond_exp M F g x ∂M)"
unfolding set_lebesgue_integral_def by auto
also have "... = (∫x. indicator A x * f x ∂M) + (∫x. indicator A x * g x ∂M)"
using real_cond_exp_intg(2) assms ‹A ∈ sets F› intAf intAg by auto
also have "... = (∫x∈A. f x ∂M) + (∫x∈A. g x ∂M)"
unfolding set_lebesgue_integral_def by auto
also have "... = (∫x∈A. (f x + g x)∂M)"
by (rule set_integral_add(2)[symmetric]) (auto simp add: assms set_integrable_def ‹A ∈ sets M› intAf intAg)
finally show "(∫x∈A. (f x + g x)∂M) = (∫x∈A. (real_cond_exp M F f x + real_cond_exp M F g x)∂M)"
by simp
qed (auto simp add: assms)
lemma real_cond_exp_cong:
assumes ae: "AE x in M. f x = g x" and [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable M"
shows "AE x in M. real_cond_exp M F f x = real_cond_exp M F g x"
proof -
have "AE x in M. nn_cond_exp M F (λx. ennreal (f x)) x = nn_cond_exp M F (λx. ennreal (g x)) x"
apply (rule nn_cond_exp_cong) using assms by auto
moreover have "AE x in M. nn_cond_exp M F (λx. ennreal (-f x)) x = nn_cond_exp M F (λx. ennreal(-g x)) x"
apply (rule nn_cond_exp_cong) using assms by auto
ultimately show "AE x in M. real_cond_exp M F f x = real_cond_exp M F g x"
unfolding real_cond_exp_def by auto
qed
lemma real_cond_exp_cmult [intro, simp]:
fixes c::real
assumes "integrable M f"
shows "AE x in M. real_cond_exp M F (λx. c * f x) x = c * real_cond_exp M F f x"
by (rule real_cond_exp_mult[where ?f = "λx. c" and ?g = f], auto simp add: assms borel_measurable_integrable)
lemma real_cond_exp_cdiv [intro, simp]:
fixes c::real
assumes "integrable M f"
shows "AE x in M. real_cond_exp M F (λx. f x / c) x = real_cond_exp M F f x / c"
using real_cond_exp_cmult[of _ "1/c", OF assms] by (auto simp add: field_split_simps)
lemma real_cond_exp_diff [intro, simp]:
assumes [measurable]: "integrable M f" "integrable M g"
shows "AE x in M. real_cond_exp M F (λx. f x - g x) x = real_cond_exp M F f x - real_cond_exp M F g x"
proof -
have "AE x in M. real_cond_exp M F (λx. f x + (- g x)) x = real_cond_exp M F f x + real_cond_exp M F (λx. -g x) x"
using real_cond_exp_add[where ?f = f and ?g = "λx. - g x"] assms by auto
moreover have "AE x in M. real_cond_exp M F (λx. -g x) x = - real_cond_exp M F g x"
using real_cond_exp_cmult[where ?f = g and ?c = "-1"] assms(2) by auto
ultimately show ?thesis by auto
qed
lemma real_cond_exp_pos [intro]:
assumes "AE x in M. f x ≥ 0" and [measurable]: "f ∈ borel_measurable M"
shows "AE x in M. real_cond_exp M F f x ≥ 0"
proof -
define g where "g = (λx. max (f x) 0)"
have "AE x in M. f x = g x" using assms g_def by auto
then have *: "AE x in M. real_cond_exp M F f x = real_cond_exp M F g x" using real_cond_exp_cong g_def by auto
have "⋀x. g x ≥ 0" unfolding g_def by simp
then have "(λx. ennreal(-g x)) = (λx. 0)"
by (simp add: ennreal_neg)
moreover have "AE x in M. 0 = nn_cond_exp M F (λx. 0) x"
by (rule nn_cond_exp_F_meas, auto)
ultimately have "AE x in M. nn_cond_exp M F (λx. ennreal(-g x)) x = 0"
by simp
then have "AE x in M. real_cond_exp M F g x = enn2real(nn_cond_exp M F (λx. ennreal (g x)) x)"
unfolding real_cond_exp_def by auto
then have "AE x in M. real_cond_exp M F g x ≥ 0" by auto
then show ?thesis using * by auto
qed
lemma real_cond_exp_mono:
assumes "AE x in M. f x ≤ g x" and [measurable]: "integrable M f" "integrable M g"
shows "AE x in M. real_cond_exp M F f x ≤ real_cond_exp M F g x"
proof -
have "AE x in M. real_cond_exp M F g x - real_cond_exp M F f x = real_cond_exp M F (λx. g x - f x) x"
by (rule AE_symmetric[OF real_cond_exp_diff], auto simp add: assms)
moreover have "AE x in M. real_cond_exp M F (λx. g x - f x) x ≥ 0"
by (rule real_cond_exp_pos, auto simp add: assms(1))
ultimately have "AE x in M. real_cond_exp M F g x - real_cond_exp M F f x ≥ 0" by auto
then show ?thesis by auto
qed
lemma (in -) measurable_P_restriction [measurable (raw)]:
assumes [measurable]: "Measurable.pred M P" "A ∈ sets M"
shows "{x ∈ A. P x} ∈ sets M"
proof -
have "A ⊆ space M" using sets.sets_into_space[OF assms(2)].
then have "{x ∈ A. P x} = A ∩ {x ∈ space M. P x}" by blast
then show ?thesis by auto
qed
lemma real_cond_exp_gr_c:
assumes [measurable]: "integrable M f"
and AE: "AE x in M. f x > c"
shows "AE x in M. real_cond_exp M F f x > c"
proof -
define X where "X = {x ∈ space M. real_cond_exp M F f x ≤ c}"
have [measurable]: "X ∈ sets F"
unfolding X_def apply measurable by (metis sets.top subalg subalgebra_def)
then have [measurable]: "X ∈ sets M" using sets_restr_to_subalg subalg subalgebra_def by blast
have "emeasure M X = 0"
proof (rule ccontr)
assume "¬(emeasure M X) = 0"
have "emeasure (restr_to_subalg M F) X = emeasure M X"
by (simp add: emeasure_restr_to_subalg subalg)
then have "emeasure (restr_to_subalg M F) X > 0"
using ‹¬(emeasure M X) = 0› gr_zeroI by auto
then obtain A where "A ∈ sets (restr_to_subalg M F)" "A ⊆ X" "emeasure (restr_to_subalg M F) A > 0" "emeasure (restr_to_subalg M F) A < ∞"
using sigma_fin_subalg by (metis emeasure_notin_sets ennreal_0 infinity_ennreal_def le_less_linear neq_top_trans
not_gr_zero order_refl sigma_finite_measure.approx_PInf_emeasure_with_finite)
then have [measurable]: "A ∈ sets F" using subalg sets_restr_to_subalg by blast
then have [measurable]: "A ∈ sets M" using sets_restr_to_subalg subalg subalgebra_def by blast
have Ic: "set_integrable M A (λx. c)"
unfolding set_integrable_def
using ‹emeasure (restr_to_subalg M F) A < ∞› emeasure_restr_to_subalg subalg by fastforce
have If: "set_integrable M A f"
unfolding set_integrable_def
by (rule integrable_mult_indicator, auto simp add: ‹integrable M f›)
have "AE x in M. indicator A x * c = indicator A x * f x"
proof (rule integral_ineq_eq_0_then_AE)
have "(∫x∈A. c ∂M) = (∫x∈A. f x ∂M)"
proof (rule antisym)
show "(∫x∈A. c ∂M) ≤ (∫x∈A. f x ∂M)"
apply (rule set_integral_mono_AE) using Ic If assms(2) by auto
have "(∫x∈A. f x ∂M) = (∫x∈A. real_cond_exp M F f x ∂M)"
by (rule real_cond_exp_intA, auto simp add: ‹integrable M f›)
also have "... ≤ (∫x∈A. c ∂M)"
apply (rule set_integral_mono)
unfolding set_integrable_def
apply (rule integrable_mult_indicator, simp, simp add: real_cond_exp_int(1)[OF ‹integrable M f›])
using Ic X_def ‹A ⊆ X› by (auto simp: set_integrable_def)
finally show "(∫x∈A. f x ∂M) ≤ (∫x∈A. c ∂M)" by simp
qed
then have "measure M A * c = LINT x|M. indicat_real A x * f x"
by (auto simp: set_lebesgue_integral_def)
then show "LINT x|M. indicat_real A x * c = LINT x|M. indicat_real A x * f x"
by auto
show "AE x in M. indicat_real A x * c ≤ indicat_real A x * f x"
using AE unfolding indicator_def by auto
qed (use Ic If in ‹auto simp: set_integrable_def›)
then have "AE x∈A in M. c = f x" by auto
then have "AE x∈A in M. False" using assms(2) by auto
have "A ∈ null_sets M" unfolding ae_filter_def by (meson AE_iff_null_sets ‹A ∈ sets M› ‹AE x∈A in M. False›)
then show False using ‹emeasure (restr_to_subalg M F) A > 0›
by (simp add: emeasure_restr_to_subalg null_setsD1 subalg)
qed
then show ?thesis using AE_iff_null_sets[OF ‹X ∈ sets M›] unfolding X_def by auto
qed
lemma real_cond_exp_less_c:
assumes [measurable]: "integrable M f"
and "AE x in M. f x < c"
shows "AE x in M. real_cond_exp M F f x < c"
proof -
have "AE x in M. real_cond_exp M F f x = -real_cond_exp M F (λx. -f x) x"
using real_cond_exp_cmult[OF ‹integrable M f›, of "-1"] by auto
moreover have "AE x in M. real_cond_exp M F (λx. -f x) x > -c"
apply (rule real_cond_exp_gr_c) using assms by auto
ultimately show ?thesis by auto
qed
lemma real_cond_exp_ge_c:
assumes [measurable]: "integrable M f"
and "AE x in M. f x ≥ c"
shows "AE x in M. real_cond_exp M F f x ≥ c"
proof -
obtain u::"nat ⇒ real" where u: "⋀n. u n < c" "u ⇢ c"
using approx_from_below_dense_linorder[of "c-1" c] by auto
have *: "AE x in M. real_cond_exp M F f x > u n" for n::nat
apply (rule real_cond_exp_gr_c) using assms ‹u n < c› by auto
have "AE x in M. ∀n. real_cond_exp M F f x > u n"
by (subst AE_all_countable, auto simp add: *)
moreover have "real_cond_exp M F f x ≥ c" if "∀n. real_cond_exp M F f x > u n" for x
proof -
have "real_cond_exp M F f x ≥ u n" for n using that less_imp_le by auto
then show ?thesis using u(2) LIMSEQ_le_const2 by metis
qed
ultimately show ?thesis by auto
qed
lemma real_cond_exp_le_c:
assumes [measurable]: "integrable M f"
and "AE x in M. f x ≤ c"
shows "AE x in M. real_cond_exp M F f x ≤ c"
proof -
have "AE x in M. real_cond_exp M F f x = -real_cond_exp M F (λx. -f x) x"
using real_cond_exp_cmult[OF ‹integrable M f›, of "-1"] by auto
moreover have "AE x in M. real_cond_exp M F (λx. -f x) x ≥ -c"
apply (rule real_cond_exp_ge_c) using assms by auto
ultimately show ?thesis by auto
qed
lemma real_cond_exp_mono_strict:
assumes "AE x in M. f x < g x" and [measurable]: "integrable M f" "integrable M g"
shows "AE x in M. real_cond_exp M F f x < real_cond_exp M F g x"
proof -
have "AE x in M. real_cond_exp M F g x - real_cond_exp M F f x = real_cond_exp M F (λx. g x - f x) x"
by (rule AE_symmetric[OF real_cond_exp_diff], auto simp add: assms)
moreover have "AE x in M. real_cond_exp M F (λx. g x - f x) x > 0"
by (rule real_cond_exp_gr_c, auto simp add: assms)
ultimately have "AE x in M. real_cond_exp M F g x - real_cond_exp M F f x > 0" by auto
then show ?thesis by auto
qed
lemma real_cond_exp_nested_subalg [intro, simp]:
assumes "subalgebra M G" "subalgebra G F"
and [measurable]: "integrable M f"
shows "AE x in M. real_cond_exp M F (real_cond_exp M G f) x = real_cond_exp M F f x"
proof (rule real_cond_exp_charact)
interpret G: sigma_finite_subalgebra M G by (rule nested_subalg_is_sigma_finite[OF assms(1) assms(2)])
show "integrable M (real_cond_exp M G f)" by (auto simp add: assms G.real_cond_exp_int(1))
fix A assume [measurable]: "A ∈ sets F"
then have [measurable]: "A ∈ sets G" using assms(2) by (meson subsetD subalgebra_def)
have "set_lebesgue_integral M A (real_cond_exp M G f) = set_lebesgue_integral M A f"
by (rule G.real_cond_exp_intA[symmetric], auto simp add: assms(3))
also have "... = set_lebesgue_integral M A (real_cond_exp M F f)"
by (rule real_cond_exp_intA, auto simp add: assms(3))
finally show "set_lebesgue_integral M A (real_cond_exp M G f) = set_lebesgue_integral M A (real_cond_exp M F f)" by auto
qed (auto simp add: assms real_cond_exp_int(1))
lemma real_cond_exp_sum [intro, simp]:
fixes f::"'b ⇒ 'a ⇒ real"
assumes [measurable]: "⋀i. integrable M (f i)"
shows "AE x in M. real_cond_exp M F (λx. ∑i∈I. f i x) x = (∑i∈I. real_cond_exp M F (f i) x)"
proof (rule real_cond_exp_charact)
fix A assume [measurable]: "A ∈ sets F"
then have A_meas [measurable]: "A ∈ sets M" by (meson subsetD subalg subalgebra_def)
have *: "integrable M (λx. indicator A x * f i x)" for i
using integrable_mult_indicator[OF ‹A ∈ sets M› assms(1)] by auto
have **: "integrable M (λx. indicator A x * real_cond_exp M F (f i) x)" for i
using integrable_mult_indicator[OF ‹A ∈ sets M› real_cond_exp_int(1)[OF assms(1)]] by auto
have inti: "(∫x. indicator A x * f i x ∂M) = (∫x. indicator A x * real_cond_exp M F (f i) x ∂M)" for i
by (rule real_cond_exp_intg(2)[symmetric], auto simp add: *)
have "(∫x∈A. (∑i∈I. f i x)∂M) = (∫x. (∑i∈I. indicator A x * f i x)∂M)"
by (simp add: sum_distrib_left set_lebesgue_integral_def)
also have "... = (∑i∈I. (∫x. indicator A x * f i x ∂M))"
by (rule Bochner_Integration.integral_sum, simp add: *)
also have "... = (∑i∈I. (∫x. indicator A x * real_cond_exp M F (f i) x ∂M))"
using inti by auto
also have "... = (∫x. (∑i∈I. indicator A x * real_cond_exp M F (f i) x)∂M)"
by (rule Bochner_Integration.integral_sum[symmetric], simp add: **)
also have "... = (∫x∈A. (∑i∈I. real_cond_exp M F (f i) x)∂M)"
by (simp add: sum_distrib_left set_lebesgue_integral_def)
finally show "(∫x∈A. (∑i∈I. f i x)∂M) = (∫x∈A. (∑i∈I. real_cond_exp M F (f i) x)∂M)" by auto
qed (auto simp add: assms real_cond_exp_int(1)[OF assms(1)])
text ‹Jensen's inequality, describing the behavior of the integral under a convex function, admits
a version for the conditional expectation, as follows.›
theorem real_cond_exp_jensens_inequality:
fixes q :: "real ⇒ real"
assumes X: "integrable M X" "AE x in M. X x ∈ I"
assumes I: "I = {a <..< b} ∨ I = {a <..} ∨ I = {..< b} ∨ I = UNIV"
assumes q: "integrable M (λx. q (X x))" "convex_on I q" "q ∈ borel_measurable borel"
shows "AE x in M. real_cond_exp M F X x ∈ I"
"AE x in M. q (real_cond_exp M F X x) ≤ real_cond_exp M F (λx. q (X x)) x"
proof -
have "open I" using I by auto
then have "interior I = I" by (simp add: interior_eq)
have [measurable]: "I ∈ sets borel" using I by auto
define phi where "phi = (λx. Inf ((λt. (q x - q t) / (x - t)) ` ({x<..} ∩ I)))"
have **: "q (X x) ≥ q (real_cond_exp M F X x) + phi (real_cond_exp M F X x) * (X x - real_cond_exp M F X x)"
if "X x ∈ I" "real_cond_exp M F X x ∈ I" for x
unfolding phi_def apply (rule convex_le_Inf_differential)
using ‹convex_on I q› that ‹interior I = I› by auto
text ‹It is not clear that the function $\phi$ is measurable. We replace it by a version which
is better behaved.›
define psi where "psi = (λx. phi x * indicator I x)"
have A: "psi y = phi y" if "y ∈ I" for y unfolding psi_def indicator_def using that by auto
have *: "q (X x) ≥ q (real_cond_exp M F X x) + psi (real_cond_exp M F X x) * (X x - real_cond_exp M F X x)"
if "X x ∈ I" "real_cond_exp M F X x ∈ I" for x
unfolding A[OF ‹real_cond_exp M F X x ∈ I›] using ** that by auto
note I
moreover have "AE x in M. real_cond_exp M F X x > a" if "I ⊆ {a <..}" for a
apply (rule real_cond_exp_gr_c) using X that by auto
moreover have "AE x in M. real_cond_exp M F X x < b" if "I ⊆ {..<b}" for b
apply (rule real_cond_exp_less_c) using X that by auto
ultimately show "AE x in M. real_cond_exp M F X x ∈ I"
by (elim disjE) (auto simp: subset_eq)
then have main_ineq: "AE x in M. q (X x) ≥ q (real_cond_exp M F X x) + psi (real_cond_exp M F X x) * (X x - real_cond_exp M F X x)"
using * X(2) by auto
text ‹Then, one wants to take the conditional expectation of this inequality. On the left, one gets
the conditional expectation of $q \circ X$. On the right, the last term vanishes, and one
is left with $q$ of the conditional expectation, as desired. Unfortunately, this argument only
works if $\psi \cdot X$ and $q(E(X | F))$ are integrable, and there is no reason why this should be true. The
trick is to multiply by a $F$-measurable function which is small enough to make
everything integrable.›
obtain f::"'a ⇒ real" where [measurable]: "f ∈ borel_measurable (restr_to_subalg M F)"
"integrable (restr_to_subalg M F) f"
and f: "⋀x. f x > 0" "⋀x. f x ≤ 1"
using sigma_finite_measure.obtain_positive_integrable_function[OF sigma_fin_subalg] by metis
then have [measurable]: "f ∈ borel_measurable F" by (simp add: subalg)
then have [measurable]: "f ∈ borel_measurable M" using measurable_from_subalg[OF subalg] by blast
define g where "g = (λx. f x/(1+ ¦psi (real_cond_exp M F X x)¦ + ¦q (real_cond_exp M F X x)¦))"
define G where "G = (λx. g x * psi (real_cond_exp M F X x))"
have g: "g x > 0" "g x ≤ 1" for x unfolding G_def g_def using f[of x] by (auto simp add: abs_mult)
have G: "¦G x¦ ≤ 1" for x unfolding G_def g_def using f[of x]
proof (auto simp add: abs_mult)
have "f x * ¦psi (real_cond_exp M F X x)¦ ≤ 1 * ¦psi (real_cond_exp M F X x)¦"
apply (rule mult_mono) using f[of x] by auto
also have "... ≤ 1 + ¦psi (real_cond_exp M F X x)¦ + ¦q (real_cond_exp M F X x)¦" by auto
finally show "f x * ¦psi (real_cond_exp M F X x)¦ ≤ 1 + ¦psi (real_cond_exp M F X x)¦ + ¦q (real_cond_exp M F X x)¦"
by simp
qed
have "AE x in M. g x * q (X x) ≥ g x * (q (real_cond_exp M F X x) + psi (real_cond_exp M F X x) * (X x - real_cond_exp M F X x))"
using main_ineq g by (auto simp add: divide_simps)
then have main_G: "AE x in M. g x * q (X x) ≥ g x * q (real_cond_exp M F X x) + G x * (X x - real_cond_exp M F X x)"
unfolding G_def by (auto simp add: algebra_simps)
text ‹To proceed, we need to know that $\psi$ is measurable.›
have phi_mono: "phi x ≤ phi y" if "x ≤ y" "x ∈ I" "y ∈ I" for x y
proof (cases "x < y")
case True
have "q x + phi x * (y-x) ≤ q y"
unfolding phi_def apply (rule convex_le_Inf_differential) using ‹convex_on I q› that ‹interior I = I› by auto
then have "phi x ≤ (q x - q y) / (x - y)"
using that ‹x < y› by (auto simp add: field_split_simps algebra_simps)
moreover have "(q x - q y)/(x - y) ≤ phi y"
unfolding phi_def proof (rule cInf_greatest, auto)
fix t assume "t ∈ I" "y < t"
have "(q x - q y) / (x - y) ≤ (q x - q t) / (x - t)"
apply (rule convex_on_slope_le[OF q(2)]) using ‹y < t› ‹x < y› ‹t ∈ I› ‹x ∈ I› by auto
also have "... ≤ (q y - q t) / (y - t)"
apply (rule convex_on_slope_le[OF q(2)]) using ‹y < t› ‹x < y› ‹t ∈ I› ‹x ∈ I› by auto
finally show "(q x - q y) / (x - y) ≤ (q y - q t) / (y - t)" by simp
next
obtain e where "0 < e" "ball y e ⊆ I" using ‹open I› ‹y ∈ I› openE by blast
then have "y + e/2 ∈ {y<..} ∩ I" by (auto simp: dist_real_def)
then show "{y<..} ∩ I = {} ⟹ False" by auto
qed
ultimately show "phi x ≤ phi y" by auto
next
case False
then have "x = y" using ‹x ≤ y› by auto
then show ?thesis by auto
qed
have [measurable]: "psi ∈ borel_measurable borel"
by (rule borel_measurable_piecewise_mono[of "{I, -I}"])
(auto simp add: psi_def indicator_def phi_mono intro: mono_onI)
have [measurable]: "q ∈ borel_measurable borel" using q by simp
have [measurable]: "X ∈ borel_measurable M"
"real_cond_exp M F X ∈ borel_measurable F"
"g ∈ borel_measurable F" "g ∈ borel_measurable M"
"G ∈ borel_measurable F" "G ∈ borel_measurable M"
using X measurable_from_subalg[OF subalg] unfolding G_def g_def by auto
have int1: "integrable (restr_to_subalg M F) (λx. g x * q (real_cond_exp M F X x))"
apply (rule Bochner_Integration.integrable_bound[of _ f], auto simp add: subalg ‹integrable (restr_to_subalg M F) f›)
unfolding g_def by (auto simp add: field_split_simps abs_mult algebra_simps)
have int2: "integrable M (λx. G x * (X x - real_cond_exp M F X x))"
apply (rule Bochner_Integration.integrable_bound[of _ "λx. ¦X x¦ + ¦real_cond_exp M F X x¦"])
apply (auto intro!: Bochner_Integration.integrable_add integrable_abs real_cond_exp_int ‹integrable M X› AE_I2)
using G unfolding abs_mult by (meson abs_ge_zero abs_triangle_ineq4 dual_order.trans mult_left_le_one_le)
have int3: "integrable M (λx. g x * q (X x))"
apply (rule Bochner_Integration.integrable_bound[of _ "λx. q(X x)"], auto simp add: q(1) abs_mult)
using g by (simp add: less_imp_le mult_left_le_one_le)
text ‹Taking the conditional expectation of the main convexity inequality \verb+main_G+, we get
the following.›
have "AE x in M. real_cond_exp M F (λx. g x * q (X x)) x ≥ real_cond_exp M F (λx. g x * q (real_cond_exp M F X x) + G x * (X x - real_cond_exp M F X x)) x"
apply (rule real_cond_exp_mono[OF main_G])
apply (rule Bochner_Integration.integrable_add[OF integrable_from_subalg[OF subalg int1]])
using int2 int3 by auto
text ‹This reduces to the desired inequality thanks to the properties of conditional expectation,
i.e., the conditional expectation of an $F$-measurable function is this function, and one can
multiply an $F$-measurable function outside of conditional expectations.
Since all these equalities only hold almost everywhere, we formulate them separately,
and then combine all of them to simplify the above equation, again almost everywhere.›
moreover have "AE x in M. real_cond_exp M F (λx. g x * q (X x)) x = g x * real_cond_exp M F (λx. q (X x)) x"
by (rule real_cond_exp_mult, auto simp add: int3)
moreover have "AE x in M. real_cond_exp M F (λx. g x * q (real_cond_exp M F X x) + G x * (X x - real_cond_exp M F X x)) x
= real_cond_exp M F (λx. g x * q (real_cond_exp M F X x)) x + real_cond_exp M F (λx. G x * (X x - real_cond_exp M F X x)) x"
by (rule real_cond_exp_add, auto simp add: integrable_from_subalg[OF subalg int1] int2)
moreover have "AE x in M. real_cond_exp M F (λx. g x * q (real_cond_exp M F X x)) x = g x * q (real_cond_exp M F X x)"
by (rule real_cond_exp_F_meas, auto simp add: integrable_from_subalg[OF subalg int1])
moreover have "AE x in M. real_cond_exp M F (λx. G x * (X x - real_cond_exp M F X x)) x = G x * real_cond_exp M F (λx. (X x - real_cond_exp M F X x)) x"
by (rule real_cond_exp_mult, auto simp add: int2)
moreover have "AE x in M. real_cond_exp M F (λx. (X x - real_cond_exp M F X x)) x = real_cond_exp M F X x - real_cond_exp M F (λx. real_cond_exp M F X x) x"
by (rule real_cond_exp_diff, auto intro!: real_cond_exp_int ‹integrable M X›)
moreover have "AE x in M. real_cond_exp M F (λx. real_cond_exp M F X x) x = real_cond_exp M F X x "
by (rule real_cond_exp_F_meas, auto intro!: real_cond_exp_int ‹integrable M X›)
ultimately have "AE x in M. g x * real_cond_exp M F (λx. q (X x)) x ≥ g x * q (real_cond_exp M F X x)"
by auto
then show "AE x in M. real_cond_exp M F (λx. q (X x)) x ≥ q (real_cond_exp M F X x)"
using g(1) by (auto simp add: field_split_simps)
qed
text ‹Jensen's inequality does not imply that $q(E(X|F))$ is integrable, as it only proves an upper
bound for it. Indeed, this is not true in general, as the following counterexample shows:
on $[1,\infty)$ with Lebesgue measure, let $F$ be the sigma-algebra generated by the intervals $[n, n+1)$
for integer $n$. Let $q(x) = - \sqrt{x}$ for $x\geq 0$. Define $X$ which is equal to $1/n$ over
$[n, n+1/n)$ and $2^{-n}$ on $[n+1/n, n+1)$. Then $X$ is integrable as $\sum 1/n^2 < \infty$, and
$q(X)$ is integrable as $\sum 1/n^{3/2} < \infty$. On the other hand, $E(X|F)$ is essentially equal
to $1/n^2$ on $[n, n+1)$ (we neglect the term $2^{-n}$, we only put it there because $X$ should take
its values in $I=(0,\infty)$). Hence, $q(E(X|F))$ is equal to $-1/n$ on $[n, n+1)$, hence it is not
integrable.
However, this counterexample is essentially the only situation where this function is not
integrable, as shown by the next lemma.
›
lemma integrable_convex_cond_exp:
fixes q :: "real ⇒ real"
assumes X: "integrable M X" "AE x in M. X x ∈ I"
assumes I: "I = {a <..< b} ∨ I = {a <..} ∨ I = {..< b} ∨ I = UNIV"
assumes q: "integrable M (λx. q (X x))" "convex_on I q" "q ∈ borel_measurable borel"
assumes H: "emeasure M (space M) = ∞ ⟹ 0 ∈ I"
shows "integrable M (λx. q (real_cond_exp M F X x))"
proof -
have [measurable]: "(λx. q (real_cond_exp M F X x)) ∈ borel_measurable M"
"q ∈ borel_measurable borel"
"X ∈ borel_measurable M"
using X(1) q(3) by auto
have "open I" using I by auto
then have "interior I = I" by (simp add: interior_eq)
consider "emeasure M (space M) = 0" | "emeasure M (space M) > 0 ∧ emeasure M (space M) < ∞" | "emeasure M (space M) = ∞"
by (metis infinity_ennreal_def not_gr_zero top.not_eq_extremum)
then show ?thesis
proof (cases)
case 1
show ?thesis by (subst integrable_cong_AE[of _ _ "λx. 0"], auto intro: emeasure_0_AE[OF 1])
next
case 2
interpret finite_measure M using 2 by (auto intro!: finite_measureI)
have "I ≠ {}"
using ‹AE x in M. X x ∈ I› 2 eventually_mono integral_less_AE_space by fastforce
then obtain z where "z ∈ I" by auto
define A where "A = Inf ((λt. (q z - q t) / (z - t)) ` ({z<..} ∩ I))"
have "q y ≥ q z + A * (y - z)" if "y ∈ I" for y unfolding A_def apply (rule convex_le_Inf_differential)
using ‹z ∈ I› ‹y ∈ I› ‹interior I = I› q(2) by auto
then have "AE x in M. q (real_cond_exp M F X x) ≥ q z + A * (real_cond_exp M F X x - z)"
using real_cond_exp_jensens_inequality(1)[OF X I q] by auto
moreover have "AE x in M. q (real_cond_exp M F X x) ≤ real_cond_exp M F (λx. q (X x)) x"
using real_cond_exp_jensens_inequality(2)[OF X I q] by auto
moreover have "¦a¦ ≤ ¦b¦ + ¦c¦" if "b ≤ a ∧ a ≤ c" for a b c::real
using that by auto
ultimately have *: "AE x in M. ¦q (real_cond_exp M F X x)¦
≤ ¦real_cond_exp M F (λx. q (X x)) x¦ + ¦q z + A * (real_cond_exp M F X x - z)¦"
by auto
show "integrable M (λx. q (real_cond_exp M F X x))"
apply (rule Bochner_Integration.integrable_bound[of _ "λx. ¦real_cond_exp M F (λx. q (X x)) x¦ + ¦q z + A * (real_cond_exp M F X x - z)¦"])
apply (auto intro!: Bochner_Integration.integrable_add integrable_abs integrable_mult_right Bochner_Integration.integrable_diff real_cond_exp_int(1))
using X(1) q(1) * by auto
next
case 3
then have "0 ∈ I" using H finite_measure.finite_emeasure_space by auto
have "q(0) = 0"
proof (rule ccontr)
assume *: "¬(q(0) = 0)"
define e where "e = ¦q(0)¦ / 2"
then have "e > 0" using * by auto
have "continuous (at 0) q"
using q(2) ‹0 ∈ I› ‹open I› ‹interior I = I› continuous_on_interior convex_on_continuous by blast
then obtain d where d: "d > 0" "⋀y. ¦y - 0¦ < d ⟹ ¦q y - q 0¦ < e" using ‹e > 0›
by (metis continuous_at_real_range real_norm_def)
then have *: "¦q(y)¦ > e" if "¦y¦ < d" for y
proof -
have "¦q 0¦ ≤ ¦q 0 - q y¦ + ¦q y¦" by auto
also have "... < e + ¦q y¦" using d(2) that by force
finally have "¦q y¦ > ¦q 0¦ - e" by auto
then show ?thesis unfolding e_def by simp
qed
have "emeasure M {x ∈ space M. ¦X x¦ < d} ≤ emeasure M ({x ∈ space M. 1 ≤ ennreal(1/e) * ¦q(X x)¦})"
by (rule emeasure_mono, auto simp add: * ‹e>0› less_imp_le ennreal_mult''[symmetric])
also have "... ≤ (1/e) * (∫⇧+x. ennreal(¦q(X x)¦) * indicator (space M) x ∂M)"
by (rule nn_integral_Markov_inequality, auto)
also have "... = (1/e) * (∫⇧+x. ennreal(¦q(X x)¦) ∂M)" by auto
also have "... = (1/e) * ennreal(∫x. ¦q(X x)¦ ∂M)"
using nn_integral_eq_integral[OF integrable_abs[OF q(1)]] by auto
also have "... < ∞"
by (simp add: ennreal_mult_less_top)
finally have A: "emeasure M {x ∈ space M. ¦X x¦ < d} < ∞" by simp
have "{x ∈ space M. ¦X x¦ ≥ d} = {x ∈ space M. 1 ≤ ennreal(1/d) * ¦X x¦} ∩ space M"
by (auto simp add: ‹d>0› ennreal_mult''[symmetric])
then have "emeasure M {x ∈ space M. ¦X x¦ ≥ d} = emeasure M ({x ∈ space M. 1 ≤ ennreal(1/d) * ¦X x¦})"
by auto
also have "... ≤ (1/d) * (∫⇧+x. ennreal(¦X x¦) * indicator (space M) x ∂M)"
by (rule nn_integral_Markov_inequality, auto)
also have "... = (1/d) * (∫⇧+x. ennreal(¦X x¦) ∂M)" by auto
also have "... = (1/d) * ennreal(∫x. ¦X x¦ ∂M)"
using nn_integral_eq_integral[OF integrable_abs[OF X(1)]] by auto
also have "... < ∞"
by (simp add: ennreal_mult_less_top)
finally have B: "emeasure M {x ∈ space M. ¦X x¦ ≥ d} < ∞" by simp
have "space M = {x ∈ space M. ¦X x¦ < d} ∪ {x ∈ space M. ¦X x¦ ≥ d}" by auto
then have "emeasure M (space M) = emeasure M ({x ∈ space M. ¦X x¦ < d} ∪ {x ∈ space M. ¦X x¦ ≥ d})"
by simp
also have "... ≤ emeasure M {x ∈ space M. ¦X x¦ < d} + emeasure M {x ∈ space M. ¦X x¦ ≥ d}"
by (auto intro!: emeasure_subadditive)
also have "... < ∞" using A B by auto
finally show False using ‹emeasure M (space M) = ∞› by auto
qed
define A where "A = Inf ((λt. (q 0 - q t) / (0 - t)) ` ({0<..} ∩ I))"
have "q y ≥ q 0 + A * (y - 0)" if "y ∈ I" for y unfolding A_def apply (rule convex_le_Inf_differential)
using ‹0 ∈ I› ‹y ∈ I› ‹interior I = I› q(2) by auto
then have "q y ≥ A * y" if "y ∈ I" for y using ‹q 0 = 0› that by auto
then have "AE x in M. q (real_cond_exp M F X x) ≥ A * real_cond_exp M F X x"
using real_cond_exp_jensens_inequality(1)[OF X I q] by auto
moreover have "AE x in M. q (real_cond_exp M F X x) ≤ real_cond_exp M F (λx. q (X x)) x"
using real_cond_exp_jensens_inequality(2)[OF X I q] by auto
moreover have "¦a¦ ≤ ¦b¦ + ¦c¦" if "b ≤ a ∧ a ≤ c" for a b c::real
using that by auto
ultimately have *: "AE x in M. ¦q (real_cond_exp M F X x)¦
≤ ¦real_cond_exp M F (λx. q (X x)) x¦ + ¦A * real_cond_exp M F X x¦"
by auto
show "integrable M (λx. q (real_cond_exp M F X x))"
apply (rule Bochner_Integration.integrable_bound[of _ "λx. ¦real_cond_exp M F (λx. q (X x)) x¦ + ¦A * real_cond_exp M F X x ¦"])
apply (auto intro!: Bochner_Integration.integrable_add integrable_abs integrable_mult_right Bochner_Integration.integrable_diff real_cond_exp_int(1))
using X(1) q(1) * by auto
qed
qed
end
end