Variance of random variables

We define the variance of a real-valued random variable as Var[X] = 𝔼[(X - 𝔼[X])^2] (in the ProbabilityTheory locale).

Main definitions

• ProbabilityTheory.evariance: the variance of a real-valued random variable as an extended non-negative real.
• ProbabilityTheory.variance: the variance of a real-valued random variable as a real number.

Main results

• ProbabilityTheory.variance_le_expectation_sq: the inequality Var[X] ≤ 𝔼[X^2].
• ProbabilityTheory.meas_ge_le_variance_div_sq: Chebyshev's inequality, i.e., ℙ {ω | c ≤ |X ω - 𝔼[X]|} ≤ ENNReal.ofReal (Var[X] / c ^ 2).
• ProbabilityTheory.meas_ge_le_evariance_div_sq: Chebyshev's inequality formulated with evariance without requiring the random variables to be L².
• ProbabilityTheory.IndepFun.variance_add: the variance of the sum of two independent random variables is the sum of the variances.
• ProbabilityTheory.IndepFun.variance_sum: the variance of a finite sum of pairwise independent random variables is the sum of the variances.
• ProbabilityTheory.variance_le_sub_mul_sub: the variance of a random variable X satisfying a ≤ X ≤ b almost everywhere is at most (b - 𝔼 X) * (𝔼 X - a).
• ProbabilityTheory.variance_le_sq_of_bounded: the variance of a random variable X satisfying a ≤ X ≤ b almost everywhere is at most((b - a) / 2) ^ 2.

def ProbabilityTheory.evariance {Ω : Type u_1} {x✝ : MeasurableSpace Ω} (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω) : ENNReal

The ℝ≥0∞-valued variance of a real-valued random variable defined as the Lebesgue integral of (X - 𝔼[X])^2.

Equations

• ProbabilityTheory.evariance X μ = ∫⁻ (ω : Ω), ↑‖X ω - ∫ (x : Ω), X x ∂μ‖₊ ^ 2 ∂μ

def ProbabilityTheory.variance {Ω : Type u_1} {x✝ : MeasurableSpace Ω} (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω) : ℝ

The ℝ-valued variance of a real-valued random variable defined by applying ENNReal.toReal to evariance.

Equations

• ProbabilityTheory.variance X μ = (ProbabilityTheory.evariance X μ).toReal

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

The ℝ≥0∞-valued variance of the real-valued random variable X according to the measure μ.

This is defined as the Lebesgue integral of (X - 𝔼[X])^2.

Equations

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

def ProbabilityTheory.«termEVar[_]» : Lean.ParserDescr

The ℝ≥0∞-valued variance of the real-valued random variable X according to the volume measure.

This is defined as the Lebesgue integral of (X - 𝔼[X])^2.

Equations

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

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

The ℝ-valued variance of the real-valued random variable X according to the measure μ.

It is set to 0 if X has infinite variance.

Equations

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

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

The ℝ-valued variance of the real-valued random variable X according to the volume measure.

It is set to 0 if X has infinite variance.

Equations

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

theorem MeasureTheory.Memℒp.evariance_lt_top {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : Measure Ω} [IsFiniteMeasure μ] (hX : Memℒp X 2 μ) : ProbabilityTheory.evariance X μ < ⊤

theorem ProbabilityTheory.evariance_eq_top {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (hXm : MeasureTheory.AEStronglyMeasurable X μ) (hX : ¬MeasureTheory.Memℒp X 2 μ) : evariance X μ = ⊤

theorem ProbabilityTheory.evariance_lt_top_iff_memℒp {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.AEStronglyMeasurable X μ) : evariance X μ < ⊤ ↔ MeasureTheory.Memℒp X 2 μ

theorem MeasureTheory.Memℒp.ofReal_variance_eq {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : Measure Ω} [IsFiniteMeasure μ] (hX : Memℒp X 2 μ) : ENNReal.ofReal (ProbabilityTheory.variance X μ) = ProbabilityTheory.evariance X μ

theorem ProbabilityTheory.evariance_eq_lintegral_ofReal {Ω : Type u_1} {m : MeasurableSpace Ω} (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω) : evariance X μ = ∫⁻ (ω : Ω), ENNReal.ofReal ((X ω - ∫ (x : Ω), X x ∂μ) ^ 2) ∂μ

theorem MeasureTheory.Memℒp.variance_eq_of_integral_eq_zero {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : Measure Ω} (hX : Memℒp X 2 μ) (hXint : ∫ (x : Ω), X x ∂μ = 0) : ProbabilityTheory.variance X μ = ∫ (x : Ω), (X ^ 2) x ∂μ

theorem MeasureTheory.Memℒp.variance_eq {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : Measure Ω} [IsFiniteMeasure μ] (hX : Memℒp X 2 μ) : ProbabilityTheory.variance X μ = ∫ (x : Ω), ((X - fun (x : Ω) => ∫ (x : Ω), X x ∂μ) ^ 2) x ∂μ

@[simp]

theorem ProbabilityTheory.evariance_zero {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} : evariance 0 μ = 0

theorem ProbabilityTheory.evariance_eq_zero_iff {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (hX : AEMeasurable X μ) : evariance X μ = 0 ↔ X =ᵐ[μ] fun (x : Ω) => ∫ (x : Ω), X x ∂μ

theorem ProbabilityTheory.evariance_mul {Ω : Type u_1} {m : MeasurableSpace Ω} (c : ℝ) (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω) : evariance (fun (ω : Ω) => c * X ω) μ = ENNReal.ofReal (c ^ 2) * evariance X μ

@[simp]

theorem ProbabilityTheory.variance_zero {Ω : Type u_1} {m : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω) : variance 0 μ = 0

theorem ProbabilityTheory.variance_nonneg {Ω : Type u_1} {m : MeasurableSpace Ω} (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω) : 0 ≤ variance X μ

theorem ProbabilityTheory.variance_mul {Ω : Type u_1} {m : MeasurableSpace Ω} (c : ℝ) (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω) : variance (fun (ω : Ω) => c * X ω) μ = c ^ 2 * variance X μ

theorem ProbabilityTheory.variance_smul {Ω : Type u_1} {m : MeasurableSpace Ω} (c : ℝ) (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω) : variance (c • X) μ = c ^ 2 * variance X μ

theorem ProbabilityTheory.variance_smul' {Ω : Type u_1} {m : MeasurableSpace Ω} {A : Type u_2} [CommSemiring A] [Algebra A ℝ] (c : A) (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω) : variance (c • X) μ = c ^ 2 • variance X μ

theorem ProbabilityTheory.variance_def' {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} (hX : MeasureTheory.Memℒp X 2 μ) : variance X μ = ∫ (x : Ω), (X ^ 2) x ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2

theorem ProbabilityTheory.variance_le_expectation_sq {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} (hm : MeasureTheory.AEStronglyMeasurable X μ) : variance X μ ≤ ∫ (x : Ω), (X ^ 2) x ∂μ

theorem ProbabilityTheory.evariance_def' {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} (hX : MeasureTheory.AEStronglyMeasurable X μ) : evariance X μ = ∫⁻ (ω : Ω), ↑(‖X ω‖₊ ^ 2) ∂μ - ENNReal.ofReal ((∫ (x : Ω), X x ∂μ) ^ 2)

theorem ProbabilityTheory.meas_ge_le_evariance_div_sq {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hX : MeasureTheory.AEStronglyMeasurable X μ) {c : NNReal} (hc : c ≠ 0) : μ {ω : Ω | ↑c ≤ |X ω - ∫ (x : Ω), X x ∂μ|} ≤ evariance X μ / ↑c ^ 2

Chebyshev's inequality for ℝ≥0∞-valued variance.

theorem ProbabilityTheory.meas_ge_le_variance_div_sq {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} (hX : MeasureTheory.Memℒp X 2 μ) {c : ℝ} (hc : 0 < c) : μ {ω : Ω | c ≤ |X ω - ∫ (x : Ω), X x ∂μ|} ≤ ENNReal.ofReal (variance X μ / c ^ 2)

Chebyshev's inequality: one can control the deviation probability of a real random variable from its expectation in terms of the variance.

theorem ProbabilityTheory.IndepFun.variance_add {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X Y : Ω → ℝ} (hX : MeasureTheory.Memℒp X 2 μ) (hY : MeasureTheory.Memℒp Y 2 μ) (h : IndepFun X Y μ) : variance (X + Y) μ = variance X μ + variance Y μ

The variance of the sum of two independent random variables is the sum of the variances.

theorem ProbabilityTheory.IndepFun.variance_sum {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ι : Type u_2} {X : ι → Ω → ℝ} {s : Finset ι} (hs : ∀ i ∈ s, MeasureTheory.Memℒp (X i) 2 μ) (h : (↑s).Pairwise fun (i j : ι) => IndepFun (X i) (X j) μ) : variance (∑ i ∈ s, X i) μ = ∑ i ∈ s, variance (X i) μ

The variance of a finite sum of pairwise independent random variables is the sum of the variances.

theorem ProbabilityTheory.variance_le_sub_mul_sub {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {a b : ℝ} {X : Ω → ℝ} (h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b) (hX : AEMeasurable X μ) : variance X μ ≤ (b - ∫ (x : Ω), X x ∂μ) * (∫ (x : Ω), X x ∂μ - a)

The Bhatia-Davis inequality on variance

The variance of a random variable X satisfying a ≤ X ≤ b almost everywhere is at most (b - 𝔼 X) * (𝔼 X - a).

theorem ProbabilityTheory.variance_le_sq_of_bounded {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {a b : ℝ} {X : Ω → ℝ} (h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b) (hX : AEMeasurable X μ) : variance X μ ≤ ((b - a) / 2) ^ 2

Popoviciu's inequality on variance

The variance of a random variable X satisfying a ≤ X ≤ b almost everywhere is at most ((b - a) / 2) ^ 2.