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.

@[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

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

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.condLExp_lt_top {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} {P : Measure Ω} {f : Ω → ENNReal} (hf : ∫⁻ (x : Ω), f x ∂P ≠ ⊤) : ∀ᵐ (x : Ω) ∂P, P⁻[f | mΩ] x < ⊤

theorem MeasureTheory.condLExp_ne_top {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} {P : Measure Ω} {f : Ω → ENNReal} (hf : ∫⁻ (x : Ω), f x ∂P ≠ ⊤) : ∀ᵐ (x : Ω) ∂P, P⁻[f | mΩ] x ≠ ⊤

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 =ᵐ[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 =ᵐ[P] P⁻[X | mΩ]

The conditional (Lebesgue) expectation P⁻[X|mΩ] is defined uniquely as an mΩ-measurable function up to P-ae equality by its (Lebesgue) integral over all mΩ-measurable sets.

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 =ᵐ[P] Y) : P⁻[X | mΩ] =ᵐ[P] P⁻[Y | mΩ]

@[simp]

theorem MeasureTheory.condLExp_zero {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} (P : Measure Ω) : P⁻[0 | mΩ] = 0

@[simp]

theorem MeasureTheory.condLExp_one {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} (hm : mΩ ≤ mΩ₀) (P : Measure Ω) [hσ : SigmaFinite (P.trim hm)] : P⁻[1 | mΩ] = 1

theorem MeasureTheory.condLExp_congr_ae_trim {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} (hm : mΩ ≤ mΩ₀) {P : Measure Ω} {X Y : Ω → ENNReal} (hXY : X =ᵐ[P] Y) : P⁻[X | mΩ] =ᵐ[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 | ⊥] =ᵐ[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 ≤ᵐ[P] Y) : P⁻[X | mΩ] ≤ᵐ[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Ω] ≤ᵐ[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Ω] =ᵐ[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Ω] =ᵐ[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Ω] =ᵐ[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Ω] ≤ᵐ[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Ω] =ᵐ[P] c • P⁻[X | mΩ]

theorem MeasureTheory.condLExp_tsum {Ω : Type u_1} {mΩ₀ : MeasurableSpace Ω} {P : Measure Ω} {ι : Type u_2} (mΩ : MeasurableSpace Ω) [Countable ι] {X : ι → Ω → ENNReal} (hX : ∀ (i : ι), AEMeasurable (X i) P) : P⁻[∑' (i : ι), X i | mΩ] =ᵐ[P] ∑' (i : ι), P⁻[X i | mΩ]

theorem MeasureTheory.condLExp_finsetSum {Ω : Type u_1} {mΩ₀ : MeasurableSpace Ω} {P : Measure Ω} {ι : Type u_2} (mΩ : MeasurableSpace Ω) (s : Finset ι) {X : ι → Ω → ENNReal} (hX : ∀ (i : ι), AEMeasurable (X i) P) : P⁻[∑ i ∈ s, X i | mΩ] =ᵐ[P] ∑ i ∈ s, P⁻[X i | mΩ]

@[deprecated MeasureTheory.condLExp_finsetSum (since := "2026-04-08")]

theorem MeasureTheory.condLExp_finset_sum {Ω : Type u_1} {mΩ₀ : MeasurableSpace Ω} {P : Measure Ω} {ι : Type u_2} (mΩ : MeasurableSpace Ω) (s : Finset ι) {X : ι → Ω → ENNReal} (hX : ∀ (i : ι), AEMeasurable (X i) P) : P⁻[∑ i ∈ s, X i | mΩ] =ᵐ[P] ∑ i ∈ s, P⁻[X i | mΩ]

Alias of MeasureTheory.condLExp_finsetSum.