# Documentation

Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

# Conditional expectation in L2 #

This file contains one step of the construction of the conditional expectation, which is completed in MeasureTheory.Function.ConditionalExpectation.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 #

• condexpL2: Conditional expectation of a function in L2 with respect to a sigma-algebra: it is the orthogonal projection on the subspace lpMeas.

## Implementation notes #

Most of the results in this file are valid for a complete real normed space F. However, some lemmas also use 𝕜 : IsROrC:

• condexpL2 is defined only for an InnerProductSpace 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 NormedSpace 𝕜 F.
noncomputable def MeasureTheory.condexpL2 {α : Type u_1} (E : Type u_2) (𝕜 : Type u_7) [] [] [] {m : } {m0 : } {μ : } (hm : m m0) :
{ x // x } →L[𝕜] { x // x MeasureTheory.lpMeas E 𝕜 m 2 μ }

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

Instances For
theorem MeasureTheory.aeStronglyMeasurable'_condexpL2 {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [] [] [] {m : } {m0 : } {μ : } (hm : m m0) (f : { x // x }) :
MeasureTheory.AEStronglyMeasurable' m (↑(↑() f)) μ
theorem MeasureTheory.integrableOn_condexpL2_of_measure_ne_top {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [] [] [] {m : } {m0 : } {μ : } {s : Set α} (hm : m m0) (hμs : μ s ) (f : { x // x }) :
MeasureTheory.IntegrableOn (↑(↑() f)) s
theorem MeasureTheory.integrable_condexpL2_of_isFiniteMeasure {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [] [] [] {m : } {m0 : } {μ : } (hm : m m0) {f : { x // x }} :
MeasureTheory.Integrable ↑(↑() f)
theorem MeasureTheory.norm_condexpL2_le_one {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [] [] [] {m : } {m0 : } {μ : } (hm : m m0) :
theorem MeasureTheory.norm_condexpL2_le {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [] [] [] {m : } {m0 : } {μ : } (hm : m m0) (f : { x // x }) :
↑() f f
theorem MeasureTheory.snorm_condexpL2_le {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [] [] [] {m : } {m0 : } {μ : } (hm : m m0) (f : { x // x }) :
MeasureTheory.snorm (↑(↑() f)) 2 μ MeasureTheory.snorm (f) 2 μ
theorem MeasureTheory.norm_condexpL2_coe_le {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [] [] [] {m : } {m0 : } {μ : } (hm : m m0) (f : { x // x }) :
↑(↑() f) f
theorem MeasureTheory.inner_condexpL2_left_eq_right {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [] [] [] {m : } {m0 : } {μ : } (hm : m m0) {f : { x // x }} {g : { x // x }} :
inner (↑(↑() f)) g = inner f ↑(↑() g)
theorem MeasureTheory.condexpL2_indicator_of_measurable {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [] [] [] {m : } {m0 : } {μ : } {s : Set α} (hm : m m0) (hs : ) (hμs : μ s ) (c : E) :
↑(↑() (MeasureTheory.indicatorConstLp 2 (hm s hs) hμs c)) = MeasureTheory.indicatorConstLp 2 (hm s hs) hμs c
theorem MeasureTheory.inner_condexpL2_eq_inner_fun {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [] [] [] {m : } {m0 : } {μ : } (hm : m m0) (f : { x // x }) (g : { x // x }) (hg : ) :
inner (↑(↑() f)) g = inner f g
theorem MeasureTheory.integral_condexpL2_eq_of_fin_meas_real {α : Type u_1} {𝕜 : Type u_7} [] {m : } {m0 : } {μ : } {s : Set α} {hm : m m0} (f : { x // x }) (hs : ) (hμs : μ s ) :
∫ (x : α) in s, ↑(↑() f) xμ = ∫ (x : α) in s, f xμ
theorem MeasureTheory.lintegral_nnnorm_condexpL2_le {α : Type u_1} {m : } {m0 : } {μ : } {s : Set α} {hm : m m0} (hs : ) (hμs : μ s ) (f : { x // }) :
∫⁻ (x : α) in s, ↑(↑() f) x‖₊μ ∫⁻ (x : α) in s, f x‖₊μ
theorem MeasureTheory.condexpL2_ae_eq_zero_of_ae_eq_zero {α : Type u_1} {m : } {m0 : } {μ : } {s : Set α} {hm : m m0} (hs : ) (hμs : μ s ) {f : { x // }} (hf : ) :
↑(↑() f) =ᶠ[] 0
theorem MeasureTheory.lintegral_nnnorm_condexpL2_indicator_le_real {α : Type u_1} {m : } {m0 : } {μ : } {s : Set α} {t : Set α} {hm : m m0} (hs : ) (hμs : μ s ) (ht : ) (hμt : μ t ) :
∫⁻ (a : α) in t, ↑(↑() ()) a‖₊μ μ (s t)
theorem MeasureTheory.condexpL2_const_inner {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [] [] [] {m : } {m0 : } {μ : } (hm : m m0) (f : { x // x }) (c : E) :
↑(↑() (MeasureTheory.Memℒp.toLp (fun a => inner c (f a)) (_ : MeasureTheory.Memℒp (fun a => inner c (f a)) 2))) =ᶠ[] fun a => inner c (↑(↑() f) a)

condexpL2 commutes with taking inner products with constants. See the lemma condexpL2_comp_continuousLinearMap for a more general result about commuting with continuous linear maps.

theorem MeasureTheory.integral_condexpL2_eq {α : Type u_1} {E' : Type u_3} {𝕜 : Type u_7} [] [] [] [] [] {m : } {m0 : } {μ : } {s : Set α} (hm : m m0) (f : { x // x }) (hs : ) (hμs : μ s ) :
∫ (x : α) in s, ↑(↑() f) xμ = ∫ (x : α) in s, f xμ

condexpL2 verifies the equality of integrals defining the conditional expectation.

theorem MeasureTheory.condexpL2_comp_continuousLinearMap {α : Type u_1} {E' : Type u_3} (𝕜 : Type u_7) [] [] [] [] [] {m : } {m0 : } {μ : } {E'' : Type u_8} (𝕜' : Type u_9) [IsROrC 𝕜'] [] [InnerProductSpace 𝕜' E''] [] [NormedSpace E''] (hm : m m0) (T : E' →L[] E'') (f : { x // x }) :
↑(↑(MeasureTheory.condexpL2 E'' 𝕜' hm) ()) =ᶠ[] ↑(ContinuousLinearMap.compLp T ↑(↑() f))
theorem MeasureTheory.condexpL2_indicator_ae_eq_smul {α : Type u_1} {E' : Type u_3} (𝕜 : Type u_7) [] [] [] [] [] {m : } {m0 : } {μ : } {s : Set α} (hm : m m0) (hs : ) (hμs : μ s ) (x : E') :
↑(↑() ()) =ᶠ[] fun a => ↑(↑() ()) a x
theorem MeasureTheory.condexpL2_indicator_eq_toSpanSingleton_comp {α : Type u_1} {E' : Type u_3} (𝕜 : Type u_7) [] [] [] [] [] {m : } {m0 : } {μ : } {s : Set α} (hm : m m0) (hs : ) (hμs : μ s ) (x : E') :
↑(↑() ()) = ContinuousLinearMap.compLp () ↑(↑() ())
theorem MeasureTheory.set_lintegral_nnnorm_condexpL2_indicator_le {α : Type u_1} {E' : Type u_3} {𝕜 : Type u_7} [] [] [] [] [] {m : } {m0 : } {μ : } {s : Set α} (hm : m m0) (hs : ) (hμs : μ s ) (x : E') {t : Set α} (ht : ) (hμt : μ t ) :
∫⁻ (a : α) in t, ↑(↑() ()) a‖₊μ μ (s t) * x‖₊
theorem MeasureTheory.lintegral_nnnorm_condexpL2_indicator_le {α : Type u_1} {E' : Type u_3} {𝕜 : Type u_7} [] [] [] [] [] {m : } {m0 : } {μ : } {s : Set α} (hm : m m0) (hs : ) (hμs : μ s ) (x : E') :
∫⁻ (a : α), ↑(↑() ()) a‖₊μ μ s * x‖₊
theorem MeasureTheory.integrable_condexpL2_indicator {α : Type u_1} {E' : Type u_3} {𝕜 : Type u_7} [] [] [] [] [] {m : } {m0 : } {μ : } {s : Set α} (hm : m m0) (hs : ) (hμs : μ s ) (x : E') :
MeasureTheory.Integrable ↑(↑() ())

If the measure μ.trim hm is sigma-finite, then the conditional expectation of a measurable set with finite measure is integrable.

noncomputable def MeasureTheory.condexpIndSMul {α : Type u_1} {G : Type u_5} {m : } {m0 : } {μ : } {s : Set α} [] (hm : m m0) (hs : ) (hμs : μ s ) (x : G) :
{ x // x }

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

Instances For
theorem MeasureTheory.aeStronglyMeasurable'_condexpIndSMul {α : Type u_1} {G : Type u_5} {m : } {m0 : } {μ : } {s : Set α} [] (hm : m m0) (hs : ) (hμs : μ s ) (x : G) :
theorem MeasureTheory.condexpIndSMul_add {α : Type u_1} {G : Type u_5} {m : } {m0 : } {μ : } {s : Set α} [] {hm : m m0} (hs : ) (hμs : μ s ) (x : G) (y : G) :
theorem MeasureTheory.condexpIndSMul_smul {α : Type u_1} {G : Type u_5} {m : } {m0 : } {μ : } {s : Set α} [] {hm : m m0} (hs : ) (hμs : μ s ) (c : ) (x : G) :
theorem MeasureTheory.condexpIndSMul_smul' {α : Type u_1} {F : Type u_4} {𝕜 : Type u_7} [] [] {m : } {m0 : } {μ : } {s : Set α} {hm : m m0} [] [] (hs : ) (hμs : μ s ) (c : 𝕜) (x : F) :
theorem MeasureTheory.condexpIndSMul_ae_eq_smul {α : Type u_1} {G : Type u_5} {m : } {m0 : } {μ : } {s : Set α} [] (hm : m m0) (hs : ) (hμs : μ s ) (x : G) :
↑(MeasureTheory.condexpIndSMul hm hs hμs x) =ᶠ[] fun a => ↑(↑() ()) a x
theorem MeasureTheory.set_lintegral_nnnorm_condexpIndSMul_le {α : Type u_1} {G : Type u_5} {m : } {m0 : } {μ : } {s : Set α} [] (hm : m m0) (hs : ) (hμs : μ s ) (x : G) {t : Set α} (ht : ) (hμt : μ t ) :
∫⁻ (a : α) in t, ↑(MeasureTheory.condexpIndSMul hm hs hμs x) a‖₊μ μ (s t) * x‖₊
theorem MeasureTheory.lintegral_nnnorm_condexpIndSMul_le {α : Type u_1} {G : Type u_5} {m : } {m0 : } {μ : } {s : Set α} [] (hm : m m0) (hs : ) (hμs : μ s ) (x : G) :
∫⁻ (a : α), ↑(MeasureTheory.condexpIndSMul hm hs hμs x) a‖₊μ μ s * x‖₊
theorem MeasureTheory.integrable_condexpIndSMul {α : Type u_1} {G : Type u_5} {m : } {m0 : } {μ : } {s : Set α} [] (hm : m m0) (hs : ) (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 MeasureTheory.condexpIndSMul_empty {α : Type u_1} {G : Type u_5} {m : } {m0 : } {μ : } [] {hm : m m0} {x : G} :
MeasureTheory.condexpIndSMul hm (_ : ) (_ : μ ) x = 0
theorem MeasureTheory.set_integral_condexpL2_indicator {α : Type u_1} {m : } {m0 : } {μ : } {s : Set α} {t : Set α} {hm : m m0} (hs : ) (ht : ) (hμs : μ s ) (hμt : μ t ) :
∫ (x : α) in s, ↑(↑() ()) xμ = ENNReal.toReal (μ (t s))
theorem MeasureTheory.set_integral_condexpIndSMul {α : Type u_1} {G' : Type u_6} [] [] [] {m : } {m0 : } {μ : } {s : Set α} {t : Set α} {hm : m m0} (hs : ) (ht : ) (hμs : μ s ) (hμt : μ t ) (x : G') :
∫ (a : α) in s, ↑(MeasureTheory.condexpIndSMul hm ht hμt x) aμ = ENNReal.toReal (μ (t s)) x
theorem MeasureTheory.condexpL2_indicator_nonneg {α : Type u_1} {m : } {m0 : } {μ : } {s : Set α} (hm : m m0) (hs : ) (hμs : μ s ) :
0 ≤ᶠ[] ↑(↑() ())
theorem MeasureTheory.condexpIndSMul_nonneg {α : Type u_1} {m : } {m0 : } {μ : } {s : Set α} {hm : m m0} {E : Type u_10} [] [] (hs : ) (hμs : μ s ) (x : E) (hx : 0 x) :
0 ≤ᶠ[] ↑(MeasureTheory.condexpIndSMul hm hs hμs x)