# 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
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
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))) ν