# mathlib3documentation

measure_theory.function.conditional_expectation.condexp_L2

# 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 subspace Lp_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_L2 is defined only for an inner_product_space for now, and we use 𝕜 for its field.
• results about scalar multiplication are stated not only for ℝ but also for 𝕜 if we happen to have normed_space 𝕜 F.
noncomputable def measure_theory.condexp_L2 {α : Type u_1} {E : Type u_2} (𝕜 : Type u_7) [is_R_or_C 𝕜] [ E] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) :
μ) →L[𝕜] m 2 μ)

Conditional expectation of a function in L2 with respect to a sigma-algebra

Equations
theorem measure_theory.ae_strongly_measurable'_condexp_L2 {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [is_R_or_C 𝕜] [ E] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (f : μ)) :
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 𝕜] [ E] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} (hm : m m0) (hμs : μ s ) (f : μ)) :
μ
theorem measure_theory.integrable_condexp_L2_of_is_finite_measure {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [is_R_or_C 𝕜] [ E] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) {f : μ)} :
μ
theorem measure_theory.norm_condexp_L2_le_one {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [is_R_or_C 𝕜] [ E] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) :
theorem measure_theory.norm_condexp_L2_le {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [is_R_or_C 𝕜] [ E] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (f : μ)) :
theorem measure_theory.snorm_condexp_L2_le {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [is_R_or_C 𝕜] [ E] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (f : μ)) :
2 μ
theorem measure_theory.norm_condexp_L2_coe_le {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [is_R_or_C 𝕜] [ E] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (f : μ)) :
theorem measure_theory.inner_condexp_L2_left_eq_right {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [is_R_or_C 𝕜] [ E] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) {f g : μ)} :
theorem measure_theory.condexp_L2_indicator_of_measurable {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [is_R_or_C 𝕜] [ E] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} (hm : m m0) (hs : measurable_set s) (hμs : μ s ) (c : E) :
( c)) = c
theorem measure_theory.inner_condexp_L2_eq_inner_fun {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [is_R_or_C 𝕜] [ E] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (f g : μ)) (hg : μ) :
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 : μ)) (hs : measurable_set s) (hμs : μ s ) :
(x : α) in s, ( f) x μ = (x : α) in s, f x μ
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 : μ)) :
∫⁻ (x : α) in s, ( f) x‖₊ μ ∫⁻ (x : α) in s, f x‖₊ μ
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 : μ)} (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 ) :
∫⁻ (a : α) in t, ( hμs 1)) a‖₊ μ μ (s t)
theorem measure_theory.condexp_L2_const_inner {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [is_R_or_C 𝕜] [ E] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (f : μ)) (c : E) :
( (measure_theory.mem_ℒp.to_Lp (λ (a : α), (f a)) _)) =ᵐ[μ] λ (a : α), (( 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 𝕜] [ E'] [complete_space E'] [ E'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} (hm : m m0) (f : 2 μ)) (hs : measurable_set s) (hμs : μ s ) :
(x : α) in s, ( f) x μ = (x : α) in s, f x μ

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 𝕜] [ E'] [complete_space E'] [ E'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {E'' : Type u_8} (𝕜' : Type u_9) [is_R_or_C 𝕜'] [ E''] [complete_space E''] [ E''] (hm : m m0) (T : E' →L[] E'') (f : 2 μ)) :
( hm) (T.comp_Lp f)) =ᵐ[μ] (T.comp_Lp ( f))
theorem measure_theory.condexp_L2_indicator_ae_eq_smul {α : Type u_1} {E' : Type u_3} (𝕜 : Type u_7) [is_R_or_C 𝕜] [ E'] [complete_space E'] [ E'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} (hm : m m0) (hs : measurable_set s) (hμs : μ s ) (x : E') :
( hμs x)) =ᵐ[μ] λ (a : α), ( 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 𝕜] [ E'] [complete_space E'] [ E'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} (hm : m m0) (hs : measurable_set s) (hμs : μ s ) (x : E') :
( hμs x)) = ( 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 𝕜] [ E'] [complete_space E'] [ 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 ) :
∫⁻ (a : α) in t, ( hμs x)) a‖₊ μ μ (s t) * x‖₊
theorem measure_theory.lintegral_nnnorm_condexp_L2_indicator_le {α : Type u_1} {E' : Type u_3} {𝕜 : Type u_7} [is_R_or_C 𝕜] [ E'] [complete_space E'] [ 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)] :
∫⁻ (a : α), ( hμs x)) a‖₊ μ μ s * x‖₊
theorem measure_theory.integrable_condexp_L2_indicator {α : Type u_1} {E' : Type u_3} {𝕜 : Type u_7} [is_R_or_C 𝕜] [ E'] [complete_space E'] [ 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') :

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} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [ G] (hm : m m0) (hs : measurable_set s) (hμs : μ s ) (x : G) :
μ)

Conditional expectation of the indicator of a measurable set with finite measure, in L2.

Equations
theorem measure_theory.ae_strongly_measurable'_condexp_ind_smul {α : Type u_1} {G : Type u_5} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [ G] (hm : m m0) (hs : measurable_set s) (hμs : μ s ) (x : G) :
μ
theorem measure_theory.condexp_ind_smul_add {α : Type u_1} {G : Type u_5} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [ G] {hm : m m0} (hs : measurable_set s) (hμs : μ s ) (x y : G) :
hμs (x + y) = hμs x + hμs y
theorem measure_theory.condexp_ind_smul_smul {α : Type u_1} {G : Type u_5} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [ G] {hm : m m0} (hs : measurable_set s) (hμs : μ s ) (c : ) (x : G) :
hμs (c x) = c hμs x
theorem measure_theory.condexp_ind_smul_smul' {α : Type u_1} {F : Type u_4} {𝕜 : Type u_7} [is_R_or_C 𝕜] [ F] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} {hm : m m0} [ F] [ F] (hs : measurable_set s) (hμs : μ s ) (c : 𝕜) (x : F) :
hμs (c x) = c hμs x
theorem measure_theory.condexp_ind_smul_ae_eq_smul {α : Type u_1} {G : Type u_5} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [ G] (hm : m m0) (hs : measurable_set s) (hμs : μ s ) (x : G) :
hμs x) =ᵐ[μ] λ (a : α), ( hμs 1)) a x
theorem measure_theory.set_lintegral_nnnorm_condexp_ind_smul_le {α : Type u_1} {G : Type u_5} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [ G] (hm : m m0) (hs : measurable_set s) (hμs : μ s ) (x : G) {t : set α} (ht : measurable_set t) (hμt : μ t ) :
∫⁻ (a : α) in t, hμs x) a‖₊ μ μ (s t) * x‖₊
theorem measure_theory.lintegral_nnnorm_condexp_ind_smul_le {α : Type u_1} {G : Type u_5} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [ G] (hm : m m0) (hs : measurable_set s) (hμs : μ s ) (x : G) [measure_theory.sigma_finite (μ.trim hm)] :
∫⁻ (a : α), hμs x) a‖₊ μ μ s * x‖₊
theorem measure_theory.integrable_condexp_ind_smul {α : Type u_1} {G : Type u_5} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [ G] (hm : m m0) [measure_theory.sigma_finite (μ.trim hm)] (hs : measurable_set s) (hμs : μ s ) (x : G) :
μ

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} {m m0 : measurable_space α} {μ : measure_theory.measure α} [ 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 ) :
(x : α) in s, ( hμt 1)) x μ = (μ (t s)).to_real
theorem measure_theory.set_integral_condexp_ind_smul {α : Type u_1} {G' : Type u_6} [ 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') :
(a : α) in s, hμt x) a μ = (μ (t s)).to_real x
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 ≤ᵐ[μ] ( 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} [ E] [ E] [measure_theory.sigma_finite (μ.trim hm)] (hs : measurable_set s) (hμs : μ s ) (x : E) (hx : 0 x) :
0 ≤ᵐ[μ] hμs x)