Theory Conditional_Expectation_Banach
theory Conditional_Expectation_Banach
imports "HOL-Probability.Conditional_Expectation" "HOL-Probability.Independent_Family"
begin
section ‹Conditional Expectation in Banach Spaces›
text ‹While constructing the conditional expectation operator, we have come up with the following approach, which is based on the construction in \cite{Hytoenen_2016}.
Both our approach, and the one in \cite{Hytoenen_2016} are based on showing that the conditional expectation is a contraction on some dense subspace of the space of functions ‹L⇧1(E)›.
In our approach, we start by constructing the conditional expectation explicitly for simple functions.
Then we show that the conditional expectation is a contraction on simple functions, i.e. ‹∥E(s|F)(x)∥ ≤ E(∥s(x)∥|F)› for ‹μ›-almost all ‹x ∈ Ω› with ‹s : Ω → E› simple and integrable.
Using this, we can show that the conditional expectation of a convergent sequence of simple functions is again convergent.
Finally, we show that this limit exhibits the properties of a conditional expectation.
This approach has the benefit of being straightforward and easy to implement, since we could make use of the existing formalization for real-valued functions.
To use the construction in \cite{Hytoenen_2016} we need more tools from functional analysis, which Isabelle/HOL currently does not have.›
text ‹Before we can talk about 'the' conditional expectation, we must define what it means for a function to have a conditional expectation.›
definition has_cond_exp :: "'a measure ⇒ 'a measure ⇒ ('a ⇒ 'b) ⇒ ('a ⇒ 'b::{real_normed_vector, second_countable_topology}) ⇒ bool" where
"has_cond_exp M F f g = ((∀A ∈ sets F. (∫ x ∈ A. f x ∂M) = (∫ x ∈ A. g x ∂M))
∧ integrable M f
∧ integrable M g
∧ g ∈ borel_measurable F)"
text ‹This predicate precisely characterizes what it means for a function \<^term>‹f› to have a conditional expectation \<^term>‹g›,
with respect to the measure \<^term>‹M› and the sub-‹σ›-algebra \<^term>‹F›.›
lemma has_cond_expI':
assumes "⋀A. A ∈ sets F ⟹ (∫ x ∈ A. f x ∂M) = (∫ x ∈ A. g x ∂M)"
"integrable M f"
"integrable M g"
"g ∈ borel_measurable F"
shows "has_cond_exp M F f g"
using assms unfolding has_cond_exp_def by simp
lemma has_cond_expD:
assumes "has_cond_exp M F f g"
shows "⋀A. A ∈ sets F ⟹ (∫ x ∈ A. f x ∂M) = (∫ x ∈ A. g x ∂M)"
"integrable M f"
"integrable M g"
"g ∈ borel_measurable F"
using assms unfolding has_cond_exp_def by simp+
text ‹Now we can use Hilbert’s ‹ϵ›-operator to define the conditional expectation, if it exists.›
definition cond_exp :: "'a measure ⇒ 'a measure ⇒ ('a ⇒ 'b) ⇒ ('a ⇒ 'b::{banach, second_countable_topology})" where
"cond_exp M F f = (if ∃g. has_cond_exp M F f g then (SOME g. has_cond_exp M F f g) else (λ_. 0))"
lemma borel_measurable_cond_exp[measurable]: "cond_exp M F f ∈ borel_measurable F"
by (metis cond_exp_def someI has_cond_exp_def borel_measurable_const)
lemma integrable_cond_exp[intro]: "integrable M (cond_exp M F f)"
by (metis cond_exp_def has_cond_expD(3) integrable_zero someI)
lemma set_integrable_cond_exp[intro]:
assumes "A ∈ sets M"
shows "set_integrable M A (cond_exp M F f)" using integrable_mult_indicator[OF assms integrable_cond_exp, of F f] by (auto simp add: set_integrable_def intro!: integrable_mult_indicator[OF assms integrable_cond_exp])
lemma has_cond_exp_self:
assumes "integrable M f"
shows "has_cond_exp M (vimage_algebra (space M) f borel) f f"
using assms by (auto intro!: has_cond_expI' measurable_vimage_algebra1)
lemma has_cond_exp_sets_cong:
assumes "sets F = sets G"
shows "has_cond_exp M F = has_cond_exp M G"
using assms unfolding has_cond_exp_def by force
lemma cond_exp_sets_cong:
assumes "sets F = sets G"
shows "AE x in M. cond_exp M F f x = cond_exp M G f x"
by (intro AE_I2, simp add: cond_exp_def has_cond_exp_sets_cong[OF assms, of M])
context sigma_finite_subalgebra
begin
lemma borel_measurable_cond_exp'[measurable]: "cond_exp M F f ∈ borel_measurable M"
by (metis cond_exp_def someI has_cond_exp_def borel_measurable_const subalg measurable_from_subalg)
lemma cond_exp_null:
assumes "∄g. has_cond_exp M F f g"
shows "cond_exp M F f = (λ_. 0)"
unfolding cond_exp_def using assms by argo
text ‹We state the tower property of the conditional expectation in terms of the predicate \<^term>‹has_cond_exp›.›
lemma has_cond_exp_nested_subalg:
fixes f :: "'a ⇒ 'b::{second_countable_topology, banach}"
assumes "subalgebra G F" "has_cond_exp M F f h" "has_cond_exp M G f h'"
shows "has_cond_exp M F h' h"
by (intro has_cond_expI') (metis assms has_cond_expD in_mono subalgebra_def)+
text ‹The following lemma shows that the conditional expectation is unique as an element of L1, given that it exists.›
lemma has_cond_exp_charact:
fixes f :: "'a ⇒ 'b::{second_countable_topology, banach}"
assumes "has_cond_exp M F f g"
shows "has_cond_exp M F f (cond_exp M F f)"
"AE x in M. cond_exp M F f x = g x"
proof -
show cond_exp: "has_cond_exp M F f (cond_exp M F f)" using assms someI cond_exp_def by metis
let ?MF = "restr_to_subalg M F"
interpret sigma_finite_measure ?MF by (rule sigma_fin_subalg)
{
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)" using assms subalg by (auto simp add: integral_subalgebra2 set_lebesgue_integral_def dest!: has_cond_expD)
also have "... = (∫x ∈ A. cond_exp M F f x ∂M)" using assms cond_exp by (simp add: has_cond_exp_def)
also have "... = (∫x ∈ A. cond_exp M F f x ∂?MF)" using subalg by (auto simp add: integral_subalgebra2 set_lebesgue_integral_def)
finally have "(∫x ∈ A. g x ∂?MF) = (∫x ∈ A. cond_exp M F f x ∂?MF)" by simp
}
hence "AE x in ?MF. cond_exp M F f x = g x" using cond_exp assms subalg by (intro density_unique_banach, auto dest: has_cond_expD intro!: integrable_in_subalg)
then show "AE x in M. cond_exp M F f x = g x" using AE_restr_to_subalg[OF subalg] by simp
qed
corollary cond_exp_charact:
fixes f :: "'a ⇒ 'b::{second_countable_topology, banach}"
assumes "⋀A. A ∈ sets F ⟹ (∫ x ∈ A. f x ∂M) = (∫ x ∈ A. g x ∂M)"
"integrable M f"
"integrable M g"
"g ∈ borel_measurable F"
shows "AE x in M. cond_exp M F f x = g x"
by (intro has_cond_exp_charact has_cond_expI' assms) auto
text ‹Identity on F-measurable functions:›
text ‹If an integrable function \<^term>‹f› is already \<^term>‹F›-measurable, then \<^term>‹cond_exp M F f = f› ‹μ›-a.e.
This is a corollary of the lemma on the characterization of \<^term>‹cond_exp›.›
corollary cond_exp_F_meas[intro, simp]:
fixes f :: "'a ⇒ 'b::{second_countable_topology, banach}"
assumes "integrable M f"
"f ∈ borel_measurable F"
shows "AE x in M. cond_exp M F f x = f x"
by (rule cond_exp_charact, auto intro: assms)
text ‹Congruence›
lemma has_cond_exp_cong:
assumes "integrable M f" "⋀x. x ∈ space M ⟹ f x = g x" "has_cond_exp M F g h"
shows "has_cond_exp M F f h"
proof (intro has_cond_expI'[OF _ assms(1)])
fix A assume asm: "A ∈ sets F"
hence "set_lebesgue_integral M A f = set_lebesgue_integral M A g" by (intro set_lebesgue_integral_cong) (meson assms(2) subalg in_mono subalgebra_def sets.sets_into_space subalgebra_def subsetD)+
thus "set_lebesgue_integral M A f = set_lebesgue_integral M A h" using asm assms(3) by (simp add: has_cond_exp_def)
qed (auto simp add: has_cond_expD[OF assms(3)])
lemma cond_exp_cong:
fixes f :: "'a ⇒ 'b::{second_countable_topology,banach}"
assumes "integrable M f" "integrable M g" "⋀x. x ∈ space M ⟹ f x = g x"
shows "AE x in M. cond_exp M F f x = cond_exp M F g x"
proof (cases "∃h. has_cond_exp M F f h")
case True
then obtain h where h: "has_cond_exp M F f h" "has_cond_exp M F g h" using has_cond_exp_cong assms by metis
show ?thesis using h[THEN has_cond_exp_charact(2)] by fastforce
next
case False
moreover have "∄h. has_cond_exp M F g h" using False has_cond_exp_cong assms by auto
ultimately show ?thesis unfolding cond_exp_def by auto
qed
lemma has_cond_exp_cong_AE:
assumes "integrable M f" "AE x in M. f x = g x" "has_cond_exp M F g h"
shows "has_cond_exp M F f h"
using assms(1,2) subalg subalgebra_def subset_iff
by (intro has_cond_expI', subst set_lebesgue_integral_cong_AE[OF _ assms(1)[THEN borel_measurable_integrable] borel_measurable_integrable(1)[OF has_cond_expD(2)[OF assms(3)]]])
(fast intro: has_cond_expD[OF assms(3)] integrable_cong_AE_imp[OF _ _ AE_symmetric])+
lemma has_cond_exp_cong_AE':
assumes "h ∈ borel_measurable F" "AE x in M. h x = h' x" "has_cond_exp M F f h'"
shows "has_cond_exp M F f h"
using assms(1, 2) subalg subalgebra_def subset_iff
using AE_restr_to_subalg2[OF subalg assms(2)] measurable_from_subalg
by (intro has_cond_expI' , subst set_lebesgue_integral_cong_AE[OF _ measurable_from_subalg(1,1)[OF subalg], OF _ assms(1) has_cond_expD(4)[OF assms(3)]])
(fast intro: has_cond_expD[OF assms(3)] integrable_cong_AE_imp[OF _ _ AE_symmetric])+
lemma cond_exp_cong_AE:
fixes f :: "'a ⇒ 'b::{second_countable_topology,banach}"
assumes "integrable M f" "integrable M g" "AE x in M. f x = g x"
shows "AE x in M. cond_exp M F f x = cond_exp M F g x"
proof (cases "∃h. has_cond_exp M F f h")
case True
then obtain h where h: "has_cond_exp M F f h" "has_cond_exp M F g h" using has_cond_exp_cong_AE assms by (metis (mono_tags, lifting) eventually_mono)
show ?thesis using h[THEN has_cond_exp_charact(2)] by fastforce
next
case False
moreover have "∄h. has_cond_exp M F g h" using False has_cond_exp_cong_AE assms by auto
ultimately show ?thesis unfolding cond_exp_def by auto
qed
text ‹The conditional expectation operator on the reals, \<^term>‹real_cond_exp›, satisfies the conditions of the conditional expectation as we have defined it.›
lemma has_cond_exp_real:
fixes f :: "'a ⇒ real"
assumes "integrable M f"
shows "has_cond_exp M F f (real_cond_exp M F f)"
by (intro has_cond_expI', auto intro!: real_cond_exp_intA assms)
lemma cond_exp_real[intro]:
fixes f :: "'a ⇒ real"
assumes "integrable M f"
shows "AE x in M. cond_exp M F f x = real_cond_exp M F f x"
using has_cond_exp_charact has_cond_exp_real assms by blast
lemma cond_exp_cmult:
fixes f :: "'a ⇒ real"
assumes "integrable M f"
shows "AE x in M. cond_exp M F (λx. c * f x) x = c * cond_exp M F f x"
using real_cond_exp_cmult[OF assms(1), of c] assms(1)[THEN cond_exp_real] assms(1)[THEN integrable_mult_right, THEN cond_exp_real, of c] by fastforce
subsection ‹Existence›
text ‹Showing the existence is a bit involved. Specifically, what we aim to show is that \<^term>‹has_cond_exp M F f (cond_exp M F f)› holds for any Bochner-integrable \<^term>‹f›.
We will employ the standard machinery of measure theory. First, we will prove existence for indicator functions.
Then we will extend our proof by linearity to simple functions.
Finally we use a limiting argument to show that the conditional expectation exists for all Bochner-integrable functions.›
text ‹Indicator functions›
lemma has_cond_exp_indicator:
assumes "A ∈ sets M" "emeasure M A < ∞"
shows "has_cond_exp M F (λx. indicat_real A x *⇩R y) (λx. real_cond_exp M F (indicator A) x *⇩R y)"
proof (intro has_cond_expI', goal_cases)
case (1 B)
have "(∫x∈B. (indicat_real A x *⇩R y) ∂M) = (∫x∈B. indicat_real A x ∂M) *⇩R y" using assms by (intro set_integral_scaleR_left, meson 1 in_mono subalg subalgebra_def, blast)
also have "... = (∫x∈B. real_cond_exp M F (indicator A) x ∂M) *⇩R y" using 1 assms by (subst real_cond_exp_intA, auto)
also have "... = (∫x∈B. (real_cond_exp M F (indicator A) x *⇩R y) ∂M)" using assms by (intro set_integral_scaleR_left[symmetric], meson 1 in_mono subalg subalgebra_def, blast)
finally show ?case .
next
case 2
show ?case using integrable_scaleR_left integrable_real_indicator assms by blast
next
case 3
show ?case using assms by (intro integrable_scaleR_left, intro real_cond_exp_int, blast+)
next
case 4
show ?case by (intro borel_measurable_scaleR, intro Conditional_Expectation.borel_measurable_cond_exp, simp)
qed
lemma cond_exp_indicator[intro]:
fixes y :: "'b::{second_countable_topology,banach}"
assumes [measurable]: "A ∈ sets M" "emeasure M A < ∞"
shows "AE x in M. cond_exp M F (λx. indicat_real A x *⇩R y) x = cond_exp M F (indicator A) x *⇩R y"
proof -
have "AE x in M. cond_exp M F (λx. indicat_real A x *⇩R y) x = real_cond_exp M F (indicator A) x *⇩R y" using has_cond_exp_indicator[OF assms] has_cond_exp_charact by blast
thus ?thesis using cond_exp_real[OF integrable_real_indicator, OF assms] by fastforce
qed
text ‹Addition›
lemma has_cond_exp_add:
fixes f g :: "'a ⇒ 'b::{second_countable_topology,banach}"
assumes "has_cond_exp M F f f'" "has_cond_exp M F g g'"
shows "has_cond_exp M F (λx. f x + g x) (λx. f' x + g' x)"
proof (intro has_cond_expI', goal_cases)
case (1 A)
have "(∫x∈A. (f x + g x)∂M) = (∫x∈A. f x ∂M) + (∫x∈A. g x ∂M)" using assms[THEN has_cond_expD(2)] subalg 1 by (intro set_integral_add(2), auto simp add: subalgebra_def set_integrable_def intro: integrable_mult_indicator)
also have "... = (∫x∈A. f' x ∂M) + (∫x∈A. g' x ∂M)" using assms[THEN has_cond_expD(1)[OF _ 1]] by argo
also have "... = (∫x∈A. (f' x + g' x)∂M)" using assms[THEN has_cond_expD(3)] subalg 1 by (intro set_integral_add(2)[symmetric], auto simp add: subalgebra_def set_integrable_def intro: integrable_mult_indicator)
finally show ?case .
next
case 2
show ?case by (metis Bochner_Integration.integrable_add assms has_cond_expD(2))
next
case 3
show ?case by (metis Bochner_Integration.integrable_add assms has_cond_expD(3))
next
case 4
show ?case using assms borel_measurable_add has_cond_expD(4) by blast
qed
lemma has_cond_exp_scaleR_right:
fixes f :: "'a ⇒ 'b::{second_countable_topology,banach}"
assumes "has_cond_exp M F f f'"
shows "has_cond_exp M F (λx. c *⇩R f x) (λx. c *⇩R f' x)"
using has_cond_expD[OF assms] by (intro has_cond_expI', auto)
lemma cond_exp_scaleR_right:
fixes f :: "'a ⇒ 'b::{second_countable_topology,banach}"
assumes "integrable M f"
shows "AE x in M. cond_exp M F (λx. c *⇩R f x) x = c *⇩R cond_exp M F f x"
proof (cases "∃f'. has_cond_exp M F f f'")
case True
then show ?thesis using assms has_cond_exp_charact has_cond_exp_scaleR_right by metis
next
case False
show ?thesis
proof (cases "c = 0")
case True
then show ?thesis by simp
next
case c_nonzero: False
have "∄f'. has_cond_exp M F (λx. c *⇩R f x) f'"
proof (standard, goal_cases)
case 1
then obtain f' where f': "has_cond_exp M F (λx. c *⇩R f x) f'" by blast
have "has_cond_exp M F f (λx. inverse c *⇩R f' x)" using has_cond_expD[OF f'] divideR_right[OF c_nonzero] assms by (intro has_cond_expI', auto)
then show ?case using False by blast
qed
then show ?thesis using cond_exp_null[OF False] cond_exp_null by force
qed
qed
lemma cond_exp_uminus:
fixes f :: "'a ⇒ 'b::{second_countable_topology,banach}"
assumes "integrable M f"
shows "AE x in M. cond_exp M F (λx. - f x) x = - cond_exp M F f x"
using cond_exp_scaleR_right[OF assms, of "-1"] by force
text ‹Together with the induction scheme ‹integrable_simple_function_induct›, we can show that the conditional expectation of an integrable simple function exists.›
corollary has_cond_exp_simple:
fixes f :: "'a ⇒ 'b::{second_countable_topology,banach}"
assumes "simple_function M f" "emeasure M {y ∈ space M. f y ≠ 0} ≠ ∞"
shows "has_cond_exp M F f (cond_exp M F f)"
using assms
proof (induction rule: integrable_simple_function_induct)
case (cong f g)
then show ?case using has_cond_exp_cong by (metis (no_types, opaque_lifting) Bochner_Integration.integrable_cong has_cond_expD(2) has_cond_exp_charact(1))
next
case (indicator A y)
then show ?case using has_cond_exp_charact[OF has_cond_exp_indicator] by fast
next
case (add u v)
then show ?case using has_cond_exp_add has_cond_exp_charact(1) by blast
qed
text ‹Now comes the most difficult part. Given a convergent sequence of integrable simple functions \<^term>‹λn. s n›,
we must show that the sequence \<^term>‹λn. cond_exp M F (s n)› is also convergent. Furthermore, we must show that this limit satisfies the properties of a conditional expectation.
Unfortunately, we will only be able to show that this sequence convergences in the L1-norm.
Luckily, this is enough to show that the operator \<^term>‹cond_exp M F› preserves limits as a function from L1 to L1.›
text ‹In anticipation of this result, we show that the conditional expectation operator is a contraction for simple functions.
We first reformulate the lemma ‹real_cond_exp_abs›, which shows the statement for real-valued functions, using our definitions.
Then we show the statement for simple functions via induction.›
lemma cond_exp_contraction_real:
fixes f :: "'a ⇒ real"
assumes integrable[measurable]: "integrable M f"
shows "AE x in M. norm (cond_exp M F f x) ≤ cond_exp M F (λx. norm (f x)) x"
proof-
have int: "integrable M (λx. norm (f x))" using assms by blast
have *: "AE x in M. 0 ≤ cond_exp M F (λx. norm (f x)) x" using cond_exp_real[THEN AE_symmetric, OF integrable_norm[OF integrable]] real_cond_exp_ge_c[OF integrable_norm[OF integrable], of 0] norm_ge_zero by fastforce
have **: "A ∈ sets F ⟹ (∫x∈A. ¦f x¦ ∂M) = (∫x∈A. real_cond_exp M F (λx. norm (f x)) x ∂M)" for A unfolding real_norm_def using assms integrable_abs real_cond_exp_intA by blast
have norm_int: "A ∈ sets F ⟹ (∫x∈A. ¦f x¦ ∂M) = (∫⇧+x∈A. ¦f x¦ ∂M)" for A using assms by (intro nn_set_integral_eq_set_integral[symmetric], blast, fastforce) (meson subalg subalgebra_def subsetD)
have "AE x in M. real_cond_exp M F (λx. norm (f x)) x ≥ 0" using int real_cond_exp_ge_c by force
hence cond_exp_norm_int: "A ∈ sets F ⟹ (∫x∈A. real_cond_exp M F (λx. norm (f x)) x ∂M) = (∫⇧+x∈A. real_cond_exp M F (λx. norm (f x)) x ∂M)" for A using assms by (intro nn_set_integral_eq_set_integral[symmetric], blast, fastforce) (meson subalg subalgebra_def subsetD)
have "A ∈ sets F ⟹ (∫⇧+x∈A. ¦f x¦∂M) = (∫⇧+x∈A. real_cond_exp M F (λx. norm (f x)) x ∂M)" for A using ** norm_int cond_exp_norm_int by (auto simp add: nn_integral_set_ennreal)
moreover have "(λx. ennreal ¦f x¦) ∈ borel_measurable M" by measurable
moreover have "(λx. ennreal (real_cond_exp M F (λx. norm (f x)) x)) ∈ borel_measurable F" by measurable
ultimately have "AE x in M. nn_cond_exp M F (λx. ennreal ¦f x¦) x = real_cond_exp M F (λx. norm (f x)) x" by (intro nn_cond_exp_charact[THEN AE_symmetric], auto)
hence "AE x in M. nn_cond_exp M F (λx. ennreal ¦f x¦) x ≤ cond_exp M F (λx. norm (f x)) x" using cond_exp_real[OF int] by force
moreover have "AE x in M. ¦real_cond_exp M F f x¦ = norm (cond_exp M F f x)" unfolding real_norm_def using cond_exp_real[OF assms] * by force
ultimately have "AE x in M. ennreal (norm (cond_exp M F f x)) ≤ cond_exp M F (λx. norm (f x)) x" using real_cond_exp_abs[OF assms[THEN borel_measurable_integrable]] by fastforce
hence "AE x in M. enn2real (ennreal (norm (cond_exp M F f x))) ≤ enn2real (cond_exp M F (λx. norm (f x)) x)" using ennreal_le_iff2 by force
thus ?thesis using * by fastforce
qed
lemma cond_exp_contraction_simple:
fixes f :: "'a ⇒ 'b::{second_countable_topology, banach}"
assumes "simple_function M f" "emeasure M {y ∈ space M. f y ≠ 0} ≠ ∞"
shows "AE x in M. norm (cond_exp M F f x) ≤ cond_exp M F (λx. norm (f x)) x"
using assms
proof (induction rule: integrable_simple_function_induct)
case (cong f g)
hence ae: "AE x in M. f x = g x" by blast
hence "AE x in M. cond_exp M F f x = cond_exp M F g x" using cong has_cond_exp_simple by (subst cond_exp_cong_AE) (auto intro!: has_cond_expD(2))
hence "AE x in M. norm (cond_exp M F f x) = norm (cond_exp M F g x)" by force
moreover have "AE x in M. cond_exp M F (λx. norm (f x)) x = cond_exp M F (λx. norm (g x)) x" using ae cong has_cond_exp_simple by (subst cond_exp_cong_AE) (auto dest: has_cond_expD)
ultimately show ?case using cong(6) by fastforce
next
case (indicator A y)
hence "AE x in M. cond_exp M F (λa. indicator A a *⇩R y) x = cond_exp M F (indicator A) x *⇩R y" by blast
hence *: "AE x in M. norm (cond_exp M F (λa. indicat_real A a *⇩R y) x) ≤ norm y * cond_exp M F (λx. norm (indicat_real A x)) x" using cond_exp_contraction_real[OF integrable_real_indicator, OF indicator] by fastforce
have "AE x in M. norm y * cond_exp M F (λx. norm (indicat_real A x)) x = norm y * real_cond_exp M F (λx. norm (indicat_real A x)) x" using cond_exp_real[OF integrable_real_indicator, OF indicator] by fastforce
moreover have "AE x in M. cond_exp M F (λx. norm y * norm (indicat_real A x)) x = real_cond_exp M F (λx. norm y * norm (indicat_real A x)) x" using indicator by (intro cond_exp_real, auto)
ultimately have "AE x in M. norm y * cond_exp M F (λx. norm (indicat_real A x)) x = cond_exp M F (λx. norm y * norm (indicat_real A x)) x" using real_cond_exp_cmult[of "λx. norm (indicat_real A x)" "norm y"] indicator by fastforce
moreover have "(λx. norm y * norm (indicat_real A x)) = (λx. norm (indicat_real A x *⇩R y))" by force
ultimately show ?case using * by force
next
case (add u v)
have "AE x in M. norm (cond_exp M F (λa. u a + v a) x) = norm (cond_exp M F u x + cond_exp M F v x)" using has_cond_exp_charact(2)[OF has_cond_exp_add, OF has_cond_exp_simple(1,1), OF add(1,2,3,4)] by fastforce
moreover have "AE x in M. norm (cond_exp M F u x + cond_exp M F v x) ≤ norm (cond_exp M F u x) + norm (cond_exp M F v x)" using norm_triangle_ineq by blast
moreover have "AE x in M. norm (cond_exp M F u x) + norm (cond_exp M F v x) ≤ cond_exp M F (λx. norm (u x)) x + cond_exp M F (λx. norm (v x)) x" using add(6,7) by fastforce
moreover have "AE x in M. cond_exp M F (λx. norm (u x)) x + cond_exp M F (λx. norm (v x)) x = cond_exp M F (λx. norm (u x) + norm (v x)) x" using integrable_simple_function[OF add(1,2)] integrable_simple_function[OF add(3,4)] by (intro has_cond_exp_charact(2)[OF has_cond_exp_add[OF has_cond_exp_charact(1,1)], THEN AE_symmetric], auto intro: has_cond_exp_real)
moreover have "AE x in M. cond_exp M F (λx. norm (u x) + norm (v x)) x = cond_exp M F (λx. norm (u x + v x)) x" using add(5) integrable_simple_function[OF add(1,2)] integrable_simple_function[OF add(3,4)] by (intro cond_exp_cong, auto)
ultimately show ?case by force
qed
lemma has_cond_exp_simple_lim:
fixes f :: "'a ⇒ 'b::{second_countable_topology, banach}"
assumes integrable[measurable]: "integrable M f"
and "⋀i. simple_function M (s i)"
and "⋀i. emeasure M {y ∈ space M. s i y ≠ 0} ≠ ∞"
and "⋀x. x ∈ space M ⟹ (λi. s i x) ⇢ f x"
and "⋀x i. x ∈ space M ⟹ norm (s i x) ≤ 2 * norm (f x)"
obtains r
where "strict_mono r" "has_cond_exp M F f (λx. lim (λi. cond_exp M F (s (r i)) x))"
"AE x in M. convergent (λi. cond_exp M F (s (r i)) x)"
proof -
have [measurable]: "(s i) ∈ borel_measurable M" for i using assms(2) by (simp add: borel_measurable_simple_function)
have integrable_s: "integrable M (λx. s i x)" for i using assms integrable_simple_function by blast
have integrable_4f: "integrable M (λx. 4 * norm (f x))" using assms(1) by simp
have integrable_2f: "integrable M (λx. 2 * norm (f x))" using assms(1) by simp
have integrable_2_cond_exp_norm_f: "integrable M (λx. 2 * cond_exp M F (λx. norm (f x)) x)" by fast
have "emeasure M {y ∈ space M. s i y - s j y ≠ 0} ≤ emeasure M {y ∈ space M. s i y ≠ 0} + emeasure M {y ∈ space M. s j y ≠ 0}" for i j using simple_functionD(2)[OF assms(2)] by (intro order_trans[OF emeasure_mono emeasure_subadditive], auto)
hence fin_sup: "emeasure M {y ∈ space M. s i y - s j y ≠ 0} ≠ ∞" for i j using assms(3) by (metis (mono_tags) ennreal_add_eq_top linorder_not_less top.not_eq_extremum infinity_ennreal_def)
have "emeasure M {y ∈ space M. norm (s i y - s j y) ≠ 0} ≤ emeasure M {y ∈ space M. s i y ≠ 0} + emeasure M {y ∈ space M. s j y ≠ 0}" for i j using simple_functionD(2)[OF assms(2)] by (intro order_trans[OF emeasure_mono emeasure_subadditive], auto)
hence fin_sup_norm: "emeasure M {y ∈ space M. norm (s i y - s j y) ≠ 0} ≠ ∞" for i j using assms(3) by (metis (mono_tags) ennreal_add_eq_top linorder_not_less top.not_eq_extremum infinity_ennreal_def)
have Cauchy: "Cauchy (λn. s n x)" if "x ∈ space M" for x using assms(4) LIMSEQ_imp_Cauchy that by blast
hence bounded_range_s: "bounded (range (λn. s n x))" if "x ∈ space M" for x using that cauchy_imp_bounded by fast
text ‹Since the sequence \<^term>‹(λn. s n x)› is Cauchy for almost all \<^term>‹x›, we know that the diameter tends to zero almost everywhere.›
text ‹Dominated convergence tells us that the integral of the diameter also converges to zero.›
have "AE x in M. (λn. diameter {s i x | i. n ≤ i}) ⇢ 0" using Cauchy cauchy_iff_diameter_tends_to_zero_and_bounded by fast
moreover have "(λx. diameter {s i x |i. n ≤ i}) ∈ borel_measurable M" for n using bounded_range_s borel_measurable_diameter by measurable
moreover have "AE x in M. norm (diameter {s i x |i. n ≤ i}) ≤ 4 * norm (f x)" for n
proof -
{
fix x assume x: "x ∈ space M"
have "diameter {s i x |i. n ≤ i} ≤ 2 * norm (f x) + 2 * norm (f x)" by (intro diameter_le, blast, subst dist_norm[symmetric], intro dist_triangle3[THEN order_trans, of 0], intro add_mono) (auto intro: assms(5)[OF x])
hence "norm (diameter {s i x |i. n ≤ i}) ≤ 4 * norm (f x)" using diameter_ge_0[OF bounded_subset[OF bounded_range_s], OF x, of "{s i x |i. n ≤ i}"] by force
}
thus ?thesis by fast
qed
ultimately have diameter_tendsto_zero: "(λn. LINT x|M. diameter {s i x | i. n ≤ i}) ⇢ 0" by (intro integral_dominated_convergence[OF borel_measurable_const[of 0] _ integrable_4f, simplified]) (fast+)
have diameter_integrable: "integrable M (λx. diameter {s i x | i. n ≤ i})" for n using assms(1,5)
by (intro integrable_bound_diameter[OF bounded_range_s integrable_2f], auto)
have dist_integrable: "integrable M (λx. dist (s i x) (s j x))" for i j using assms(5) dist_triangle3[of "s i _" _ 0, THEN order_trans, OF add_mono, of _ "2 * norm (f _)"]
by (intro Bochner_Integration.integrable_bound[OF integrable_4f]) fastforce+
text ‹Since \<^term>‹cond_exp M F› is a contraction for simple functions, the following sequence of integral values is also Cauchy.›
text ‹This follows, since the distance between the terms of this sequence are always less than or equal to the diameter, which itself converges to zero.›
text ‹Hence, we obtain a subsequence which is Cauchy almost everywhere.›
have "∃N. ∀i≥N. ∀j≥N. LINT x|M. norm (cond_exp M F (s i) x - cond_exp M F (s j) x) < e" if e_pos: "e > 0" for e
proof -
obtain N where *: "LINT x|M. diameter {s i x | i. n ≤ i} < e" if "n ≥ N" for n using that order_tendsto_iff[THEN iffD1, OF diameter_tendsto_zero, unfolded eventually_sequentially] e_pos by presburger
{
fix i j x assume asm: "i ≥ N" "j ≥ N" "x ∈ space M"
have "case_prod dist ` ({s i x |i. N ≤ i} × {s i x |i. N ≤ i}) = case_prod (λi j. dist (s i x) (s j x)) ` ({N..} × {N..})" by fast
hence "diameter {s i x | i. N ≤ i} = (SUP (i, j) ∈ {N..} × {N..}. dist (s i x) (s j x))" unfolding diameter_def by auto
moreover have "(SUP (i, j) ∈ {N..} × {N..}. dist (s i x) (s j x)) ≥ dist (s i x) (s j x)" using asm bounded_imp_bdd_above[OF bounded_imp_dist_bounded, OF bounded_range_s] by (intro cSup_upper, auto)
ultimately have "diameter {s i x | i. N ≤ i} ≥ dist (s i x) (s j x)" by presburger
}
hence "LINT x|M. dist (s i x) (s j x) < e" if "i ≥ N" "j ≥ N" for i j using that * by (intro integral_mono[OF dist_integrable diameter_integrable, THEN order.strict_trans1], blast+)
moreover have "LINT x|M. norm (cond_exp M F (s i) x - cond_exp M F (s j) x) ≤ LINT x|M. dist (s i x) (s j x)" for i j
proof -
have "LINT x|M. norm (cond_exp M F (s i) x - cond_exp M F (s j) x) = LINT x|M. norm (cond_exp M F (s i) x + - 1 *⇩R cond_exp M F (s j) x)" unfolding dist_norm by simp
also have "... = LINT x|M. norm (cond_exp M F (λx. s i x - s j x) x)" using has_cond_exp_charact(2)[OF has_cond_exp_add[OF _ has_cond_exp_scaleR_right, OF has_cond_exp_charact(1,1), OF has_cond_exp_simple(1,1)[OF assms(2,3)]], THEN AE_symmetric, of i "-1" j] by (intro integral_cong_AE) force+
also have "... ≤ LINT x|M. cond_exp M F (λx. norm (s i x - s j x)) x" using cond_exp_contraction_simple[OF _ fin_sup, of i j] integrable_cond_exp assms(2) by (intro integral_mono_AE, fast+)
also have "... = LINT x|M. norm (s i x - s j x)" unfolding set_integral_space(1)[OF integrable_cond_exp, symmetric] set_integral_space[OF dist_integrable[unfolded dist_norm], symmetric] by (intro has_cond_expD(1)[OF has_cond_exp_simple[OF _ fin_sup_norm], symmetric]) (metis assms(2) simple_function_compose1 simple_function_diff, metis sets.top subalg subalgebra_def)
finally show ?thesis unfolding dist_norm .
qed
ultimately show ?thesis using order.strict_trans1 by meson
qed
then obtain r where strict_mono_r: "strict_mono r" and AE_Cauchy: "AE x in M. Cauchy (λi. cond_exp M F (s (r i)) x)"
by (rule cauchy_L1_AE_cauchy_subseq[OF integrable_cond_exp], auto)
hence ae_lim_cond_exp: "AE x in M. (λn. cond_exp M F (s (r n)) x) ⇢ lim (λn. cond_exp M F (s (r n)) x)" using Cauchy_convergent_iff convergent_LIMSEQ_iff by fastforce
text ‹Now that we have a candidate for the conditional expectation, we must show that it actually has the required properties.›
text ‹Dominated convergence shows that this limit is indeed integrable.›
text ‹Here, we again use the fact that conditional expectation is a contraction on simple functions.›
have cond_exp_bounded: "AE x in M. norm (cond_exp M F (s (r n)) x) ≤ cond_exp M F (λx. 2 * norm (f x)) x" for n
proof -
have "AE x in M. norm (cond_exp M F (s (r n)) x) ≤ cond_exp M F (λx. norm (s (r n) x)) x" by (rule cond_exp_contraction_simple[OF assms(2,3)])
moreover have "AE x in M. real_cond_exp M F (λx. norm (s (r n) x)) x ≤ real_cond_exp M F (λx. 2 * norm (f x)) x" using integrable_s integrable_2f assms(5) by (intro real_cond_exp_mono, auto)
ultimately show ?thesis using cond_exp_real[OF integrable_norm, OF integrable_s, of "r n"] cond_exp_real[OF integrable_2f] by force
qed
have lim_integrable: "integrable M (λx. lim (λi. cond_exp M F (s (r i)) x))" by (intro integrable_dominated_convergence[OF _ borel_measurable_cond_exp' integrable_cond_exp ae_lim_cond_exp cond_exp_bounded], simp)
text ‹Moreover, we can use the DCT twice to show that the conditional expectation property holds, i.e. the value of the integral of the candidate, agrees with \<^term>‹f› on sets \<^term>‹A ∈ F›.›
{
fix A assume A_in_sets_F: "A ∈ sets F"
have "AE x in M. norm (indicator A x *⇩R cond_exp M F (s (r n)) x) ≤ cond_exp M F (λx. 2 * norm (f x)) x" for n
proof -
have "AE x in M. norm (indicator A x *⇩R cond_exp M F (s (r n)) x) ≤ norm (cond_exp M F (s (r n)) x)" unfolding indicator_def by simp
thus ?thesis using cond_exp_bounded[of n] by force
qed
hence lim_cond_exp_int: "(λn. LINT x:A|M. cond_exp M F (s (r n)) x) ⇢ (LINT x:A|M. lim (λn. cond_exp M F (s (r n)) x))"
using ae_lim_cond_exp measurable_from_subalg[OF subalg borel_measurable_indicator, OF A_in_sets_F] cond_exp_bounded
unfolding set_lebesgue_integral_def
by (intro integral_dominated_convergence[OF borel_measurable_scaleR borel_measurable_scaleR integrable_cond_exp]) (fastforce simp add: tendsto_scaleR)+
have "AE x in M. norm (indicator A x *⇩R s (r n) x) ≤ 2 * norm (f x)" for n
proof -
have "AE x in M. norm (indicator A x *⇩R s (r n) x) ≤ norm (s (r n) x)" unfolding indicator_def by simp
thus ?thesis using assms(5)[of _ "r n"] by fastforce
qed
hence lim_s_int: "(λn. LINT x:A|M. s (r n) x) ⇢ (LINT x:A|M. f x)"
using measurable_from_subalg[OF subalg borel_measurable_indicator, OF A_in_sets_F] LIMSEQ_subseq_LIMSEQ[OF assms(4) strict_mono_r] assms(5)
unfolding set_lebesgue_integral_def comp_def
by (intro integral_dominated_convergence[OF borel_measurable_scaleR borel_measurable_scaleR integrable_2f]) (fastforce simp add: tendsto_scaleR)+
have "(LINT x:A|M. lim (λn. cond_exp M F (s (r n)) x)) = lim (λn. LINT x:A|M. cond_exp M F (s (r n)) x)" using limI[OF lim_cond_exp_int] by argo
also have "... = lim (λn. LINT x:A|M. s (r n) x)" using has_cond_expD(1)[OF has_cond_exp_simple[OF assms(2,3)] A_in_sets_F, symmetric] by presburger
also have "... = (LINT x:A|M. f x)" using limI[OF lim_s_int] by argo
finally have "(LINT x:A|M. lim (λn. cond_exp M F (s (r n)) x)) = (LINT x:A|M. f x)" .
}
text ‹Putting it all together, we have the statement we are looking for.›
hence "has_cond_exp M F f (λx. lim (λi. cond_exp M F (s (r i)) x))" using assms(1) lim_integrable by (intro has_cond_expI', auto)
thus thesis using AE_Cauchy Cauchy_convergent strict_mono_r by (auto intro!: that)
qed
text ‹Now, we can show that the conditional expectation is well-defined for all integrable functions.›
corollary has_cond_expI:
fixes f :: "'a ⇒ 'b::{second_countable_topology,banach}"
assumes "integrable M f"
shows "has_cond_exp M F f (cond_exp M F f)"
proof -
obtain s where s_is: "⋀i. simple_function M (s i)" "⋀i. emeasure M {y ∈ space M. s i y ≠ 0} ≠ ∞" "⋀x. x ∈ space M ⟹ (λi. s i x) ⇢ f x" "⋀x i. x ∈ space M ⟹ norm (s i x) ≤ 2 * norm (f x)" using integrable_implies_simple_function_sequence[OF assms] by blast
show ?thesis using has_cond_exp_simple_lim[OF assms s_is] has_cond_exp_charact(1) by metis
qed
subsection ‹Properties›
text ‹The defining property of the conditional expectation now always holds, given that the function \<^term>‹f› is integrable.›
lemma cond_exp_set_integral:
fixes f :: "'a ⇒ 'b::{second_countable_topology,banach}"
assumes "integrable M f" "A ∈ sets F"
shows "(∫ x ∈ A. f x ∂M) = (∫ x ∈ A. cond_exp M F f x ∂M)"
using has_cond_expD(1)[OF has_cond_expI, OF assms] by argo
text ‹The following property of the conditional expectation is called the "Tower Property".›
lemma cond_exp_nested_subalg:
fixes f :: "'a ⇒ 'b::{second_countable_topology,banach}"
assumes "integrable M f" "subalgebra M G" "subalgebra G F"
shows "AE ξ in M. cond_exp M F f ξ = cond_exp M F (cond_exp M G f) ξ"
using has_cond_expI assms sigma_finite_subalgebra_def by (auto intro!: has_cond_exp_nested_subalg[THEN has_cond_exp_charact(2), THEN AE_symmetric] sigma_finite_subalgebra.has_cond_expI[OF sigma_finite_subalgebra.intro[OF assms(2)]] nested_subalg_is_sigma_finite)
text ‹The conditional expectation is linear.›
lemma cond_exp_add:
fixes f :: "'a ⇒ 'b::{second_countable_topology,banach}"
assumes "integrable M f" "integrable M g"
shows "AE x in M. cond_exp M F (λx. f x + g x) x = cond_exp M F f x + cond_exp M F g x"
using has_cond_exp_add[OF has_cond_expI(1,1), OF assms, THEN has_cond_exp_charact(2)] .
lemma cond_exp_diff:
fixes f :: "'a ⇒ 'b :: {second_countable_topology, banach}"
assumes "integrable M f" "integrable M g"
shows "AE x in M. cond_exp M F (λx. f x - g x) x = cond_exp M F f x - cond_exp M F g x"
using has_cond_exp_add[OF _ has_cond_exp_scaleR_right, OF has_cond_expI(1,1), OF assms, THEN has_cond_exp_charact(2), of "-1"] by simp
lemma cond_exp_diff':
fixes f :: "'a ⇒ 'b :: {second_countable_topology, banach}"
assumes "integrable M f" "integrable M g"
shows "AE x in M. cond_exp M F (f - g) x = cond_exp M F f x - cond_exp M F g x"
unfolding fun_diff_def using assms by (rule cond_exp_diff)
lemma cond_exp_scaleR_left:
fixes f :: "'a ⇒ real"
assumes "integrable M f"
shows "AE x in M. cond_exp M F (λx. f x *⇩R c) x = cond_exp M F f x *⇩R c"
using cond_exp_set_integral[OF assms] subalg assms unfolding subalgebra_def
by (intro cond_exp_charact,
subst set_integral_scaleR_left, blast, intro assms,
subst set_integral_scaleR_left, blast, intro integrable_cond_exp)
auto
text ‹The conditional expectation operator is a contraction, i.e. a bounded linear operator with operator norm less than or equal to 1.›
text ‹To show this we first obtain a subsequence \<^term>‹λx. (λi. s (r i) x)›, such that \<^term>‹(λi. cond_exp M F (s (r i)) x)› converges to \<^term>‹cond_exp M F f x› a.e.
Afterwards, we obtain a sub-subsequence \<^term>‹λx. (λi. s (r (r' i)) x)›, such that \<^term>‹(λi. cond_exp M F (λx. norm (s (r i))) x)› converges to \<^term>‹cond_exp M F (λx. norm (f x)) x› a.e.
Finally, we show that the inequality holds by showing that the terms of the subsequences obey the inequality and the fact that a subsequence of a convergent sequence converges to the same limit.›
lemma cond_exp_contraction:
fixes f :: "'a ⇒ 'b::{second_countable_topology, banach}"
assumes "integrable M f"
shows "AE x in M. norm (cond_exp M F f x) ≤ cond_exp M F (λx. norm (f x)) x"
proof -
obtain s where s: "⋀i. simple_function M (s i)" "⋀i. emeasure M {y ∈ space M. s i y ≠ 0} ≠ ∞" "⋀x. x ∈ space M ⟹ (λi. s i x) ⇢ f x" "⋀i x. x ∈ space M ⟹ norm (s i x) ≤ 2 * norm (f x)"
by (blast intro: integrable_implies_simple_function_sequence[OF assms])
obtain r where r: "strict_mono r" and "has_cond_exp M F f (λx. lim (λi. cond_exp M F (s (r i)) x))" "AE x in M. (λi. cond_exp M F (s (r i)) x) ⇢ lim (λi. cond_exp M F (s (r i)) x)"
using has_cond_exp_simple_lim[OF assms s] unfolding convergent_LIMSEQ_iff by blast
hence r_tendsto: "AE x in M. (λi. cond_exp M F (s (r i)) x) ⇢ cond_exp M F f x" using has_cond_exp_charact(2) by force
have norm_s_r: "⋀i. simple_function M (λx. norm (s (r i) x))" "⋀i. emeasure M {y ∈ space M. norm (s (r i) y) ≠ 0} ≠ ∞" "⋀x. x ∈ space M ⟹ (λi. norm (s (r i) x)) ⇢ norm (f x)" "⋀i x. x ∈ space M ⟹ norm (norm (s (r i) x)) ≤ 2 * norm (norm (f x))"
using s by (auto intro: LIMSEQ_subseq_LIMSEQ[OF tendsto_norm r, unfolded comp_def] simple_function_compose1)
obtain r' where r': "strict_mono r'" and "has_cond_exp M F (λx. norm (f x)) (λx. lim (λi. cond_exp M F (λx. norm (s (r (r' i)) x)) x))" "AE x in M. (λi. cond_exp M F (λx. norm (s (r (r' i)) x)) x) ⇢ lim (λi. cond_exp M F (λx. norm (s (r (r' i)) x)) x)" using has_cond_exp_simple_lim[OF integrable_norm norm_s_r, OF assms] unfolding convergent_LIMSEQ_iff by blast
hence r'_tendsto: "AE x in M. (λi. cond_exp M F (λx. norm (s (r (r' i)) x)) x) ⇢ cond_exp M F (λx. norm (f x)) x" using has_cond_exp_charact(2) by force
have "AE x in M. ∀i. norm (cond_exp M F (s (r (r' i))) x) ≤ cond_exp M F (λx. norm (s (r (r' i)) x)) x" using s by (auto intro: cond_exp_contraction_simple simp add: AE_all_countable)
moreover have "AE x in M. (λi. norm (cond_exp M F (s (r (r' i))) x)) ⇢ norm (cond_exp M F f x)" using r_tendsto LIMSEQ_subseq_LIMSEQ[OF tendsto_norm r', unfolded comp_def] by fast
ultimately show ?thesis using LIMSEQ_le r'_tendsto by fast
qed
text ‹The following lemmas are called "pulling out whats known". We first show the statement for real-valued functions using the lemma ‹real_cond_exp_intg›, which is already present.
We then show it for arbitrary \<^term>‹g› using the lecture notes of Gordan Zitkovic for the course "Theory of Probability I" \cite{Zitkovic_2015}.›
lemma cond_exp_measurable_mult:
fixes f g :: "'a ⇒ real"
assumes [measurable]: "integrable M (λx. f x * g x)" "integrable M g" "f ∈ borel_measurable F"
shows "integrable M (λx. f x * cond_exp M F g x)"
"AE x in M. cond_exp M F (λx. f x * g x) x = f x * cond_exp M F g x"
proof-
show integrable: "integrable M (λx. f x * cond_exp M F g x)" using cond_exp_real[OF assms(2)] by (intro integrable_cong_AE_imp[OF real_cond_exp_intg(1), OF assms(1,3) assms(2)[THEN borel_measurable_integrable]] measurable_from_subalg[OF subalg]) auto
interpret sigma_finite_measure "restr_to_subalg M F" by (rule sigma_fin_subalg)
{
fix A assume asm: "A ∈ sets F"
hence asm': "A ∈ sets M" using subalg by (fastforce simp add: subalgebra_def)
have "set_lebesgue_integral M A (cond_exp M F (λx. f x * g x)) = set_lebesgue_integral M A (λx. f x * g x)" by (simp add: cond_exp_set_integral[OF assms(1) asm])
also have "... = set_lebesgue_integral M A (λx. f x * real_cond_exp M F g x)" using borel_measurable_times[OF borel_measurable_indicator[OF asm] assms(3)] borel_measurable_integrable[OF assms(2)] integrable_mult_indicator[OF asm' assms(1)] by (fastforce simp add: set_lebesgue_integral_def mult.assoc[symmetric] intro: real_cond_exp_intg(2)[symmetric])
also have "... = set_lebesgue_integral M A (λx. f x * cond_exp M F g x)" using cond_exp_real[OF assms(2)] asm' borel_measurable_cond_exp' borel_measurable_cond_exp2 measurable_from_subalg[OF subalg assms(3)] by (auto simp add: set_lebesgue_integral_def intro: integral_cong_AE)
finally have "set_lebesgue_integral M A (cond_exp M F (λx. f x * g x)) = (∫x∈A. (f x * cond_exp M F g x)∂M)" .
}
hence "AE x in restr_to_subalg M F. cond_exp M F (λx. f x * g x) x = f x * cond_exp M F g x" by (intro density_unique_banach integrable_cond_exp integrable integrable_in_subalg subalg, measurable, simp add: set_lebesgue_integral_def integral_subalgebra2[OF subalg] sets_restr_to_subalg[OF subalg])
thus "AE x in M. cond_exp M F (λx. f x * g x) x = f x * cond_exp M F g x" by (rule AE_restr_to_subalg[OF subalg])
qed
lemma cond_exp_measurable_scaleR:
fixes f :: "'a ⇒ real" and g :: "'a ⇒ 'b :: {second_countable_topology, banach}"
assumes [measurable]: "integrable M (λx. f x *⇩R g x)" "integrable M g" "f ∈ borel_measurable F"
shows "integrable M (λx. f x *⇩R cond_exp M F g x)"
"AE x in M. cond_exp M F (λx. f x *⇩R g x) x = f x *⇩R cond_exp M F g x"
proof -
let ?F = "restr_to_subalg M F"
have subalg': "subalgebra M (restr_to_subalg M F)" by (metis sets_eq_imp_space_eq sets_restr_to_subalg subalg subalgebra_def)
{
fix z assume asm[measurable]: "integrable M (λx. z x *⇩R g x)" "z ∈ borel_measurable ?F"
hence asm'[measurable]: "z ∈ borel_measurable F" using measurable_in_subalg' subalg by blast
have "integrable M (λx. z x *⇩R cond_exp M F g x)" "LINT x|M. z x *⇩R g x = LINT x|M. z x *⇩R cond_exp M F g x"
proof -
obtain s where s_is: "⋀i. simple_function ?F (s i)" "⋀x. x ∈ space ?F ⟹ (λi. s i x) ⇢ z x" "⋀i x. x ∈ space ?F ⟹ norm (s i x) ≤ 2 * norm (z x)" using borel_measurable_implies_sequence_metric[OF asm(2), of 0] by force
text ‹We need to apply the dominated convergence theorem twice, therefore we need to show the following prerequisites.›
have s_scaleR_g_tendsto: "AE x in M. (λi. s i x *⇩R g x) ⇢ z x *⇩R g x" using s_is(2) by (simp add: space_restr_to_subalg tendsto_scaleR)
have s_scaleR_cond_exp_g_tendsto: "AE x in ?F. (λi. s i x *⇩R cond_exp M F g x) ⇢ z x *⇩R cond_exp M F g x" using s_is(2) by (simp add: tendsto_scaleR)
have s_scaleR_g_meas: "(λx. s i x *⇩R g x) ∈ borel_measurable M" for i using s_is(1)[THEN borel_measurable_simple_function, THEN subalg'[THEN measurable_from_subalg]] by simp
have s_scaleR_cond_exp_g_meas: "(λx. s i x *⇩R cond_exp M F g x) ∈ borel_measurable ?F" for i using s_is(1)[THEN borel_measurable_simple_function] measurable_in_subalg[OF subalg borel_measurable_cond_exp] by (fastforce intro: borel_measurable_scaleR)
have s_scaleR_g_AE_bdd: "AE x in M. norm (s i x *⇩R g x) ≤ 2 * norm (z x *⇩R g x)" for i using s_is(3) by (fastforce simp add: space_restr_to_subalg mult.assoc[symmetric] mult_right_mono)
{
fix i
have asm: "integrable M (λx. norm (z x) * norm (g x))" using asm(1)[THEN integrable_norm] by simp
have "AE x in ?F. norm (s i x *⇩R cond_exp M F g x) ≤ 2 * norm (z x) * norm (cond_exp M F g x)" using s_is(3) by (fastforce simp add: mult_mono)
moreover have "AE x in ?F. norm (z x) * cond_exp M F (λx. norm (g x)) x = cond_exp M F (λx. norm (z x) * norm (g x)) x" by (rule cond_exp_measurable_mult(2)[THEN AE_symmetric, OF asm integrable_norm, OF assms(2), THEN AE_restr_to_subalg2[OF subalg]], auto)
ultimately have "AE x in ?F. norm (s i x *⇩R cond_exp M F g x) ≤ 2 * cond_exp M F (λx. norm (z x *⇩R g x)) x" using cond_exp_contraction[OF assms(2), THEN AE_restr_to_subalg2[OF subalg]] order_trans[OF _ mult_mono] by fastforce
}
note s_scaleR_cond_exp_g_AE_bdd = this
text ‹In the following section we need to pay attention to which measures we are using for integration. The rhs is F-measurable while the lhs is only M-measurable.›
{
fix i
have s_meas_M[measurable]: "s i ∈ borel_measurable M" by (meson borel_measurable_simple_function measurable_from_subalg s_is(1) subalg')
have s_meas_F[measurable]: "s i ∈ borel_measurable F" by (meson borel_measurable_simple_function measurable_in_subalg' s_is(1) subalg)
have s_scaleR_eq: "s i x *⇩R h x = (∑y∈s i ` space M. (indicator (s i -` {y} ∩ space M) x *⇩R y) *⇩R h x)" if "x ∈ space M" for x and h :: "'a ⇒ 'b"
using simple_function_indicator_representation_banach[OF s_is(1), of x i] that unfolding space_restr_to_subalg scaleR_left.sum[of _ _ "h x", symmetric] by presburger
have "LINT x|M. s i x *⇩R g x = LINT x|M. (∑y∈s i ` space M. indicator (s i -` {y} ∩ space M) x *⇩R y *⇩R g x)" using s_scaleR_eq by (intro Bochner_Integration.integral_cong) auto
also have "... = (∑y∈s i ` space M. LINT x|M. indicator (s i -` {y} ∩ space M) x *⇩R y *⇩R g x)" by (intro Bochner_Integration.integral_sum integrable_mult_indicator[OF _ integrable_scaleR_right] assms(2)) simp
also have "... = (∑y∈s i ` space M. y *⇩R set_lebesgue_integral M (s i -` {y} ∩ space M) g)" by (simp only: set_lebesgue_integral_def[symmetric]) simp
also have "... = (∑y∈s i ` space M. y *⇩R set_lebesgue_integral M (s i -` {y} ∩ space M) (cond_exp M F g))" using assms(2) subalg borel_measurable_vimage[OF s_meas_F] by (subst cond_exp_set_integral, auto simp add: subalgebra_def)
also have "... = (∑y∈s i ` space M. LINT x|M. indicator (s i -` {y} ∩ space M) x *⇩R y *⇩R cond_exp M F g x)" by (simp only: set_lebesgue_integral_def[symmetric]) simp
also have "... = LINT x|M. (∑y∈s i ` space M. indicator (s i -` {y} ∩ space M) x *⇩R y *⇩R cond_exp M F g x)" by (intro Bochner_Integration.integral_sum[symmetric] integrable_mult_indicator[OF _ integrable_scaleR_right]) auto
also have "... = LINT x|M. s i x *⇩R cond_exp M F g x" using s_scaleR_eq by (intro Bochner_Integration.integral_cong) auto
finally have "LINT x|M. s i x *⇩R g x = LINT x|?F. s i x *⇩R cond_exp M F g x" by (simp add: integral_subalgebra2[OF subalg])
}
note integral_s_eq = this
text ‹Now we just plug in the results we obtained into DCT, and use the fact that limits are unique.›
show "integrable M (λx. z x *⇩R cond_exp M F g x)" using s_scaleR_cond_exp_g_meas asm(2) borel_measurable_cond_exp' by (intro integrable_from_subalg[OF subalg] integrable_cond_exp integrable_dominated_convergence[OF _ _ _ s_scaleR_cond_exp_g_tendsto s_scaleR_cond_exp_g_AE_bdd]) (auto intro: measurable_from_subalg[OF subalg] integrable_in_subalg measurable_in_subalg subalg)
have "(λi. LINT x|M. s i x *⇩R g x) ⇢ LINT x|M. z x *⇩R g x" using s_scaleR_g_meas asm(1)[THEN integrable_norm] asm' borel_measurable_cond_exp' by (intro integral_dominated_convergence[OF _ _ _ s_scaleR_g_tendsto s_scaleR_g_AE_bdd]) (auto intro: measurable_from_subalg[OF subalg])
moreover have "(λi. LINT x|?F. s i x *⇩R cond_exp M F g x) ⇢ LINT x|?F. z x *⇩R cond_exp M F g x" using s_scaleR_cond_exp_g_meas asm(2) borel_measurable_cond_exp' by (intro integral_dominated_convergence[OF _ _ _ s_scaleR_cond_exp_g_tendsto s_scaleR_cond_exp_g_AE_bdd]) (auto intro: measurable_from_subalg[OF subalg] integrable_in_subalg measurable_in_subalg subalg)
ultimately show "LINT x|M. z x *⇩R g x = LINT x|M. z x *⇩R cond_exp M F g x" using integral_s_eq using subalg by (simp add: LIMSEQ_unique integral_subalgebra2)
qed
}
note * = this
text ‹The main statement now follows with \<^term>‹z = (λx. indicator A x * f x)›.›
show "integrable M (λx. f x *⇩R cond_exp M F g x)" using * assms measurable_in_subalg[OF subalg] by blast
{
fix A assume asm: "A ∈ F"
hence "integrable M (λx. indicat_real A x *⇩R f x *⇩R g x)" using subalg by (fastforce simp add: subalgebra_def intro!: integrable_mult_indicator assms(1))
hence "set_lebesgue_integral M A (λx. f x *⇩R g x) = set_lebesgue_integral M A (λx. f x *⇩R cond_exp M F g x)" unfolding set_lebesgue_integral_def using asm by (auto intro!: * measurable_in_subalg[OF subalg])
}
thus "AE x in M. cond_exp M F (λx. f x *⇩R g x) x = f x *⇩R cond_exp M F g x" using borel_measurable_cond_exp by (intro cond_exp_charact, auto intro!: * assms measurable_in_subalg[OF subalg])
qed
lemma cond_exp_sum [intro, simp]:
fixes f :: "'t ⇒ 'a ⇒ 'b :: {second_countable_topology,banach}"
assumes [measurable]: "⋀i. integrable M (f i)"
shows "AE x in M. cond_exp M F (λx. ∑i∈I. f i x) x = (∑i∈I. cond_exp M F (f i) x)"
proof (rule has_cond_exp_charact, intro has_cond_expI')
fix A assume [measurable]: "A ∈ sets F"
then have A_meas [measurable]: "A ∈ sets M" by (meson subsetD subalg subalgebra_def)
have "(∫x∈A. (∑i∈I. f i x)∂M) = (∫x. (∑i∈I. indicator A x *⇩R f i x)∂M)" unfolding set_lebesgue_integral_def by (simp add: scaleR_sum_right)
also have "... = (∑i∈I. (∫x. indicator A x *⇩R f i x ∂M))" using assms by (auto intro!: Bochner_Integration.integral_sum integrable_mult_indicator)
also have "... = (∑i∈I. (∫x. indicator A x *⇩R cond_exp M F (f i) x ∂M))" using cond_exp_set_integral[OF assms] by (simp add: set_lebesgue_integral_def)
also have "... = (∫x. (∑i∈I. indicator A x *⇩R cond_exp M F (f i) x)∂M)" using assms by (auto intro!: Bochner_Integration.integral_sum[symmetric] integrable_mult_indicator)
also have "... = (∫x∈A. (∑i∈I. cond_exp M F (f i) x)∂M)" unfolding set_lebesgue_integral_def by (simp add: scaleR_sum_right)
finally show "(∫x∈A. (∑i∈I. f i x)∂M) = (∫x∈A. (∑i∈I. cond_exp M F (f i) x)∂M)" by auto
qed (auto simp add: assms integrable_cond_exp)
subsection ‹Linearly Ordered Banach Spaces›
text ‹In this subsection we show monotonicity results concerning the conditional expectation operator.›
lemma cond_exp_gr_c:
fixes f :: "'a ⇒ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}"
assumes "integrable M f" "AE x in M. f x > c"
shows "AE x in M. cond_exp M F f x > c"
proof -
define X where "X = {x ∈ space M. cond_exp M F f x ≤ c}"
have [measurable]: "X ∈ sets F" unfolding X_def by measurable (metis sets.top subalg subalgebra_def)
hence X_in_M: "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)
hence "emeasure (restr_to_subalg M F) X > 0" using ‹¬(emeasure M X) = 0› gr_zeroI by auto
then obtain A where A: "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)
hence [simp]: "A ∈ sets F" using subalg sets_restr_to_subalg by blast
hence A_in_sets_M[simp]: "A ∈ sets M" using sets_restr_to_subalg subalg subalgebra_def by blast
have [simp]: "set_integrable M A (λx. c)" using A subalg by (auto simp add: set_integrable_def emeasure_restr_to_subalg)
have [simp]: "set_integrable M A f" unfolding set_integrable_def by (rule integrable_mult_indicator, auto simp add: assms(1))
have "AE x in M. indicator A x *⇩R c = indicator A x *⇩R f x"
proof (rule integral_eq_mono_AE_eq_AE)
have "(∫x∈A. c ∂M) ≤ (∫x∈A. f x ∂M)" using assms(2) by (intro set_integral_mono_AE_banach) auto
moreover
{
have "(∫x∈A. f x ∂M) = (∫x∈A. cond_exp M F f x ∂M)" by (rule cond_exp_set_integral, auto simp add: assms)
also have "... ≤ (∫x∈A. c ∂M)" using A by (auto intro!: set_integral_mono_banach simp add: X_def)
finally have "(∫x∈A. f x ∂M) ≤ (∫x∈A. c ∂M)" by simp
}
ultimately show "LINT x|M. indicator A x *⇩R c = LINT x|M. indicator A x *⇩R f x" unfolding set_lebesgue_integral_def by simp
show "AE x in M. indicator A x *⇩R c ≤ indicator A x *⇩R f x" using assms by (auto simp add: X_def indicator_def)
qed (auto simp add: set_integrable_def[symmetric])
hence "AE x∈A in M. c = f x" by auto
hence "AE x∈A in M. False" using assms(2) by auto
hence "A ∈ null_sets M" using AE_iff_null_sets A_in_sets_M by metis
thus False using A(3) by (simp add: emeasure_restr_to_subalg null_setsD1 subalg)
qed
thus ?thesis using AE_iff_null_sets[OF X_in_M] unfolding X_def by auto
qed
corollary cond_exp_less_c:
fixes f :: "'a ⇒ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}"
assumes "integrable M f" "AE x in M. f x < c"
shows "AE x in M. cond_exp M F f x < c"
proof -
have "AE x in M. cond_exp M F f x = - cond_exp M F (λx. - f x) x" using cond_exp_uminus[OF assms(1)] by auto
moreover have "AE x in M. cond_exp M F (λx. - f x) x > - c" using assms by (intro cond_exp_gr_c) auto
ultimately show ?thesis by (force simp add: minus_less_iff)
qed
lemma cond_exp_mono_strict:
fixes f :: "'a ⇒ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}"
assumes "integrable M f" "integrable M g" "AE x in M. f x < g x"
shows "AE x in M. cond_exp M F f x < cond_exp M F g x"
using cond_exp_less_c[OF Bochner_Integration.integrable_diff, OF assms(1,2), of 0]
cond_exp_diff[OF assms(1,2)] assms(3) by auto
lemma cond_exp_ge_c:
fixes f :: "'a ⇒ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}"
assumes [measurable]: "integrable M f"
and "AE x in M. f x ≥ c"
shows "AE x in M. cond_exp M F f x ≥ c"
proof -
let ?F = "restr_to_subalg M F"
interpret sigma_finite_measure "restr_to_subalg M F" using sigma_fin_subalg by auto
{
fix A assume asm: "A ∈ sets ?F" "0 < measure ?F A"
have [simp]: "sets ?F = sets F" "measure ?F A = measure M A" using asm by (auto simp add: measure_def sets_restr_to_subalg[OF subalg] emeasure_restr_to_subalg[OF subalg])
have M_A: "emeasure M A < ∞" using measure_zero_top asm by (force simp add: top.not_eq_extremum)
hence F_A: "emeasure ?F A < ∞" using asm(1) emeasure_restr_to_subalg subalg by fastforce
have "set_lebesgue_integral M A (λ_. c) ≤ set_lebesgue_integral M A f" using assms asm M_A subalg by (intro set_integral_mono_AE_banach, auto simp add: set_integrable_def integrable_mult_indicator subalgebra_def sets_restr_to_subalg)
also have "... = set_lebesgue_integral M A (cond_exp M F f)" using cond_exp_set_integral[OF assms(1)] asm by auto
also have "... = set_lebesgue_integral ?F A (cond_exp M F f)" unfolding set_lebesgue_integral_def using asm borel_measurable_cond_exp by (intro integral_subalgebra2[OF subalg, symmetric], simp)
finally have "(1 / measure ?F A) *⇩R set_lebesgue_integral ?F A (cond_exp M F f) ∈ {c..}" using asm subalg M_A by (auto simp add: set_integral_const subalgebra_def intro!: pos_divideR_le_eq[THEN iffD1])
}
thus ?thesis using AE_restr_to_subalg[OF subalg] averaging_theorem[OF integrable_in_subalg closed_atLeast, OF subalg borel_measurable_cond_exp integrable_cond_exp] by auto
qed
corollary cond_exp_le_c:
fixes f :: "'a ⇒ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}"
assumes "integrable M f"
and "AE x in M. f x ≤ c"
shows "AE x in M. cond_exp M F f x ≤ c"
proof -
have "AE x in M. cond_exp M F f x = - cond_exp M F (λx. - f x) x" using cond_exp_uminus[OF assms(1)] by force
moreover have "AE x in M. cond_exp M F (λx. - f x) x ≥ - c" using assms by (intro cond_exp_ge_c) auto
ultimately show ?thesis by (force simp add: minus_le_iff)
qed
corollary cond_exp_mono:
fixes f :: "'a ⇒ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}"
assumes "integrable M f" "integrable M g" "AE x in M. f x ≤ g x"
shows "AE x in M. cond_exp M F f x ≤ cond_exp M F g x"
using cond_exp_le_c[OF Bochner_Integration.integrable_diff, OF assms(1,2), of 0]
cond_exp_diff[OF assms(1,2)] assms(3) by auto
corollary cond_exp_min:
fixes f :: "'a ⇒ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}"
assumes "integrable M f" "integrable M g"
shows "AE ξ in M. cond_exp M F (λx. min (f x) (g x)) ξ ≤ min (cond_exp M F f ξ) (cond_exp M F g ξ)"
proof -
have "AE ξ in M. cond_exp M F (λx. min (f x) (g x)) ξ ≤ cond_exp M F f ξ" by (intro cond_exp_mono integrable_min assms, simp)
moreover have "AE ξ in M. cond_exp M F (λx. min (f x) (g x)) ξ ≤ cond_exp M F g ξ" by (intro cond_exp_mono integrable_min assms, simp)
ultimately show "AE ξ in M. cond_exp M F (λx. min (f x) (g x)) ξ ≤ min (cond_exp M F f ξ) (cond_exp M F g ξ)" by fastforce
qed
corollary cond_exp_max:
fixes f :: "'a ⇒ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}"
assumes "integrable M f" "integrable M g"
shows "AE ξ in M. cond_exp M F (λx. max (f x) (g x)) ξ ≥ max (cond_exp M F f ξ) (cond_exp M F g ξ)"
proof -
have "AE ξ in M. cond_exp M F (λx. max (f x) (g x)) ξ ≥ cond_exp M F f ξ" by (intro cond_exp_mono integrable_max assms, simp)
moreover have "AE ξ in M. cond_exp M F (λx. max (f x) (g x)) ξ ≥ cond_exp M F g ξ" by (intro cond_exp_mono integrable_max assms, simp)
ultimately show "AE ξ in M. cond_exp M F (λx. max (f x) (g x)) ξ ≥ max (cond_exp M F f ξ) (cond_exp M F g ξ)" by fastforce
qed
corollary cond_exp_inf:
fixes f :: "'a ⇒ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector, lattice}"
assumes "integrable M f" "integrable M g"
shows "AE ξ in M. cond_exp M F (λx. inf (f x) (g x)) ξ ≤ inf (cond_exp M F f ξ) (cond_exp M F g ξ)"
unfolding inf_min using assms by (rule cond_exp_min)
corollary cond_exp_sup:
fixes f :: "'a ⇒ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector, lattice}"
assumes "integrable M f" "integrable M g"
shows "AE ξ in M. cond_exp M F (λx. sup (f x) (g x)) ξ ≥ sup (cond_exp M F f ξ) (cond_exp M F g ξ)"
unfolding sup_max using assms by (rule cond_exp_max)
end
subsection ‹Probability Spaces›
lemma (in prob_space) sigma_finite_subalgebra_restr_to_subalg:
assumes "subalgebra M F"
shows "sigma_finite_subalgebra M F"
proof (intro sigma_finite_subalgebra.intro)
interpret F: prob_space "restr_to_subalg M F" using assms prob_space_restr_to_subalg prob_space_axioms by blast
show "sigma_finite_measure (restr_to_subalg M F)" by (rule F.sigma_finite_measure_axioms)
qed (rule assms)
lemma (in prob_space) cond_exp_trivial:
fixes f :: "'a ⇒ 'b :: {second_countable_topology, banach}"
assumes "integrable M f"
shows "AE x in M. cond_exp M (sigma (space M) {}) f x = expectation f"
proof -
interpret sigma_finite_subalgebra M "sigma (space M) {}" by (auto intro: sigma_finite_subalgebra_restr_to_subalg simp add: subalgebra_def sigma_sets_empty_eq)
show ?thesis using assms by (intro cond_exp_charact) (auto simp add: sigma_sets_empty_eq set_lebesgue_integral_def prob_space cong: Bochner_Integration.integral_cong)
qed
text ‹The following lemma shows that independent ‹σ›-algebras don't matter for the conditional expectation. The proof is adapted from \cite{Zitkovic_2015}.›
lemma (in prob_space) cond_exp_indep_subalgebra:
fixes f :: "'a ⇒ 'b :: {second_countable_topology, banach, real_normed_field}"
assumes subalgebra: "subalgebra M F" "subalgebra M G"
and independent: "indep_set G (sigma (space M) (F ∪ vimage_algebra (space M) f borel))"
assumes [measurable]: "integrable M f"
shows "AE x in M. cond_exp M (sigma (space M) (F ∪ G)) f x = cond_exp M F f x"
proof -
interpret Un_sigma: sigma_finite_subalgebra M "sigma (space M) (F ∪ G)" using assms(1,2) by (auto intro!: sigma_finite_subalgebra_restr_to_subalg sets.sigma_sets_subset simp add: subalgebra_def space_measure_of_conv sets_measure_of_conv)
interpret sigma_finite_subalgebra M F using assms by (auto intro: sigma_finite_subalgebra_restr_to_subalg)
{
fix A
assume asm: "A ∈ sigma (space M) {a ∩ b | a b. a ∈ F ∧ b ∈ G}"
have in_events: "sigma_sets (space M) {a ∩ b |a b. a ∈ sets F ∧ b ∈ sets G} ⊆ events" using subalgebra by (intro sets.sigma_sets_subset, auto simp add: subalgebra_def)
have "Int_stable {a ∩ b | a b. a ∈ F ∧ b ∈ G}"
proof -
{
fix af bf ag bg
assume F: "af ∈ F" "bf ∈ F" and G: "ag ∈ G" "bg ∈ G"
have "af ∩ bf ∈ F" by (intro sets.Int F)
moreover have "ag ∩ bg ∈ G" by (intro sets.Int G)
ultimately have "∃a b. af ∩ ag ∩ (bf ∩ bg) = a ∩ b ∧ a ∈ sets F ∧ b ∈ sets G" by (metis inf_assoc inf_left_commute)
}
thus ?thesis by (force intro!: Int_stableI)
qed
moreover have "{a ∩ b | a b. a ∈ F ∧ b ∈ G} ⊆ Pow (space M)" using subalgebra by (force simp add: subalgebra_def dest: sets.sets_into_space)
moreover have "A ∈ sigma_sets (space M) {a ∩ b | a b. a ∈ F ∧ b ∈ G}" using calculation asm by force
ultimately have "set_lebesgue_integral M A f = set_lebesgue_integral M A (cond_exp M F f)"
proof (induction rule: sigma_sets_induct_disjoint)
case (basic A)
then obtain a b where A: "A = a ∩ b" "a ∈ F" "b ∈ G" by blast
hence events[measurable]: "a ∈ events" "b ∈ events" using subalgebra by (auto simp add: subalgebra_def)
have [simp]: "sigma_sets (space M) {indicator b -` A ∩ space M |A. A ∈ borel} ⊆ G"
using borel_measurable_indicator[OF A(3), THEN measurable_sets] sets.top subalgebra
by (intro sets.sigma_sets_subset') (fastforce simp add: subalgebra_def)+
have Un_in_sigma: "F ∪ vimage_algebra (space M) f borel ⊆ sigma (space M) (F ∪ vimage_algebra (space M) f borel)" by (metis equalityE le_supI sets.space_closed sigma_le_sets space_vimage_algebra subalg subalgebra_def)
have [intro]: "indep_var borel (indicator b) borel (λω. indicator a ω *⇩R f ω)"
proof -
have [simp]: "sigma_sets (space M) {(λω. indicator a ω *⇩R f ω) -` A ∩ space M |A. A ∈ borel} ⊆ sigma (space M) (F ∪ vimage_algebra (space M) f borel)"
proof -
have *: "(λω. indicator a ω *⇩R f ω) ∈ borel_measurable (sigma (space M) (F ∪ vimage_algebra (space M) f borel))"
using borel_measurable_indicator[OF A(2), THEN measurable_sets, OF borel_open] subalgebra
by (intro borel_measurable_scaleR borel_measurableI Un_in_sigma[THEN subsetD])
(auto simp add: space_measure_of_conv subalgebra_def sets_vimage_algebra2)
thus ?thesis using measurable_sets[OF *] by (intro sets.sigma_sets_subset', auto simp add: space_measure_of_conv)
qed
have "indep_set (sigma_sets (space M) {indicator b -` A ∩ space M |A. A ∈ borel}) (sigma_sets (space M) {(λω. indicator a ω *⇩R f ω) -` A ∩ space M |A. A ∈ borel})"
using independent unfolding indep_set_def by (rule indep_sets_mono_sets, auto split: bool.split)
thus ?thesis by (subst indep_var_eq, auto intro!: borel_measurable_scaleR)
qed
have [intro]: "indep_var borel (indicator b) borel (λω. indicat_real a ω *⇩R cond_exp M F f ω)"
proof -
have [simp]:"sigma_sets (space M) {(λω. indicator a ω *⇩R cond_exp M F f ω) -` A ∩ space M |A. A ∈ borel} ⊆ sigma (space M) (F ∪ vimage_algebra (space M) f borel)"
proof -
have *: "(λω. indicator a ω *⇩R cond_exp M F f ω) ∈ borel_measurable (sigma (space M) (F ∪ vimage_algebra (space M) f borel))"
using borel_measurable_indicator[OF A(2), THEN measurable_sets, OF borel_open] subalgebra
borel_measurable_cond_exp[THEN measurable_sets, OF borel_open, of _ M F f]
by (intro borel_measurable_scaleR borel_measurableI Un_in_sigma[THEN subsetD])
(auto simp add: space_measure_of_conv subalgebra_def)
thus ?thesis using measurable_sets[OF *] by (intro sets.sigma_sets_subset', auto simp add: space_measure_of_conv)
qed
have "indep_set (sigma_sets (space M) {indicator b -` A ∩ space M |A. A ∈ borel}) (sigma_sets (space M) {(λω. indicator a ω *⇩R cond_exp M F f ω) -` A ∩ space M |A. A ∈ borel})"
using independent unfolding indep_set_def by (rule indep_sets_mono_sets, auto split: bool.split)
thus ?thesis by (subst indep_var_eq, auto intro!: borel_measurable_scaleR)
qed
have "set_lebesgue_integral M A f = (LINT x|M. indicator b x * (indicator a x *⇩R f x))"
unfolding set_lebesgue_integral_def A indicator_inter_arith
by (intro Bochner_Integration.integral_cong, auto simp add: scaleR_scaleR[symmetric] indicator_times_eq_if(1))
also have "... = (LINT x|M. indicator b x) * (LINT x|M. indicator a x *⇩R f x)"
by (intro indep_var_lebesgue_integral
Bochner_Integration.integrable_bound[OF integrable_const[of "1 :: 'b"] borel_measurable_indicator]
integrable_mult_indicator[OF _ assms(4)], blast) (auto simp add: indicator_def)
also have "... = (LINT x|M. indicator b x) * (LINT x|M. indicator a x *⇩R cond_exp M F f x)"
using cond_exp_set_integral[OF assms(4) A(2)] unfolding set_lebesgue_integral_def by argo
also have "... = (LINT x|M. indicator b x * (indicator a x *⇩R cond_exp M F f x))"
by (intro indep_var_lebesgue_integral[symmetric]
Bochner_Integration.integrable_bound[OF integrable_const[of "1 :: 'b"] borel_measurable_indicator]
integrable_mult_indicator[OF _ integrable_cond_exp], blast) (auto simp add: indicator_def)
also have "... = set_lebesgue_integral M A (cond_exp M F f)"
unfolding set_lebesgue_integral_def A indicator_inter_arith
by (intro Bochner_Integration.integral_cong, auto simp add: scaleR_scaleR[symmetric] indicator_times_eq_if(1))
finally show ?case .
next
case empty
then show ?case unfolding set_lebesgue_integral_def by simp
next
case (compl A)
have A_in_space: "A ⊆ space M" using compl using in_events sets.sets_into_space by blast
have "set_lebesgue_integral M (space M - A) f = set_lebesgue_integral M (space M - A ∪ A) f - set_lebesgue_integral M A f"
using compl(1) in_events
by (subst set_integral_Un[of "space M - A" A], blast)
(simp | intro integrable_mult_indicator[folded set_integrable_def, OF _ assms(4)], fast)+
also have "... = set_lebesgue_integral M (space M - A ∪ A) (cond_exp M F f) - set_lebesgue_integral M A (cond_exp M F f)"
using cond_exp_set_integral[OF assms(4) sets.top] compl subalgebra by (simp add: subalgebra_def Un_absorb2[OF A_in_space])
also have "... = set_lebesgue_integral M (space M - A) (cond_exp M F f)"
using compl(1) in_events
by (subst set_integral_Un[of "space M - A" A], blast)
(simp | intro integrable_mult_indicator[folded set_integrable_def, OF _ integrable_cond_exp], fast)+
finally show ?case .
next
case (union A)
have "set_lebesgue_integral M (⋃ (range A)) f = (∑i. set_lebesgue_integral M (A i) f)"
using union in_events
by (intro lebesgue_integral_countable_add) (auto simp add: disjoint_family_onD intro!: integrable_mult_indicator[folded set_integrable_def, OF _ assms(4)])
also have "... = (∑i. set_lebesgue_integral M (A i) (cond_exp M F f))" using union by presburger
also have "... = set_lebesgue_integral M (⋃ (range A)) (cond_exp M F f)"
using union in_events
by (intro lebesgue_integral_countable_add[symmetric]) (auto simp add: disjoint_family_onD intro!: integrable_mult_indicator[folded set_integrable_def, OF _ integrable_cond_exp])
finally show ?case .
qed
}
moreover have "sigma (space M) {a ∩ b | a b. a ∈ F ∧ b ∈ G} = sigma (space M) (F ∪ G)"
proof -
have "sigma_sets (space M) {a ∩ b |a b. a ∈ sets F ∧ b ∈ sets G} = sigma_sets (space M) (sets F ∪ sets G)"
proof -
{
fix a b assume asm: "a ∈ F" "b ∈ G"
hence "a ∩ b ∈ sigma_sets (space M) (F ∪ G)" using subalgebra unfolding Int_range_binary by (intro sigma_sets_Inter[OF _ binary_in_sigma_sets]) (force simp add: subalgebra_def dest: sets.sets_into_space)+
}
moreover
{
fix a
assume "a ∈ sets F"
hence "a ∈ sigma_sets (space M) {a ∩ b |a b. a ∈ sets F ∧ b ∈ sets G}"
using subalgebra sets.top[of G] sets.sets_into_space[of _ F]
by (intro sigma_sets.Basic, auto simp add: subalgebra_def)
}
moreover
{
fix a assume "a ∈ sets F ∨ a ∈ sets G" "a ∉ sets F"
hence "a ∈ sets G" by blast
hence "a ∈ sigma_sets (space M) {a ∩ b |a b. a ∈ sets F ∧ b ∈ sets G}"
using subalgebra sets.top[of F] sets.sets_into_space[of _ G]
by (intro sigma_sets.Basic, auto simp add: subalgebra_def)
}
ultimately show ?thesis by (intro sigma_sets_eqI) auto
qed
thus ?thesis using subalgebra by (intro sigma_eqI) (force simp add: subalgebra_def dest: sets.sets_into_space)+
qed
moreover have "(cond_exp M F f) ∈ borel_measurable (sigma (space M) (sets F ∪ sets G))"
proof -
have "F ⊆ sigma (space M) (F ∪ G)" by (metis Un_least Un_upper1 measure_of_of_measure sets.space_closed sets_measure_of sigma_sets_subseteq subalg subalgebra(2) subalgebra_def)
thus ?thesis using borel_measurable_cond_exp[THEN measurable_sets, OF borel_open, of _ M F f] subalgebra by (intro borel_measurableI, force simp only: space_measure_of_conv subalgebra_def)
qed
ultimately show ?thesis using assms(4) integrable_cond_exp by (intro Un_sigma.cond_exp_charact) presburger+
qed
text ‹If a random variable is independent of a ‹σ›-algebra \<^term>‹F›, its conditional expectation \<^term>‹cond_exp M F f› is just its expectation.›
lemma (in prob_space) cond_exp_indep:
fixes f :: "'a ⇒ 'b :: {second_countable_topology, banach, real_normed_field}"
assumes subalgebra: "subalgebra M F"
and independent: "indep_set F (vimage_algebra (space M) f borel)"
and integrable: "integrable M f"
shows "AE x in M. cond_exp M F f x = expectation f"
proof -
have "indep_set F (sigma (space M) (sigma (space M) {} ∪ (vimage_algebra (space M) f borel)))"
using independent unfolding indep_set_def
by (rule indep_sets_mono_sets, simp add: bool.split)
(metis bot.extremum dual_order.refl sets.sets_measure_of_eq sets.sigma_sets_subset' sets_vimage_algebra_space space_vimage_algebra sup.absorb_iff2)
hence cond_exp_indep: "AE x in M. cond_exp M (sigma (space M) (sigma (space M) {} ∪ F)) f x = expectation f"
using cond_exp_indep_subalgebra[OF _ subalgebra _ integrable, of "sigma (space M) {}"] cond_exp_trivial[OF integrable]
by (auto simp add: subalgebra_def sigma_sets_empty_eq)
have "sets (sigma (space M) (sigma (space M) {} ∪ F)) = F"
using subalgebra sets.top[of F] unfolding subalgebra_def
by (simp add: sigma_sets_empty_eq, subst insert_absorb[of "space M" F], blast)
(metis insert_absorb[OF sets.empty_sets] sets.sets_measure_of_eq)
hence "AE x in M. cond_exp M (sigma (space M) (sigma (space M) {} ∪ F)) f x = cond_exp M F f x" by (rule cond_exp_sets_cong)
thus ?thesis using cond_exp_indep by force
qed
end