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 function, as an element of . This is the orthogonal projection on the subspace of almost everywhere m-measurable functions.

Main definitions #

Implementation notes #

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

noncomputable def MeasureTheory.condexpL2 {α : Type u_1} (E : Type u_2) (𝕜 : Type u_7) [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m m0) :
(MeasureTheory.Lp E 2) →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} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m m0) (f : (MeasureTheory.Lp E 2)) :
    theorem MeasureTheory.integrableOn_condexpL2_of_measure_ne_top {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hm : m m0) (hμs : μ s ) (f : (MeasureTheory.Lp E 2)) :
    theorem MeasureTheory.norm_condexpL2_le_one {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m m0) :
    theorem MeasureTheory.norm_condexpL2_le {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m m0) (f : (MeasureTheory.Lp E 2)) :
    theorem MeasureTheory.snorm_condexpL2_le {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m m0) (f : (MeasureTheory.Lp E 2)) :
    MeasureTheory.snorm (((MeasureTheory.condexpL2 E 𝕜 hm) f)) 2 μ MeasureTheory.snorm (f) 2 μ
    theorem MeasureTheory.norm_condexpL2_coe_le {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m m0) (f : (MeasureTheory.Lp E 2)) :
    theorem MeasureTheory.inner_condexpL2_left_eq_right {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m m0) {f : (MeasureTheory.Lp E 2)} {g : (MeasureTheory.Lp E 2)} :
    ((MeasureTheory.condexpL2 E 𝕜 hm) f), g⟫_𝕜 = f, ((MeasureTheory.condexpL2 E 𝕜 hm) g)⟫_𝕜
    theorem MeasureTheory.condexpL2_indicator_of_measurable {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hm : m m0) (hs : MeasurableSet s) (hμs : μ s ) (c : E) :
    theorem MeasureTheory.inner_condexpL2_eq_inner_fun {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m m0) (f : (MeasureTheory.Lp E 2)) (g : (MeasureTheory.Lp E 2)) (hg : MeasureTheory.AEStronglyMeasurable' m (g) μ) :
    ((MeasureTheory.condexpL2 E 𝕜 hm) f), g⟫_𝕜 = f, g⟫_𝕜
    theorem MeasureTheory.integral_condexpL2_eq_of_fin_meas_real {α : Type u_1} {𝕜 : Type u_7} [IsROrC 𝕜] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {hm : m m0} (f : (MeasureTheory.Lp 𝕜 2)) (hs : MeasurableSet s) (hμs : μ s ) :
    ∫ (x : α) in s, ((MeasureTheory.condexpL2 𝕜 𝕜 hm) f) xμ = ∫ (x : α) in s, f xμ
    theorem MeasureTheory.lintegral_nnnorm_condexpL2_le {α : Type u_1} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {hm : m m0} (hs : MeasurableSet s) (hμs : μ s ) (f : (MeasureTheory.Lp 2)) :
    ∫⁻ (x : α) in s, ((MeasureTheory.condexpL2 hm) f) x‖₊μ ∫⁻ (x : α) in s, f x‖₊μ
    theorem MeasureTheory.lintegral_nnnorm_condexpL2_indicator_le_real {α : Type u_1} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} {hm : m m0} (hs : MeasurableSet s) (hμs : μ s ) (ht : MeasurableSet t) (hμt : μ t ) :
    ∫⁻ (a : α) in t, ((MeasureTheory.condexpL2 hm) (MeasureTheory.indicatorConstLp 2 hs hμs 1)) a‖₊μ μ (s t)
    theorem MeasureTheory.condexpL2_const_inner {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m m0) (f : (MeasureTheory.Lp E 2)) (c : E) :
    ((MeasureTheory.condexpL2 𝕜 𝕜 hm) (MeasureTheory.Memℒp.toLp (fun (a : α) => c, f a⟫_𝕜) (_ : MeasureTheory.Memℒp (fun (a : α) => c, f a⟫_𝕜) 2))) =ᶠ[MeasureTheory.Measure.ae μ] fun (a : α) => c, ((MeasureTheory.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} [IsROrC 𝕜] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E'] [NormedSpace E'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hm : m m0) (f : (MeasureTheory.Lp E' 2)) (hs : MeasurableSet s) (hμs : μ s ) :
    ∫ (x : α) in s, ((MeasureTheory.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) [IsROrC 𝕜] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E'] [NormedSpace E'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E'' : Type u_8} (𝕜' : Type u_9) [IsROrC 𝕜'] [NormedAddCommGroup E''] [InnerProductSpace 𝕜' E''] [CompleteSpace E''] [NormedSpace E''] (hm : m m0) (T : E' →L[] E'') (f : (MeasureTheory.Lp E' 2)) :
    theorem MeasureTheory.condexpL2_indicator_ae_eq_smul {α : Type u_1} {E' : Type u_3} (𝕜 : Type u_7) [IsROrC 𝕜] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E'] [NormedSpace E'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hm : m m0) (hs : MeasurableSet s) (hμs : μ s ) (x : E') :
    ((MeasureTheory.condexpL2 E' 𝕜 hm) (MeasureTheory.indicatorConstLp 2 hs hμs x)) =ᶠ[MeasureTheory.Measure.ae μ] fun (a : α) => ((MeasureTheory.condexpL2 hm) (MeasureTheory.indicatorConstLp 2 hs hμs 1)) a x
    theorem MeasureTheory.set_lintegral_nnnorm_condexpL2_indicator_le {α : Type u_1} {E' : Type u_3} {𝕜 : Type u_7} [IsROrC 𝕜] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E'] [NormedSpace E'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.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, ((MeasureTheory.condexpL2 E' 𝕜 hm) (MeasureTheory.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} [IsROrC 𝕜] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E'] [NormedSpace E'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hm : m m0) (hs : MeasurableSet s) (hμs : μ s ) (x : E') [MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)] :
    ∫⁻ (a : α), ((MeasureTheory.condexpL2 E' 𝕜 hm) (MeasureTheory.indicatorConstLp 2 hs hμs x)) a‖₊μ μ s * x‖₊
    theorem MeasureTheory.integrable_condexpL2_indicator {α : Type u_1} {E' : Type u_3} {𝕜 : Type u_7} [IsROrC 𝕜] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E'] [NormedSpace E'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hm : m m0) [MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)] (hs : MeasurableSet 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 MeasureTheory.condexpIndSMul {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NormedSpace G] (hm : m m0) (hs : MeasurableSet s) (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} [NormedAddCommGroup G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NormedSpace G] (hm : m m0) (hs : MeasurableSet s) (hμs : μ s ) (x : G) :
      theorem MeasureTheory.condexpIndSMul_add {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NormedSpace G] {hm : m m0} (hs : MeasurableSet s) (hμs : μ s ) (x : G) (y : G) :
      theorem MeasureTheory.condexpIndSMul_smul {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NormedSpace G] {hm : m m0} (hs : MeasurableSet s) (hμs : μ s ) (c : ) (x : G) :
      theorem MeasureTheory.condexpIndSMul_smul' {α : Type u_1} {F : Type u_4} {𝕜 : Type u_7} [IsROrC 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {hm : m m0} [NormedSpace F] [SMulCommClass 𝕜 F] (hs : MeasurableSet s) (hμs : μ s ) (c : 𝕜) (x : F) :
      theorem MeasureTheory.condexpIndSMul_ae_eq_smul {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NormedSpace G] (hm : m m0) (hs : MeasurableSet s) (hμs : μ s ) (x : G) :
      (MeasureTheory.condexpIndSMul hm hs hμs x) =ᶠ[MeasureTheory.Measure.ae μ] fun (a : α) => ((MeasureTheory.condexpL2 hm) (MeasureTheory.indicatorConstLp 2 hs hμs 1)) a x
      theorem MeasureTheory.set_lintegral_nnnorm_condexpIndSMul_le {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.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, (MeasureTheory.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 : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NormedSpace G] (hm : m m0) (hs : MeasurableSet s) (hμs : μ s ) (x : G) [MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)] :
      ∫⁻ (a : α), (MeasureTheory.condexpIndSMul hm hs hμs x) a‖₊μ μ s * x‖₊
      theorem MeasureTheory.integrable_condexpIndSMul {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NormedSpace G] (hm : m m0) [MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)] (hs : MeasurableSet 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 MeasureTheory.condexpIndSMul_empty {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedSpace G] {hm : m m0} {x : G} :
      theorem MeasureTheory.set_integral_condexpL2_indicator {α : Type u_1} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} {hm : m m0} (hs : MeasurableSet s) (ht : MeasurableSet t) (hμs : μ s ) (hμt : μ t ) :
      ∫ (x : α) in s, ((MeasureTheory.condexpL2 hm) (MeasureTheory.indicatorConstLp 2 ht hμt 1)) xμ = (μ (t s)).toReal
      theorem MeasureTheory.set_integral_condexpIndSMul {α : Type u_1} {G' : Type u_6} [NormedAddCommGroup G'] [NormedSpace G'] [CompleteSpace G'] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} {hm : m m0} (hs : MeasurableSet s) (ht : MeasurableSet t) (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.condexpIndSMul_nonneg {α : Type u_1} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {hm : m m0} {E : Type u_10} [NormedLatticeAddCommGroup E] [NormedSpace E] [OrderedSMul E] [MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)] (hs : MeasurableSet s) (hμs : μ s ) (x : E) (hx : 0 x) :