Documentation

Mathlib.Probability.CondVar

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

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.

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.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.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_le_condExp_sq {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {X : Ω} {μ : MeasureTheory.Measure Ω} (hm : m m₀) [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.Memℒp 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 μ