theorem condVar_eq_condExp_sq_sub_sq_condExp' {Ω : Type u_1} {m m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hm : m ≤ m₀) [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.MemLp X 2 μ) : ProbabilityTheory.condVar m X μ =ᵐ[μ] μ[X ^ 2 | m] - μ[X | m] ^ 2

Alternative formula for conditional variance.

For an L² random variable X, the conditional variance equals Var(X | m) = E[X² | m] − (E[X | m])² almost everywhere. This is the conditional analogue of the identity Var(X) = E[X²] − (EX)².

theorem martingale_condVar_identity {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {𝓕 : MeasureTheory.Filtration ℕ m0} {X : ℕ → Ω → ℝ} (hmart : MeasureTheory.Martingale X 𝓕 μ) (hL2 : ∀ (n : ℕ), MeasureTheory.MemLp (X n) 2 μ) {m n : ℕ} (hmn : m ≤ n) : μ[fun (ω : Ω) => (X n ω - X m ω) ^ 2 | ↑𝓕 m] =ᵐ[μ] fun (ω : Ω) => μ[fun (ω' : Ω) => X n ω' ^ 2 | ↑𝓕 m] ω - X m ω ^ 2

Conditional variance theorem for martingales (Lecture 28).

If Xₙ is a square-integrable martingale with respect to the filtration 𝓕, then for m ≤ n, E[(Xₙ − Xₘ)² | 𝓕ₘ] = E[Xₙ² | 𝓕ₘ] − Xₘ² almost surely.

This expresses the conditional variance of the increment Xₙ − Xₘ in terms of the conditional second moment of Xₙ.