Conditional variance

This file defines the variance of a real-valued random variable conditional to a sigma-algebra.

TODO

Define the Lebesgue conditional variance. See GibbsMeasure for a definition of the Lebesgue conditional expectation).

noncomputable def ProbabilityTheory.condVar {Ω : Type u_1} {m₀ : MeasurableSpace Ω} (m : MeasurableSpace Ω) (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω) : Ω → ℝ

Conditional variance of a real-valued random variable. It is defined as 0 if any one of the following conditions is true:

• m is not a sub-σ-algebra of m₀,
• μ is not σ-finite with respect to m,
• X - μ[X | m] is not square-integrable.

Equations

• ProbabilityTheory.condVar m X μ = MeasureTheory.condExp m μ ((X - MeasureTheory.condExp m μ X) ^ 2)

def ProbabilityTheory.«termVar[_;_|_]» : Lean.ParserDescr

Conditional variance of a real-valued random variable. It is defined as 0 if any one of the following conditions is true:

• m is not a sub-σ-algebra of m₀,
• μ is not σ-finite with respect to m,
• X - μ[X | m] is not square-integrable.

Equations

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

def ProbabilityTheory.«termVar[_|_]» : Lean.ParserDescr

Conditional variance of a real-valued random variable. It is defined as 0 if any one of the following conditions is true:

• m is not a sub-σ-algebra of m₀,
• volume is not σ-finite with respect to m,
• X - 𝔼[X | m] is not square-integrable.

Equations

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

theorem ProbabilityTheory.condVar_of_not_le {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (hm : ¬m ≤ m₀) : condVar m X μ = 0

theorem ProbabilityTheory.condVar_of_not_sigmaFinite {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {hm : m ≤ m₀} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (hμm : ¬MeasureTheory.SigmaFinite (μ.trim hm)) : condVar m X μ = 0

theorem ProbabilityTheory.condVar_of_sigmaFinite {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {hm : m ≤ m₀} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.SigmaFinite (μ.trim hm)] : condVar m X μ = if MeasureTheory.Integrable (fun (ω : Ω) => (X ω - MeasureTheory.condExp m μ X ω) ^ 2) μ then if MeasureTheory.StronglyMeasurable fun (ω : Ω) => (X ω - MeasureTheory.condExp m μ X ω) ^ 2 then fun (ω : Ω) => (X ω - MeasureTheory.condExp m μ X ω) ^ 2 else MeasureTheory.AEStronglyMeasurable.mk ↑↑(MeasureTheory.condExpL1 hm μ fun (ω : Ω) => (X ω - MeasureTheory.condExp m μ X ω) ^ 2) ⋯ else 0

theorem ProbabilityTheory.condVar_of_stronglyMeasurable {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {hm : m ≤ m₀} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.SigmaFinite (μ.trim hm)] (hX : MeasureTheory.StronglyMeasurable X) (hXint : MeasureTheory.Integrable ((X - MeasureTheory.condExp m μ X) ^ 2) μ) : condVar m X μ = fun (ω : Ω) => (X ω - MeasureTheory.condExp m μ X ω) ^ 2

theorem ProbabilityTheory.condVar_of_not_integrable {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (hXint : ¬MeasureTheory.Integrable (fun (ω : Ω) => (X ω - MeasureTheory.condExp m μ X ω) ^ 2) μ) : condVar m X μ = 0

@[simp]

theorem ProbabilityTheory.condVar_zero {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} : condVar m 0 μ = 0

@[simp]

theorem ProbabilityTheory.condVar_const {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (hm : m ≤ m₀) (c : ℝ) : condVar m (fun (x : Ω) => c) μ = 0

theorem ProbabilityTheory.stronglyMeasurable_condVar {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} : MeasureTheory.StronglyMeasurable (condVar m X μ)

theorem ProbabilityTheory.condVar_congr_ae {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (h : X =ᵐ[μ] Y) : condVar m X μ =ᵐ[μ] condVar m Y μ

theorem ProbabilityTheory.condVar_of_aestronglyMeasurable {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {hm : m ≤ m₀} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [hμm : MeasureTheory.SigmaFinite (μ.trim hm)] (hX : MeasureTheory.AEStronglyMeasurable X μ) (hXint : MeasureTheory.Integrable ((X - MeasureTheory.condExp m μ X) ^ 2) μ) : condVar m X μ =ᵐ[μ] (X - MeasureTheory.condExp m μ X) ^ 2

theorem ProbabilityTheory.integrable_condVar {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} : MeasureTheory.Integrable (condVar m X μ) μ

theorem ProbabilityTheory.setIntegral_condVar {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {hm : m ≤ m₀} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {s : Set Ω} [MeasureTheory.SigmaFinite (μ.trim hm)] (hX : MeasureTheory.Integrable ((X - MeasureTheory.condExp m μ X) ^ 2) μ) (hs : MeasurableSet s) : ∫ (ω : Ω) in s, condVar m X μ ω ∂μ = ∫ (ω : Ω) in s, (X ω - MeasureTheory.condExp m μ X ω) ^ 2 ∂μ

The integral of the conditional variance Var[X | m] over an m-measurable set is equal to the integral of (X - μ[X | m]) ^ 2 on that set.

theorem ProbabilityTheory.condVar_ae_eq_condExp_sq_sub_sq_condExp {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (hm : m ≤ m₀) [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.Memℒp X 2 μ) : condVar m X μ =ᵐ[μ] MeasureTheory.condExp m μ (X ^ 2) - MeasureTheory.condExp m μ X ^ 2

theorem ProbabilityTheory.condVar_ae_le_condExp_sq {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (hm : m ≤ m₀) [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.Memℒp X 2 μ) : condVar m X μ ≤ᵐ[μ] MeasureTheory.condExp m μ (X ^ 2)

theorem ProbabilityTheory.integral_condVar_add_variance_condExp {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (hm : m ≤ m₀) [MeasureTheory.IsProbabilityMeasure μ] (hX : MeasureTheory.Memℒp X 2 μ) : ∫ (x : Ω), condVar m X μ x ∂μ + variance (MeasureTheory.condExp m μ X) μ = variance X μ

Law of total variance

theorem ProbabilityTheory.condVar_bot' {Ω : Type u_1} {m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NeZero μ] (X : Ω → ℝ) : condVar ⊥ X μ = fun (x : Ω) => ⨍ (ω : Ω), (X ω - ⨍ (ω' : Ω), X ω' ∂μ) ^ 2 ∂μ

theorem ProbabilityTheory.condVar_bot_ae_eq {Ω : Type u_1} {m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (X : Ω → ℝ) : condVar ⊥ X μ =ᵐ[μ] fun (x : Ω) => ⨍ (ω : Ω), (X ω - ⨍ (ω' : Ω), X ω' ∂μ) ^ 2 ∂μ

theorem ProbabilityTheory.condVar_bot {Ω : Type u_1} {m₀ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (hX : AEMeasurable X μ) : condVar ⊥ X μ = fun (_ω : Ω) => variance X μ

theorem ProbabilityTheory.condVar_smul {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (c : ℝ) (X : Ω → ℝ) : condVar m (c • X) μ =ᵐ[μ] c ^ 2 • condVar m X μ

@[simp]

theorem ProbabilityTheory.condVar_neg {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (X : Ω → ℝ) : condVar m (-X) μ =ᵐ[μ] condVar m X μ