Conditional Lebesgue expectation

We define the conditional expectation of a ℝ≥0∞-valued function using the Lebesgue integral. Given a measure P : Measure[mΩ₀] Ω and a sub-σ-algebra mΩ of mΩ₀ (meaning hm : mΩ ≤ mΩ₀) and a function X : Ω → ℝ≥0∞, if P.trim hm is σ-finite, then the conditional (Lebesgue) expectation P⁻[X|mΩ] of X is the mΩ-measurable function such that for all mΩ-measurable sets s, ∫⁻ ω in s, P⁻[X|mΩ] ω ∂P = ∫⁻ ω in s, X ω ∂P (see setLIntegral_condLExp). This is unique up to P-ae equality (see ae_eq_condLExp).

Main definitions

• condLExp : conditional (Lebesgue) expectation of X with respect to mΩ.
• setLIntegral_condLExp: For any mΩ-measurable set s, ∫⁻ ω in s, P⁻[X|mΩ] ω ∂P = ∫⁻ ω in s, X ω ∂P.
• ae_eq_condLExp : the conditional (Lebesgue) expectation is characterized by its (Lebesgue) integral on mΩ-measurable sets up to P-ae equality.

Notation

For a measure P : Measure[mΩ₀] Ω, and another mΩ : MeasurableSpace Ω, we define the notation

• P⁻[X|mΩ] = condLExp mΩ P X

Design decisions

P⁻[X|mΩ] is assigned the junk value 0 when either ¬ mΩ ≤ mΩ₀ (mΩ is not a sub-σ-algebra) or h : mΩ ≤ mΩ₀ but ¬ SigmaFinite (P.trim hm) (the latter always holds when P is a probability measure). When both these hold, in some sense the "user definition" of P⁻[X|mΩ] should be considered "the" measurable function which satisfies setLIntegral_condLExp (which is proven unique up to P-ae measurable equality in ae_eq_condLExp). The actual definition is just used to show existence. However for (potential) convenience the actual definition assigns P⁻[X|mΩ] := X in the case when X is mΩ-measurable (which can be invoked using condLExp_eq_self).

To do

• Prove the pullout property
• Prove a dominated convergence theorem.

theorem MeasureTheory.condLExp_def {Ω : Type u_2} {mΩ₀ : MeasurableSpace Ω} (mΩ : MeasurableSpace Ω) (P : Measure Ω) (X : Ω → ENNReal) : P⁻[X|mΩ] = if hm : mΩ ≤ mΩ₀ then if SigmaFinite (P.trim hm) then if Measurable X then X else ((P.withDensity X).trim hm).rnDeriv (P.trim hm) else 0 else 0

@[irreducible]

noncomputable def MeasureTheory.condLExp {Ω : Type u_2} {mΩ₀ : MeasurableSpace Ω} (mΩ : MeasurableSpace Ω) (P : Measure Ω) (X : Ω → ENNReal) : Ω → ENNReal

Conditional (Lebesgue) expectation of a function, with notation P⁻[X|mΩ].

It is defined as 0 if either ¬ mΩ ≤ mΩ₀ or hm : mΩ ≤ mΩ₀ but ¬ SigmaFinite (P.trim hm).

One should typically not use the definition directly.

Equations

• P⁻[X|mΩ] = if hm : mΩ ≤ mΩ₀ then if MeasureTheory.SigmaFinite (P.trim hm) then if Measurable X then X else ((P.withDensity X).trim hm).rnDeriv (P.trim hm) else 0 else 0

def MeasureTheory.«term__⁻[_|_]» : Lean.TrailingParserDescr

Conditional (Lebesgue) expectation of a function, with notation P⁻[X|mΩ].

It is defined as 0 if either ¬ mΩ ≤ mΩ₀ or hm : mΩ ≤ mΩ₀ but ¬ SigmaFinite (P.trim hm).

One should typically not use the definition directly.

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.condLExpUnexpander : Lean.PrettyPrinter.Unexpander

Unexpander for μ⁻[f|m] notation.

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.condLExp_of_not_le {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} {P : Measure Ω} {X : Ω → ENNReal} (hm_not : ¬mΩ ≤ mΩ₀) : P⁻[X|mΩ] = 0

theorem MeasureTheory.condLExp_of_not_sigmaFinite {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} {P : Measure Ω} {X : Ω → ENNReal} (hm : mΩ ≤ mΩ₀) (hμm_not : ¬SigmaFinite (P.trim hm)) : P⁻[X|mΩ] = 0

theorem MeasureTheory.condLExp_eq_self {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} {X : Ω → ENNReal} (hm : mΩ ≤ mΩ₀) (P : Measure Ω) [hσ : SigmaFinite (P.trim hm)] (hX : Measurable X) : P⁻[X|mΩ] = X

theorem MeasureTheory.condLExp_of_not_sub_sigma_measurable {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} (hm : mΩ ≤ mΩ₀) (P : Measure Ω) [hσ : SigmaFinite (P.trim hm)] {X : Ω → ENNReal} (hX : ¬Measurable X) : P⁻[X|mΩ] = ((P.withDensity X).trim hm).rnDeriv (P.trim hm)

theorem MeasureTheory.measurable_condLExp {Ω : Type u_1} {mΩ₀ : MeasurableSpace Ω} (mΩ : MeasurableSpace Ω) (P : Measure Ω) (X : Ω → ENNReal) : Measurable P⁻[X|mΩ]

theorem MeasureTheory.measurable_condLExp' {Ω : Type u_1} {mΩ₀ : MeasurableSpace Ω} (mΩ : MeasurableSpace Ω) (P : Measure Ω) (X : Ω → ENNReal) : Measurable P⁻[X|mΩ]

theorem MeasureTheory.setLIntegral_condLExp {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} (hm : mΩ ≤ mΩ₀) (P : Measure Ω) [hσ : SigmaFinite (P.trim hm)] (X : Ω → ENNReal) {s : Set Ω} (hs : MeasurableSet s) : ∫⁻ (ω : Ω) in s, P⁻[X|mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P

The (Lebesgue) integral of the conditional (Lebesgue) expectation P⁻[X|mΩ] over an mΩ-measurable set is equal to the integral of X on that set.

theorem MeasureTheory.setLIntegral_condLExp_trim {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} (hm : mΩ ≤ mΩ₀) (P : Measure Ω) [hσ : SigmaFinite (P.trim hm)] (X : Ω → ENNReal) {s : Set Ω} (hs : MeasurableSet s) : ∫⁻ (ω : Ω) in s, P⁻[X|mΩ] ω ∂P.trim hm = ∫⁻ (ω : Ω) in s, X ω ∂P

theorem MeasureTheory.lintegral_condLExp {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} (hm : mΩ ≤ mΩ₀) (P : Measure Ω) [hσ : SigmaFinite (P.trim hm)] (X : Ω → ENNReal) : ∫⁻ (ω : Ω), P⁻[X|mΩ] ω ∂P = ∫⁻ (ω : Ω), X ω ∂P

theorem MeasureTheory.ae_eq_condLExp₀ {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} {Y : Ω → ENNReal} (hm : mΩ ≤ mΩ₀) {P : Measure Ω} [hσ : SigmaFinite (P.trim hm)] (X : Ω → ENNReal) (hY : AEMeasurable Y (P.trim hm)) (hXY : ∀ (s : Set Ω), MeasurableSet s → ∫⁻ (ω : Ω) in s, Y ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P) : Y =ᶠ[ae P] P⁻[X|mΩ]

theorem MeasureTheory.ae_eq_condLExp {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} {Y : Ω → ENNReal} (hm : mΩ ≤ mΩ₀) (P : Measure Ω) [hσ : SigmaFinite (P.trim hm)] (X : Ω → ENNReal) (hY : Measurable Y) (hXY : ∀ (s : Set Ω), MeasurableSet s → ∫⁻ (ω : Ω) in s, Y ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P) : Y =ᶠ[ae P] P⁻[X|mΩ]

theorem MeasureTheory.condLExp_const {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} (hm : mΩ ≤ mΩ₀) (P : Measure Ω) [hσ : SigmaFinite (P.trim hm)] (c : ENNReal) : P⁻[fun (x : Ω) => c|mΩ] = fun (x : Ω) => c

theorem MeasureTheory.condLExp_congr_ae {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} {P : Measure Ω} {X Y : Ω → ENNReal} (hXY : X =ᶠ[ae P] Y) : P⁻[X|mΩ] =ᶠ[ae P] P⁻[Y|mΩ]

theorem MeasureTheory.condLExp_congr_ae_trim {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} (hm : mΩ ≤ mΩ₀) {P : Measure Ω} {X Y : Ω → ENNReal} (hXY : X =ᶠ[ae P] Y) : P⁻[X|mΩ] =ᶠ[ae (P.trim hm)] P⁻[Y|mΩ]

theorem MeasureTheory.condLExp_bot' {Ω : Type u_1} {mΩ₀ : MeasurableSpace Ω} (P : Measure Ω) [NeZero P] (X : Ω → ENNReal) : P⁻[X|⊥] = fun (x : Ω) => (P Set.univ)⁻¹ • ∫⁻ (ω : Ω), X ω ∂P

theorem MeasureTheory.condLExp_bot_ae_eq {Ω : Type u_1} {mΩ₀ : MeasurableSpace Ω} (P : Measure Ω) (X : Ω → ENNReal) : P⁻[X|⊥] =ᶠ[ae P] fun (x : Ω) => (P Set.univ)⁻¹ • ∫⁻ (ω : Ω), X ω ∂P

theorem MeasureTheory.condLExp_bot {Ω : Type u_1} {mΩ₀ : MeasurableSpace Ω} (P : Measure Ω) [IsProbabilityMeasure P] (X : Ω → ENNReal) : P⁻[X|⊥] = fun (x : Ω) => ∫⁻ (ω : Ω), X ω ∂P

theorem MeasureTheory.condLExp_mono {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} {P : Measure Ω} {X Y : Ω → ENNReal} (hXY : X ≤ᶠ[ae P] Y) : P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[Y|mΩ]

theorem MeasureTheory.condLExp_add_le {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} {P : Measure Ω} (X Y : Ω → ENNReal) : P⁻[X|mΩ] + P⁻[Y|mΩ] ≤ᶠ[ae P] P⁻[X + Y|mΩ]

theorem MeasureTheory.condLExp_add_left {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} {P : Measure Ω} {X : Ω → ENNReal} (Y : Ω → ENNReal) (hX : AEMeasurable X P) : P⁻[X + Y|mΩ] =ᶠ[ae P] P⁻[X|mΩ] + P⁻[Y|mΩ]

theorem MeasureTheory.condLExp_add_right {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} {P : Measure Ω} (X : Ω → ENNReal) {Y : Ω → ENNReal} (hY : AEMeasurable Y P) : P⁻[X + Y|mΩ] =ᶠ[ae P] P⁻[X|mΩ] + P⁻[Y|mΩ]

theorem MeasureTheory.condLExp_smul {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} {P : Measure Ω} (X : Ω → ENNReal) (hX : AEMeasurable X P) (c : ENNReal) : P⁻[c • X|mΩ] =ᶠ[ae P] c • P⁻[X|mΩ]

theorem MeasureTheory.condLExp_smul_le {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} {P : Measure Ω} (X : Ω → ENNReal) {c : ENNReal} : c • P⁻[X|mΩ] ≤ᶠ[ae P] P⁻[c • X|mΩ]

theorem MeasureTheory.condLExp_smul' {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} {P : Measure Ω} (X : Ω → ENNReal) {c : ENNReal} (hc : c ≠ ⊤) : P⁻[c • X|mΩ] =ᶠ[ae P] c • P⁻[X|mΩ]