Conditional expectation in L2 #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file contains one step of the construction of the conditional expectation, which is completed
in measure_theory.function.conditional_expectation.basic. See that file for a description of the
full process.
We build the conditional expectation of an L² function, as an element of L². This is the
orthogonal projection on the subspace of almost everywhere m-measurable functions.
Main definitions #
condexp_L2: Conditional expectation of a function in L2 with respect to a sigma-algebra: it is the orthogonal projection on the subspaceLp_meas.
Implementation notes #
Most of the results in this file are valid for a complete real normed space F.
However, some lemmas also use 𝕜 : is_R_or_C:
condexp_L2is defined only for aninner_product_spacefor now, and we use𝕜for its field.- results about scalar multiplication are stated not only for
ℝbut also for𝕜if we happen to havenormed_space 𝕜 F.
noncomputable
def
measure_theory.condexp_L2
{α : Type u_1}
{E : Type u_2}
(𝕜 : Type u_7)
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[complete_space E]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0) :
↥(measure_theory.Lp E 2 μ) →L[𝕜] ↥(measure_theory.Lp_meas E 𝕜 m 2 μ)
Conditional expectation of a function in L2 with respect to a sigma-algebra
Equations
- measure_theory.condexp_L2 𝕜 hm = orthogonal_projection (measure_theory.Lp_meas E 𝕜 m 2 μ)
theorem
measure_theory.ae_strongly_measurable'_condexp_L2
{α : Type u_1}
{E : Type u_2}
{𝕜 : Type u_7}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[complete_space E]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp E 2 μ)) :
theorem
measure_theory.integrable_on_condexp_L2_of_measure_ne_top
{α : Type u_1}
{E : Type u_2}
{𝕜 : Type u_7}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[complete_space E]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(hm : m ≤ m0)
(hμs : ⇑μ s ≠ ⊤)
(f : ↥(measure_theory.Lp E 2 μ)) :
measure_theory.integrable_on ⇑(⇑(measure_theory.condexp_L2 𝕜 hm) f) s μ
theorem
measure_theory.integrable_condexp_L2_of_is_finite_measure
{α : Type u_1}
{E : Type u_2}
{𝕜 : Type u_7}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[complete_space E]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
[measure_theory.is_finite_measure μ]
{f : ↥(measure_theory.Lp E 2 μ)} :
measure_theory.integrable ⇑(⇑(measure_theory.condexp_L2 𝕜 hm) f) μ
theorem
measure_theory.norm_condexp_L2_le_one
{α : Type u_1}
{E : Type u_2}
{𝕜 : Type u_7}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[complete_space E]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0) :
‖measure_theory.condexp_L2 𝕜 hm‖ ≤ 1
theorem
measure_theory.norm_condexp_L2_le
{α : Type u_1}
{E : Type u_2}
{𝕜 : Type u_7}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[complete_space E]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp E 2 μ)) :
theorem
measure_theory.snorm_condexp_L2_le
{α : Type u_1}
{E : Type u_2}
{𝕜 : Type u_7}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[complete_space E]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp E 2 μ)) :
measure_theory.snorm ⇑(⇑(measure_theory.condexp_L2 𝕜 hm) f) 2 μ ≤ measure_theory.snorm ⇑f 2 μ
theorem
measure_theory.norm_condexp_L2_coe_le
{α : Type u_1}
{E : Type u_2}
{𝕜 : Type u_7}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[complete_space E]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp E 2 μ)) :
theorem
measure_theory.inner_condexp_L2_left_eq_right
{α : Type u_1}
{E : Type u_2}
{𝕜 : Type u_7}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[complete_space E]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
{f g : ↥(measure_theory.Lp E 2 μ)} :
has_inner.inner ↑(⇑(measure_theory.condexp_L2 𝕜 hm) f) g = has_inner.inner f ↑(⇑(measure_theory.condexp_L2 𝕜 hm) g)
theorem
measure_theory.condexp_L2_indicator_of_measurable
{α : Type u_1}
{E : Type u_2}
{𝕜 : Type u_7}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[complete_space E]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(hm : m ≤ m0)
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(c : E) :
↑(⇑(measure_theory.condexp_L2 𝕜 hm) (measure_theory.indicator_const_Lp 2 _ hμs c)) = measure_theory.indicator_const_Lp 2 _ hμs c
theorem
measure_theory.inner_condexp_L2_eq_inner_fun
{α : Type u_1}
{E : Type u_2}
{𝕜 : Type u_7}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[complete_space E]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(f g : ↥(measure_theory.Lp E 2 μ))
(hg : measure_theory.ae_strongly_measurable' m ⇑g μ) :
has_inner.inner ↑(⇑(measure_theory.condexp_L2 𝕜 hm) f) g = has_inner.inner f g
theorem
measure_theory.integral_condexp_L2_eq_of_fin_meas_real
{α : Type u_1}
{𝕜 : Type u_7}
[is_R_or_C 𝕜]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
{hm : m ≤ m0}
(f : ↥(measure_theory.Lp 𝕜 2 μ))
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤) :
theorem
measure_theory.lintegral_nnnorm_condexp_L2_le
{α : Type u_1}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
{hm : m ≤ m0}
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(f : ↥(measure_theory.Lp ℝ 2 μ)) :
theorem
measure_theory.condexp_L2_ae_eq_zero_of_ae_eq_zero
{α : Type u_1}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
{hm : m ≤ m0}
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
{f : ↥(measure_theory.Lp ℝ 2 μ)}
(hf : ⇑f =ᵐ[μ.restrict s] 0) :
theorem
measure_theory.lintegral_nnnorm_condexp_L2_indicator_le_real
{α : Type u_1}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
{hm : m ≤ m0}
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(ht : measurable_set t)
(hμt : ⇑μ t ≠ ⊤) :
theorem
measure_theory.condexp_L2_const_inner
{α : Type u_1}
{E : Type u_2}
{𝕜 : Type u_7}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[complete_space E]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp E 2 μ))
(c : E) :
⇑(⇑(measure_theory.condexp_L2 𝕜 hm) (measure_theory.mem_ℒp.to_Lp (λ (a : α), has_inner.inner c (⇑f a)) _)) =ᵐ[μ] λ (a : α), has_inner.inner c (⇑(⇑(measure_theory.condexp_L2 𝕜 hm) f) a)
condexp_L2 commutes with taking inner products with constants. See the lemma
condexp_L2_comp_continuous_linear_map for a more general result about commuting with continuous
linear maps.
theorem
measure_theory.integral_condexp_L2_eq
{α : Type u_1}
{E' : Type u_3}
{𝕜 : Type u_7}
[is_R_or_C 𝕜]
[normed_add_comm_group E']
[inner_product_space 𝕜 E']
[complete_space E']
[normed_space ℝ E']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp E' 2 μ))
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤) :
condexp_L2 verifies the equality of integrals defining the conditional expectation.
theorem
measure_theory.condexp_L2_comp_continuous_linear_map
{α : Type u_1}
{E' : Type u_3}
(𝕜 : Type u_7)
[is_R_or_C 𝕜]
[normed_add_comm_group E']
[inner_product_space 𝕜 E']
[complete_space E']
[normed_space ℝ E']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{E'' : Type u_8}
(𝕜' : Type u_9)
[is_R_or_C 𝕜']
[normed_add_comm_group E'']
[inner_product_space 𝕜' E'']
[complete_space E'']
[normed_space ℝ E'']
(hm : m ≤ m0)
(T : E' →L[ℝ] E'')
(f : ↥(measure_theory.Lp E' 2 μ)) :
theorem
measure_theory.condexp_L2_indicator_ae_eq_smul
{α : Type u_1}
{E' : Type u_3}
(𝕜 : Type u_7)
[is_R_or_C 𝕜]
[normed_add_comm_group E']
[inner_product_space 𝕜 E']
[complete_space E']
[normed_space ℝ E']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(hm : m ≤ m0)
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : E') :
⇑(⇑(measure_theory.condexp_L2 𝕜 hm) (measure_theory.indicator_const_Lp 2 hs hμs x)) =ᵐ[μ] λ (a : α), ⇑(⇑(measure_theory.condexp_L2 ℝ hm) (measure_theory.indicator_const_Lp 2 hs hμs 1)) a • x
theorem
measure_theory.condexp_L2_indicator_eq_to_span_singleton_comp
{α : Type u_1}
{E' : Type u_3}
(𝕜 : Type u_7)
[is_R_or_C 𝕜]
[normed_add_comm_group E']
[inner_product_space 𝕜 E']
[complete_space E']
[normed_space ℝ E']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(hm : m ≤ m0)
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : E') :
↑(⇑(measure_theory.condexp_L2 𝕜 hm) (measure_theory.indicator_const_Lp 2 hs hμs x)) = (continuous_linear_map.to_span_singleton ℝ x).comp_Lp ↑(⇑(measure_theory.condexp_L2 ℝ hm) (measure_theory.indicator_const_Lp 2 hs hμs 1))
theorem
measure_theory.set_lintegral_nnnorm_condexp_L2_indicator_le
{α : Type u_1}
{E' : Type u_3}
{𝕜 : Type u_7}
[is_R_or_C 𝕜]
[normed_add_comm_group E']
[inner_product_space 𝕜 E']
[complete_space E']
[normed_space ℝ E']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(hm : m ≤ m0)
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : E')
{t : set α}
(ht : measurable_set t)
(hμt : ⇑μ t ≠ ⊤) :
theorem
measure_theory.lintegral_nnnorm_condexp_L2_indicator_le
{α : Type u_1}
{E' : Type u_3}
{𝕜 : Type u_7}
[is_R_or_C 𝕜]
[normed_add_comm_group E']
[inner_product_space 𝕜 E']
[complete_space E']
[normed_space ℝ E']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(hm : m ≤ m0)
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : E')
[measure_theory.sigma_finite (μ.trim hm)] :
theorem
measure_theory.integrable_condexp_L2_indicator
{α : Type u_1}
{E' : Type u_3}
{𝕜 : Type u_7}
[is_R_or_C 𝕜]
[normed_add_comm_group E']
[inner_product_space 𝕜 E']
[complete_space E']
[normed_space ℝ E']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(hm : m ≤ m0)
[measure_theory.sigma_finite (μ.trim hm)]
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : E') :
measure_theory.integrable ⇑(⇑(measure_theory.condexp_L2 𝕜 hm) (measure_theory.indicator_const_Lp 2 hs hμs x)) μ
If the measure μ.trim hm is sigma-finite, then the conditional expectation of a measurable set
with finite measure is integrable.
noncomputable
def
measure_theory.condexp_ind_smul
{α : Type u_1}
{G : Type u_5}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
(hm : m ≤ m0)
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : G) :
↥(measure_theory.Lp G 2 μ)
Conditional expectation of the indicator of a measurable set with finite measure, in L2.
Equations
- measure_theory.condexp_ind_smul hm hs hμs x = ⇑(continuous_linear_map.comp_LpL 2 μ (continuous_linear_map.to_span_singleton ℝ x)) ↑(⇑(measure_theory.condexp_L2 ℝ hm) (measure_theory.indicator_const_Lp 2 hs hμs 1))
theorem
measure_theory.ae_strongly_measurable'_condexp_ind_smul
{α : Type u_1}
{G : Type u_5}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
(hm : m ≤ m0)
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : G) :
measure_theory.ae_strongly_measurable' m ⇑(measure_theory.condexp_ind_smul hm hs hμs x) μ
theorem
measure_theory.condexp_ind_smul_add
{α : Type u_1}
{G : Type u_5}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x y : G) :
measure_theory.condexp_ind_smul hm hs hμs (x + y) = measure_theory.condexp_ind_smul hm hs hμs x + measure_theory.condexp_ind_smul hm hs hμs y
theorem
measure_theory.condexp_ind_smul_smul
{α : Type u_1}
{G : Type u_5}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(c : ℝ)
(x : G) :
measure_theory.condexp_ind_smul hm hs hμs (c • x) = c • measure_theory.condexp_ind_smul hm hs hμs x
theorem
measure_theory.condexp_ind_smul_smul'
{α : Type u_1}
{F : Type u_4}
{𝕜 : Type u_7}
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
{hm : m ≤ m0}
[normed_space ℝ F]
[smul_comm_class ℝ 𝕜 F]
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(c : 𝕜)
(x : F) :
measure_theory.condexp_ind_smul hm hs hμs (c • x) = c • measure_theory.condexp_ind_smul hm hs hμs x
theorem
measure_theory.condexp_ind_smul_ae_eq_smul
{α : Type u_1}
{G : Type u_5}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
(hm : m ≤ m0)
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : G) :
⇑(measure_theory.condexp_ind_smul hm hs hμs x) =ᵐ[μ] λ (a : α), ⇑(⇑(measure_theory.condexp_L2 ℝ hm) (measure_theory.indicator_const_Lp 2 hs hμs 1)) a • x
theorem
measure_theory.set_lintegral_nnnorm_condexp_ind_smul_le
{α : Type u_1}
{G : Type u_5}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
(hm : m ≤ m0)
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : G)
{t : set α}
(ht : measurable_set t)
(hμt : ⇑μ t ≠ ⊤) :
theorem
measure_theory.lintegral_nnnorm_condexp_ind_smul_le
{α : Type u_1}
{G : Type u_5}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
(hm : m ≤ m0)
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : G)
[measure_theory.sigma_finite (μ.trim hm)] :
theorem
measure_theory.integrable_condexp_ind_smul
{α : Type u_1}
{G : Type u_5}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
(hm : m ≤ m0)
[measure_theory.sigma_finite (μ.trim hm)]
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : G) :
measure_theory.integrable ⇑(measure_theory.condexp_ind_smul hm hs hμs x) μ
If the measure μ.trim hm is sigma-finite, then the conditional expectation of a measurable set
with finite measure is integrable.
theorem
measure_theory.condexp_ind_smul_empty
{α : Type u_1}
{G : Type u_5}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[normed_space ℝ G]
{hm : m ≤ m0}
{x : G} :
theorem
measure_theory.set_integral_condexp_L2_indicator
{α : Type u_1}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
{hm : m ≤ m0}
(hs : measurable_set s)
(ht : measurable_set t)
(hμs : ⇑μ s ≠ ⊤)
(hμt : ⇑μ t ≠ ⊤) :
theorem
measure_theory.set_integral_condexp_ind_smul
{α : Type u_1}
{G' : Type u_6}
[normed_add_comm_group G']
[normed_space ℝ G']
[complete_space G']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
{hm : m ≤ m0}
(hs : measurable_set s)
(ht : measurable_set t)
(hμs : ⇑μ s ≠ ⊤)
(hμt : ⇑μ t ≠ ⊤)
(x : G') :
theorem
measure_theory.condexp_L2_indicator_nonneg
{α : Type u_1}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(hm : m ≤ m0)
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
[measure_theory.sigma_finite (μ.trim hm)] :
0 ≤ᵐ[μ] ⇑(⇑(measure_theory.condexp_L2 ℝ hm) (measure_theory.indicator_const_Lp 2 hs hμs 1))
theorem
measure_theory.condexp_ind_smul_nonneg
{α : Type u_1}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
{hm : m ≤ m0}
{E : Type u_2}
[normed_lattice_add_comm_group E]
[normed_space ℝ E]
[ordered_smul ℝ E]
[measure_theory.sigma_finite (μ.trim hm)]
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : E)
(hx : 0 ≤ x) :
0 ≤ᵐ[μ] ⇑(measure_theory.condexp_ind_smul hm hs hμs x)