# 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.
def ProbabilityTheory.evariance {Ω : Type u_1} :
{x : } → (Ω)

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

Equations
• = ∫⁻ (ω : Ω), X ω - ∫ (x : Ω), X xμ‖₊ ^ 2μ
Instances For
def ProbabilityTheory.variance {Ω : Type u_1} :
{x : } → (Ω)

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

Equations
• = .toReal
Instances For
theorem MeasureTheory.Memℒp.evariance_lt_top {Ω : Type u_1} {m : } {X : Ω} {μ : } (hX : ) :
theorem ProbabilityTheory.evariance_eq_top {Ω : Type u_1} {m : } {X : Ω} {μ : } (hXm : ) (hX : ¬) :
theorem ProbabilityTheory.evariance_lt_top_iff_memℒp {Ω : Type u_1} {m : } {X : Ω} {μ : } (hX : ) :
theorem MeasureTheory.Memℒp.ofReal_variance_eq {Ω : Type u_1} {m : } {X : Ω} {μ : } (hX : ) :
theorem ProbabilityTheory.evariance_eq_lintegral_ofReal {Ω : Type u_1} {m : } (X : Ω) (μ : ) :
= ∫⁻ (ω : Ω), ENNReal.ofReal ((X ω - ∫ (x : Ω), X xμ) ^ 2)μ
theorem MeasureTheory.Memℒp.variance_eq_of_integral_eq_zero {Ω : Type u_1} {m : } {X : Ω} {μ : } (hX : ) (hXint : ∫ (x : Ω), X xμ = 0) :
= ∫ (x : Ω), (X ^ 2) xμ
theorem MeasureTheory.Memℒp.variance_eq {Ω : Type u_1} {m : } {X : Ω} {μ : } (hX : ) :
= ∫ (x : Ω), ((X - fun (x : Ω) => ∫ (x : Ω), X xμ) ^ 2) xμ
@[simp]
theorem ProbabilityTheory.evariance_zero {Ω : Type u_1} {m : } {μ : } :
theorem ProbabilityTheory.evariance_eq_zero_iff {Ω : Type u_1} {m : } {X : Ω} {μ : } (hX : ) :
X =ᵐ[μ] fun (x : Ω) => ∫ (x : Ω), X xμ
theorem ProbabilityTheory.evariance_mul {Ω : Type u_1} {m : } (c : ) (X : Ω) (μ : ) :
ProbabilityTheory.evariance (fun (ω : Ω) => c * X ω) μ = ENNReal.ofReal (c ^ 2) *
Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem ProbabilityTheory.variance_zero {Ω : Type u_1} {m : } (μ : ) :
theorem ProbabilityTheory.variance_nonneg {Ω : Type u_1} {m : } (X : Ω) (μ : ) :
theorem ProbabilityTheory.variance_mul {Ω : Type u_1} {m : } (c : ) (X : Ω) (μ : ) :
ProbabilityTheory.variance (fun (ω : Ω) => c * X ω) μ = c ^ 2 *
theorem ProbabilityTheory.variance_smul {Ω : Type u_1} {m : } (c : ) (X : Ω) (μ : ) :
theorem ProbabilityTheory.variance_smul' {Ω : Type u_1} {m : } {A : Type u_2} [] [] (c : A) (X : Ω) (μ : ) :
Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem ProbabilityTheory.variance_def' {Ω : Type u_1} [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {X : Ω} (hX : MeasureTheory.Memℒp X 2 MeasureTheory.volume) :
ProbabilityTheory.variance X MeasureTheory.volume = (∫ (a : Ω), (X ^ 2) a) - (∫ (a : Ω), X a) ^ 2
theorem ProbabilityTheory.variance_le_expectation_sq {Ω : Type u_1} [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {X : Ω} (hm : MeasureTheory.AEStronglyMeasurable X MeasureTheory.volume) :
ProbabilityTheory.variance X MeasureTheory.volume ∫ (a : Ω), (X ^ 2) a
theorem ProbabilityTheory.evariance_def' {Ω : Type u_1} [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {X : Ω} (hX : MeasureTheory.AEStronglyMeasurable X MeasureTheory.volume) :
ProbabilityTheory.evariance X MeasureTheory.volume = (∫⁻ (ω : Ω), (X ω‖₊ ^ 2)) - ENNReal.ofReal ((∫ (a : Ω), X a) ^ 2)
theorem ProbabilityTheory.meas_ge_le_evariance_div_sq {Ω : Type u_1} {X : Ω} (hX : MeasureTheory.AEStronglyMeasurable X MeasureTheory.volume) {c : NNReal} (hc : c 0) :
MeasureTheory.volume {ω : Ω | c |X ω - ∫ (a : Ω), X a|} ProbabilityTheory.evariance X MeasureTheory.volume / c ^ 2

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

theorem ProbabilityTheory.meas_ge_le_variance_div_sq {Ω : Type u_1} [MeasureTheory.IsFiniteMeasure MeasureTheory.volume] {X : Ω} (hX : MeasureTheory.Memℒp X 2 MeasureTheory.volume) {c : } (hc : 0 < c) :
MeasureTheory.volume {ω : Ω | c |X ω - ∫ (a : Ω), X a|} ENNReal.ofReal (ProbabilityTheory.variance X MeasureTheory.volume / 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} [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {X : Ω} {Y : Ω} (hX : MeasureTheory.Memℒp X 2 MeasureTheory.volume) (hY : MeasureTheory.Memℒp Y 2 MeasureTheory.volume) (h : ProbabilityTheory.IndepFun X Y MeasureTheory.volume) :
ProbabilityTheory.variance (X + Y) MeasureTheory.volume = ProbabilityTheory.variance X MeasureTheory.volume + ProbabilityTheory.variance Y MeasureTheory.volume

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

theorem ProbabilityTheory.IndepFun.variance_sum {Ω : Type u_1} [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {ι : Type u_2} {X : ιΩ} {s : } (hs : is, MeasureTheory.Memℒp (X i) 2 MeasureTheory.volume) (h : (s).Pairwise fun (i j : ι) => ProbabilityTheory.IndepFun (X i) (X j) MeasureTheory.volume) :
ProbabilityTheory.variance (is, X i) MeasureTheory.volume = is, ProbabilityTheory.variance (X i) MeasureTheory.volume

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