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) :
() →L[𝕜] (MeasureTheory.lpMeas E 𝕜 m 2 μ)

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

Equations
Instances For
theorem MeasureTheory.aeStronglyMeasurable'_condexpL2 {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [] [] [] {m : } {m0 : } {μ : } (hm : m m0) (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 : ()) :
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 : ()} :
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 : ()) :
theorem MeasureTheory.snorm_condexpL2_le {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [] [] [] {m : } {m0 : } {μ : } (hm : m m0) (f : ()) :
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 : ()) :
(() 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 : ()} {g : ()} :
(() f), g⟫_𝕜 = 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 (_ : ) hμs c)) = MeasureTheory.indicatorConstLp 2 (_ : ) 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 : ()) (g : ()) (hg : ) :
(() f), g⟫_𝕜 = 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 : ()) (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 : α) 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 : ()} (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 : ()) (c : E) :
(() (MeasureTheory.Memℒp.toLp (fun (a : α) => c, f a⟫_𝕜) (_ : MeasureTheory.Memℒp (fun (a : α) => c, f a⟫_𝕜) 2))) =ᶠ[] fun (a : α) => 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 : ()) (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 : ()) :
((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') :
(() ()) =
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) :
()

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

Equations
• One or more equations did not get rendered due to their size.
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μ = (μ (t s)).toReal
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μ = (μ (t s)).toReal 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)