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.

source

def ProbabilityTheory.evariance {Ω : Type u_1} {mΩ : 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 ∂μ

Instances For

source

def ProbabilityTheory.variance {Ω : Type u_1} {mΩ : 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

Instances For

source

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.

Instances For

source

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.

Instances For

source

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.

Instances For

source

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.

Instances For

source

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

evariance X μ = evariance Y μ

source

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

variance X μ = variance Y μ

source

theorem ProbabilityTheory.evariance_lt_top {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.MemLp X 2 μ) :

evariance X μ < ⊤

source

theorem ProbabilityTheory.evariance_ne_top {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.MemLp X 2 μ) :

evariance X μ ≠ ⊤

source

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

evariance X μ = ⊤

source

theorem ProbabilityTheory.evariance_lt_top_iff_memLp {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.AEStronglyMeasurable X μ) :

evariance X μ < ⊤ ↔ MeasureTheory.MemLp X 2 μ

source

@[deprecated ProbabilityTheory.evariance_lt_top_iff_memLp (since := "2025-02-21")]

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.MemLp X 2 μ

Alias of ProbabilityTheory.evariance_lt_top_iff_memLp.

source

theorem ProbabilityTheory.evariance_eq_top_iff {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.AEStronglyMeasurable X μ) :

evariance X μ = ⊤ ↔ ¬MeasureTheory.MemLp X 2 μ

source

theorem ProbabilityTheory.variance_of_not_memLp {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.AEStronglyMeasurable X μ) (hX_not : ¬MeasureTheory.MemLp X 2 μ) :

variance X μ = 0

source

theorem ProbabilityTheory.ofReal_variance {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.MemLp X 2 μ) :

ENNReal.ofReal (variance X μ) = evariance X μ

source

theorem MeasureTheory.MemLp.evariance_lt_top {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : Measure Ω} [IsFiniteMeasure μ] (hX : MemLp X 2 μ) :

ProbabilityTheory.evariance X μ < ⊤

Alias of ProbabilityTheory.evariance_lt_top.

source

theorem MeasureTheory.MemLp.evariance_ne_top {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : Measure Ω} [IsFiniteMeasure μ] (hX : MemLp X 2 μ) :

ProbabilityTheory.evariance X μ ≠ ⊤

Alias of ProbabilityTheory.evariance_ne_top.

source

theorem MeasureTheory.MemLp.ofReal_variance_eq {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : Measure Ω} [IsFiniteMeasure μ] (hX : MemLp X 2 μ) :

ENNReal.ofReal (ProbabilityTheory.variance X μ) = ProbabilityTheory.evariance X μ

Alias of ProbabilityTheory.ofReal_variance.

source

@[deprecated ProbabilityTheory.evariance_lt_top (since := "2025-02-21")]

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

ProbabilityTheory.evariance X μ < ⊤

Alias of ProbabilityTheory.evariance_lt_top.

source

@[deprecated ProbabilityTheory.evariance_ne_top (since := "2025-02-21")]

theorem MeasureTheory.Memℒp.evariance_ne_top {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : Measure Ω} [IsFiniteMeasure μ] (hX : MemLp X 2 μ) :

ProbabilityTheory.evariance X μ ≠ ⊤

Alias of ProbabilityTheory.evariance_ne_top.

source

@[deprecated ProbabilityTheory.ofReal_variance (since := "2025-02-21")]

theorem MeasureTheory.Memℒp.ofReal_variance_eq {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : Measure Ω} [IsFiniteMeasure μ] (hX : MemLp X 2 μ) :

ENNReal.ofReal (ProbabilityTheory.variance X μ) = ProbabilityTheory.evariance X μ

Alias of ProbabilityTheory.ofReal_variance.

source

theorem ProbabilityTheory.evariance_eq_lintegral_ofReal {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω) :

evariance X μ = ∫⁻ (ω : Ω), ENNReal.ofReal ((X ω - ∫ (x : Ω), X x ∂μ) ^ 2) ∂μ

source

theorem ProbabilityTheory.variance_eq_integral {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (hX : AEMeasurable X μ) :

variance X μ = ∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ) ^ 2 ∂μ

source

theorem ProbabilityTheory.variance_of_integral_eq_zero {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (hX : AEMeasurable X μ) (hXint : ∫ (x : Ω), X x ∂μ = 0) :

variance X μ = ∫ (ω : Ω), X ω ^ 2 ∂μ

source

@[simp]

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

evariance 0 μ = 0

source

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 ∂μ

source

theorem ProbabilityTheory.evariance_mul {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (c : ℝ) (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω) :

evariance (fun (ω : Ω) => c * X ω) μ = ENNReal.ofReal (c ^ 2) * evariance X μ

source

@[simp]

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

variance 0 μ = 0

source

theorem ProbabilityTheory.covariance_self {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hX : AEMeasurable X μ) :

covariance X X μ = variance X μ

source

@[deprecated ProbabilityTheory.covariance_self (since := "2025-06-25")]

theorem ProbabilityTheory.covariance_same {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hX : AEMeasurable X μ) :

covariance X X μ = variance X μ

Alias of ProbabilityTheory.covariance_self.

source

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

0 ≤ variance X μ

source

theorem ProbabilityTheory.variance_mul {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (c : ℝ) (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω) :

variance (fun (ω : Ω) => c * X ω) μ = c ^ 2 * variance X μ

source

theorem ProbabilityTheory.variance_smul {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (c : ℝ) (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω) :

variance (c • X) μ = c ^ 2 * variance X μ

source

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 μ

source

theorem ProbabilityTheory.variance_eq_sub {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} (hX : MeasureTheory.MemLp X 2 μ) :

variance X μ = ∫ (x : Ω), (X ^ 2) x ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2

source

@[deprecated ProbabilityTheory.variance_eq_sub (since := "2025-08-07")]

theorem ProbabilityTheory.variance_def' {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} (hX : MeasureTheory.MemLp X 2 μ) :

variance X μ = ∫ (x : Ω), (X ^ 2) x ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2

Alias of ProbabilityTheory.variance_eq_sub.

source

theorem ProbabilityTheory.variance_add_const {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (hX : MeasureTheory.AEStronglyMeasurable X μ) (c : ℝ) :

variance (fun (ω : Ω) => X ω + c) μ = variance X μ

source

theorem ProbabilityTheory.variance_const_add {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (hX : MeasureTheory.AEStronglyMeasurable X μ) (c : ℝ) :

variance (fun (ω : Ω) => c + X ω) μ = variance X μ

source

theorem ProbabilityTheory.variance_fun_neg {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} :

variance (fun (ω : Ω) => -X ω) μ = variance X μ

source

theorem ProbabilityTheory.variance_neg {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} :

variance (-X) μ = variance X μ

source

theorem ProbabilityTheory.variance_sub_const {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (hX : MeasureTheory.AEStronglyMeasurable X μ) (c : ℝ) :

variance (fun (ω : Ω) => X ω - c) μ = variance X μ

source

theorem ProbabilityTheory.variance_const_sub {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (hX : MeasureTheory.AEStronglyMeasurable X μ) (c : ℝ) :

variance (fun (ω : Ω) => c - X ω) μ = variance X μ

source

theorem ProbabilityTheory.variance_add {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.MemLp X 2 μ) (hY : MeasureTheory.MemLp Y 2 μ) :

variance (X + Y) μ = variance X μ + 2 * covariance X Y μ + variance Y μ

source

theorem ProbabilityTheory.variance_fun_add {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.MemLp X 2 μ) (hY : MeasureTheory.MemLp Y 2 μ) :

variance (fun (ω : Ω) => X ω + Y ω) μ = variance X μ + 2 * covariance X Y μ + variance Y μ

source

theorem ProbabilityTheory.variance_sub {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.MemLp X 2 μ) (hY : MeasureTheory.MemLp Y 2 μ) :

variance (X - Y) μ = variance X μ - 2 * covariance X Y μ + variance Y μ

source

theorem ProbabilityTheory.variance_fun_sub {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.MemLp X 2 μ) (hY : MeasureTheory.MemLp Y 2 μ) :

variance (fun (ω : Ω) => X ω - Y ω) μ = variance X μ - 2 * covariance X Y μ + variance Y μ

source

theorem ProbabilityTheory.variance_sum' {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {s : Finset ι} {X : ι → Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ] (hX : ∀ i ∈ s, MeasureTheory.MemLp (X i) 2 μ) :

variance (∑ i ∈ s, X i) μ = ∑ i ∈ s, ∑ j ∈ s, covariance (X i) (X j) μ

source

theorem ProbabilityTheory.variance_sum {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ] [Fintype ι] (hX : ∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ) :

variance (∑ i : ι, X i) μ = ∑ i : ι, ∑ j : ι, covariance (X i) (X j) μ

source

theorem ProbabilityTheory.variance_fun_sum' {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {s : Finset ι} {X : ι → Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ] (hX : ∀ i ∈ s, MeasureTheory.MemLp (X i) 2 μ) :

variance (fun (ω : Ω) => ∑ i ∈ s, X i ω) μ = ∑ i ∈ s, ∑ j ∈ s, covariance (X i) (X j) μ

source

theorem ProbabilityTheory.variance_fun_sum {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ] [Fintype ι] (hX : ∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ) :

variance (fun (ω : Ω) => ∑ i : ι, X i ω) μ = ∑ i : ι, ∑ j : ι, covariance (X i) (X j) μ

source

@[simp]

theorem ProbabilityTheory.variance_dirac {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} [MeasurableSingletonClass Ω] (x : Ω) :

variance X (MeasureTheory.Measure.dirac x) = 0

source

theorem ProbabilityTheory.variance_map {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {Ω' : Type u_3} {mΩ' : MeasurableSpace Ω'} {μ : MeasureTheory.Measure Ω'} {Y : Ω' → Ω} (hX : AEMeasurable X (MeasureTheory.Measure.map Y μ)) (hY : AEMeasurable Y μ) :

variance X (MeasureTheory.Measure.map Y μ) = variance (X ∘ Y) μ

source

theorem MeasureTheory.MeasurePreserving.variance_fun_comp {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} {Ω' : Type u_3} {mΩ' : MeasurableSpace Ω'} {ν : Measure Ω'} {X : Ω → Ω'} (hX : MeasurePreserving X μ ν) {f : Ω' → ℝ} (hf : AEMeasurable f ν) :

ProbabilityTheory.variance (fun (ω : Ω) => f (X ω)) μ = ProbabilityTheory.variance f ν

source

theorem ProbabilityTheory.variance_map_equiv {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {Ω' : Type u_3} {mΩ' : MeasurableSpace Ω'} {μ : MeasureTheory.Measure Ω'} (X : Ω → ℝ) (Y : Ω' ≃ᵐ Ω) :

variance X (MeasureTheory.Measure.map (⇑Y) μ) = variance (X ∘ ⇑Y) μ

source

theorem ProbabilityTheory.variance_id_map {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hX : AEMeasurable X μ) :

variance id (MeasureTheory.Measure.map X μ) = variance X μ

source

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 ∂μ

source

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)

source

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.

source

theorem ProbabilityTheory.meas_ge_le_variance_div_sq {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} (hX : MeasureTheory.MemLp 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.

source

theorem ProbabilityTheory.IndepFun.variance_add {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X Y : Ω → ℝ} (hX : MeasureTheory.MemLp X 2 μ) (hY : MeasureTheory.MemLp 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.

source

theorem ProbabilityTheory.IndepFun.variance_fun_add {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X Y : Ω → ℝ} (hX : MeasureTheory.MemLp X 2 μ) (hY : MeasureTheory.MemLp Y 2 μ) (h : IndepFun X Y μ) :

variance (fun (ω : Ω) => X ω + Y ω) μ = variance X μ + variance Y μ

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

source

theorem ProbabilityTheory.IndepFun.variance_sum {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_3} {X : ι → Ω → ℝ} {s : Finset ι} (hs : ∀ i ∈ s, MeasureTheory.MemLp (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.

source

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).

source

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 variances

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

source

theorem ProbabilityTheory.variance_add_prod {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {Ω' : Type u_3} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] {X : Ω → ℝ} {Y : Ω' → ℝ} (hfμ : MeasureTheory.MemLp X 2 μ) (hgν : MeasureTheory.MemLp Y 2 ν) :

variance (fun (p : Ω × Ω') => X p.1 + Y p.2) (μ.prod ν) = variance X μ + variance Y ν

source

theorem ProbabilityTheory.variance_dual_prod' {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] {mE : MeasurableSpace E} [NormedAddCommGroup F] [NormedSpace ℝ F] {mF : MeasurableSpace F} {μ : MeasureTheory.Measure E} [MeasureTheory.IsProbabilityMeasure μ] {ν : MeasureTheory.Measure F} [MeasureTheory.IsProbabilityMeasure ν] {L : StrongDual ℝ (E × F)} (hLμ : MeasureTheory.MemLp (⇑(ContinuousLinearMap.comp L (ContinuousLinearMap.inl ℝ E F))) 2 μ) (hLν : MeasureTheory.MemLp (⇑(ContinuousLinearMap.comp L (ContinuousLinearMap.inr ℝ E F))) 2 ν) :

variance (⇑L) (μ.prod ν) = variance (⇑(ContinuousLinearMap.comp L (ContinuousLinearMap.inl ℝ E F))) μ + variance (⇑(ContinuousLinearMap.comp L (ContinuousLinearMap.inr ℝ E F))) ν

source

theorem ProbabilityTheory.variance_dual_prod {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] {mE : MeasurableSpace E} [NormedAddCommGroup F] [NormedSpace ℝ F] {mF : MeasurableSpace F} {μ : MeasureTheory.Measure E} [MeasureTheory.IsProbabilityMeasure μ] {ν : MeasureTheory.Measure F} [MeasureTheory.IsProbabilityMeasure ν] {L : StrongDual ℝ (E × F)} (hLμ : MeasureTheory.MemLp id 2 μ) (hLν : MeasureTheory.MemLp id 2 ν) :

variance (⇑L) (μ.prod ν) = variance (⇑(ContinuousLinearMap.comp L (ContinuousLinearMap.inl ℝ E F))) μ + variance (⇑(ContinuousLinearMap.comp L (ContinuousLinearMap.inr ℝ E F))) ν

Documentation

Mathlib.Probability.Moments.Variance

Variance of random variables #

Main definitions #

Main results #