Conditional expectation in L2

This file contains one step of the construction of the conditional expectation, which is completed in Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean. 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 𝕜 : RCLike:

• 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) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0) : ↥(Lp E 2 μ) →L[𝕜] ↥(lpMeas E 𝕜 m 2 μ)

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

Equations

• MeasureTheory.condExpL2 E 𝕜 hm = (MeasureTheory.lpMeas E 𝕜 m 2 μ).orthogonalProjectionOnto

theorem MeasureTheory.aestronglyMeasurable_condExpL2 {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0) (f : ↥(Lp E 2 μ)) : AEStronglyMeasurable (↑↑↑((condExpL2 E 𝕜 hm) f)) μ

theorem MeasureTheory.integrableOn_condExpL2_of_measure_ne_top {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (hm : m ≤ m0) (hμs : μ s ≠ ⊤) (f : ↥(Lp E 2 μ)) : IntegrableOn (↑↑↑((condExpL2 E 𝕜 hm) f)) s μ

theorem MeasureTheory.integrable_condExpL2_of_isFiniteMeasure {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0) [IsFiniteMeasure μ] {f : ↥(Lp E 2 μ)} : Integrable (↑↑↑((condExpL2 E 𝕜 hm) f)) μ

theorem MeasureTheory.norm_condExpL2_le_one {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0) : ‖condExpL2 E 𝕜 hm‖ ≤ 1

theorem MeasureTheory.norm_condExpL2_le {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0) (f : ↥(Lp E 2 μ)) : ‖(condExpL2 E 𝕜 hm) f‖ ≤ ‖f‖

theorem MeasureTheory.eLpNorm_condExpL2_le {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0) (f : ↥(Lp E 2 μ)) : eLpNorm (↑↑↑((condExpL2 E 𝕜 hm) f)) 2 μ ≤ eLpNorm (↑↑f) 2 μ

theorem MeasureTheory.norm_condExpL2_coe_le {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0) (f : ↥(Lp E 2 μ)) : ‖↑((condExpL2 E 𝕜 hm) f)‖ ≤ ‖f‖

theorem MeasureTheory.inner_condExpL2_left_eq_right {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0) {f g : ↥(Lp E 2 μ)} : inner 𝕜 (↑((condExpL2 E 𝕜 hm) f)) g = inner 𝕜 f ↑((condExpL2 E 𝕜 hm) g)

theorem MeasureTheory.condExpL2_indicator_of_measurable {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (c : E) : ↑((condExpL2 E 𝕜 hm) (indicatorConstLp 2 ⋯ hμs c)) = indicatorConstLp 2 ⋯ hμs c

theorem MeasureTheory.inner_condExpL2_eq_inner_fun {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0) (f g : ↥(Lp E 2 μ)) (hg : AEStronglyMeasurable (↑↑g) μ) : inner 𝕜 (↑((condExpL2 E 𝕜 hm) f)) g = inner 𝕜 f g

theorem MeasureTheory.integral_condExpL2_eq_of_fin_meas_real {α : Type u_1} {𝕜 : Type u_7} [RCLike 𝕜] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} {hm : m ≤ m0} (f : ↥(Lp 𝕜 2 μ)) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) : ∫ (x : α) in s, ↑↑↑((condExpL2 𝕜 𝕜 hm) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ

theorem MeasureTheory.lintegral_nnnorm_condExpL2_le {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} {hm : m ≤ m0} (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (f : ↥(Lp ℝ 2 μ)) : ∫⁻ (x : α) in s, ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊ ∂μ ≤ ∫⁻ (x : α) in s, ↑‖↑↑f x‖₊ ∂μ

theorem MeasureTheory.condExpL2_ae_eq_zero_of_ae_eq_zero {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} {hm : m ≤ m0} (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) {f : ↥(Lp ℝ 2 μ)} (hf : ↑↑f =ᵐ[μ.restrict s] 0) : ↑↑↑((condExpL2 ℝ ℝ hm) f) =ᵐ[μ.restrict s] 0

theorem MeasureTheory.lintegral_nnnorm_condExpL2_indicator_le_real {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {s t : Set α} {hm : m ≤ m0} (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (ht : MeasurableSet t) (hμt : μ t ≠ ⊤) : ∫⁻ (a : α) in t, ↑‖↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a‖₊ ∂μ ≤ μ (s ∩ t)

theorem MeasureTheory.condExpL2_const_inner {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0) (f : ↥(Lp E 2 μ)) (c : E) : ↑↑↑((condExpL2 𝕜 𝕜 hm) (MemLp.toLp (fun (a : α) => inner 𝕜 c (↑↑f a)) ⋯)) =ᵐ[μ] fun (a : α) => inner 𝕜 c (↑↑↑((condExpL2 E 𝕜 hm) 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} [RCLike 𝕜] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E'] [NormedSpace ℝ E'] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (hm : m ≤ m0) (f : ↥(Lp E' 2 μ)) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) : ∫ (x : α) in s, ↑↑↑((condExpL2 E' 𝕜 hm) 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) [RCLike 𝕜] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E'] [NormedSpace ℝ E'] {m m0 : MeasurableSpace α} {μ : Measure α} {E'' : Type u_8} (𝕜' : Type u_9) [RCLike 𝕜'] [NormedAddCommGroup E''] [InnerProductSpace 𝕜' E''] [CompleteSpace E''] [NormedSpace ℝ E''] (hm : m ≤ m0) (T : E' →L[ℝ] E'') (f : ↥(Lp E' 2 μ)) : ↑↑↑((condExpL2 E'' 𝕜' hm) (T.compLp f)) =ᵐ[μ] ↑↑(T.compLp ↑((condExpL2 E' 𝕜 hm) f))

theorem MeasureTheory.condExpL2_indicator_ae_eq_smul {α : Type u_1} {E' : Type u_3} (𝕜 : Type u_7) [RCLike 𝕜] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E'] [NormedSpace ℝ E'] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : E') : ↑↑↑((condExpL2 E' 𝕜 hm) (indicatorConstLp 2 hs hμs x)) =ᵐ[μ] fun (a : α) => ↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a • x

theorem MeasureTheory.condExpL2_indicator_eq_toSpanSingleton_comp {α : Type u_1} {E' : Type u_3} (𝕜 : Type u_7) [RCLike 𝕜] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E'] [NormedSpace ℝ E'] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : E') : ↑((condExpL2 E' 𝕜 hm) (indicatorConstLp 2 hs hμs x)) = (ContinuousLinearMap.toSpanSingleton ℝ x).compLp ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))

theorem MeasureTheory.setLIntegral_nnnorm_condExpL2_indicator_le {α : Type u_1} {E' : Type u_3} {𝕜 : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E'] [NormedSpace ℝ E'] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : E') {t : Set α} (ht : MeasurableSet t) (hμt : μ t ≠ ⊤) : ∫⁻ (a : α) in t, ↑‖↑↑↑((condExpL2 E' 𝕜 hm) (indicatorConstLp 2 hs hμs x)) a‖₊ ∂μ ≤ μ (s ∩ t) * ↑‖x‖₊

theorem MeasureTheory.lintegral_nnnorm_condExpL2_indicator_le {α : Type u_1} {E' : Type u_3} {𝕜 : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E'] [NormedSpace ℝ E'] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : E') [SigmaFinite (μ.trim hm)] : ∫⁻ (a : α), ↑‖↑↑↑((condExpL2 E' 𝕜 hm) (indicatorConstLp 2 hs hμs x)) a‖₊ ∂μ ≤ μ s * ↑‖x‖₊

theorem MeasureTheory.integrable_condExpL2_indicator {α : Type u_1} {E' : Type u_3} {𝕜 : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E'] [NormedSpace ℝ E'] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (hm : m ≤ m0) [SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : E') : Integrable (↑↑↑((condExpL2 E' 𝕜 hm) (indicatorConstLp 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 MeasureTheory.condExpIndSMul {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [NormedSpace ℝ G] (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : G) : ↥(Lp G 2 μ)

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.

theorem MeasureTheory.aestronglyMeasurable_condExpIndSMul {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [NormedSpace ℝ G] (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : G) : AEStronglyMeasurable (↑↑(condExpIndSMul hm hs hμs x)) μ

theorem MeasureTheory.condExpIndSMul_add {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [NormedSpace ℝ G] {hm : m ≤ m0} (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x y : G) : condExpIndSMul hm hs hμs (x + y) = condExpIndSMul hm hs hμs x + condExpIndSMul hm hs hμs y

theorem MeasureTheory.condExpIndSMul_smul {α : Type u_1} {F : Type u_4} {𝕜 : Type u_7} [RCLike 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} {hm : m ≤ m0} [NormedSpace ℝ F] [SMulCommClass ℝ 𝕜 F] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (c : 𝕜) (x : F) : condExpIndSMul hm hs hμs (c • x) = c • condExpIndSMul hm hs hμs x

theorem MeasureTheory.condExpIndSMul_ae_eq_smul {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [NormedSpace ℝ G] (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : G) : ↑↑(condExpIndSMul hm hs hμs x) =ᵐ[μ] fun (a : α) => ↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a • x

theorem MeasureTheory.setLIntegral_nnnorm_condExpIndSMul_le {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [NormedSpace ℝ G] (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : G) {t : Set α} (ht : MeasurableSet t) (hμt : μ t ≠ ⊤) : ∫⁻ (a : α) in t, ↑‖↑↑(condExpIndSMul hm hs hμs x) a‖₊ ∂μ ≤ μ (s ∩ t) * ↑‖x‖₊

theorem MeasureTheory.lintegral_nnnorm_condExpIndSMul_le {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [NormedSpace ℝ G] (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : G) [SigmaFinite (μ.trim hm)] : ∫⁻ (a : α), ↑‖↑↑(condExpIndSMul hm hs hμs x) a‖₊ ∂μ ≤ μ s * ↑‖x‖₊

theorem MeasureTheory.integrable_condExpIndSMul {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [NormedSpace ℝ G] (hm : m ≤ m0) [SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : G) : Integrable (↑↑(condExpIndSMul 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 MeasureTheory.condExpIndSMul_empty {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : Measure α} [NormedSpace ℝ G] {hm : m ≤ m0} {x : G} : condExpIndSMul hm ⋯ ⋯ x = 0

theorem MeasureTheory.setIntegral_condExpL2_indicator {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {s t : Set α} {hm : m ≤ m0} (hs : MeasurableSet s) (ht : MeasurableSet t) (hμs : μ s ≠ ⊤) (hμt : μ t ≠ ⊤) : ∫ (x : α) in s, ↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 ht hμt 1)) x ∂μ = μ.real (t ∩ s)

theorem MeasureTheory.setIntegral_condExpIndSMul {α : Type u_1} {G' : Type u_6} [NormedAddCommGroup G'] [NormedSpace ℝ G'] [CompleteSpace G'] {m m0 : MeasurableSpace α} {μ : Measure α} {s t : Set α} {hm : m ≤ m0} (hs : MeasurableSet s) (ht : MeasurableSet t) (hμs : μ s ≠ ⊤) (hμt : μ t ≠ ⊤) (x : G') : ∫ (a : α) in s, ↑↑(condExpIndSMul hm ht hμt x) a ∂μ = μ.real (t ∩ s) • x

theorem MeasureTheory.condExpL2_indicator_nonneg {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) [SigmaFinite (μ.trim hm)] : 0 ≤ᵐ[μ] ↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))

theorem MeasureTheory.condExpIndSMul_nonneg {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} {hm : m ≤ m0} {E : Type u_10} [NormedAddCommGroup E] [PartialOrder E] [NormedSpace ℝ E] [IsOrderedModule ℝ E] [SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : E) (hx : 0 ≤ x) : 0 ≤ᵐ[μ] ↑↑(condExpIndSMul hm hs hμs x)