# mathlibdocumentation

probability.variance

# Variance of random variables #

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

We prove the basic properties of the variance:

• variance_le_expectation_sq: the inequality Var[X] ≤ 𝔼[X^2].
• meas_ge_le_variance_div_sq: Chebyshev's inequality, i.e., ℙ {ω | c ≤ |X ω - 𝔼[X]|} ≤ ennreal.of_real (Var[X] / c ^ 2).
• indep_fun.variance_add: the variance of the sum of two independent random variables is the sum of the variances.
• indep_fun.variance_sum: the variance of a finite sum of pairwise independent random variables is the sum of the variances.
noncomputable def probability_theory.variance {Ω : Type u_1} {m : measurable_space Ω} (f : Ω → ) (μ : measure_theory.measure Ω) :

The variance of a random variable is 𝔼[X^2] - 𝔼[X]^2 or, equivalently, 𝔼[(X - 𝔼[X])^2]. We use the latter as the definition, to ensure better behavior even in garbage situations.

Equations
@[simp]
theorem probability_theory.variance_zero {Ω : Type u_1} {m : measurable_space Ω} (μ : measure_theory.measure Ω) :
theorem probability_theory.variance_nonneg {Ω : Type u_1} {m : measurable_space Ω} (f : Ω → ) (μ : measure_theory.measure Ω) :
theorem probability_theory.variance_mul {Ω : Type u_1} {m : measurable_space Ω} (c : ) (f : Ω → ) (μ : measure_theory.measure Ω) :
probability_theory.variance (λ (ω : Ω), c * f ω) μ = c ^ 2 *
theorem probability_theory.variance_smul {Ω : Type u_1} {m : measurable_space Ω} (c : ) (f : Ω → ) (μ : measure_theory.measure Ω) :
μ = c ^ 2 *
theorem probability_theory.variance_smul' {A : Type u_1} [ ] {Ω : Type u_2} {m : measurable_space Ω} (c : A) (f : Ω → ) (μ : measure_theory.measure Ω) :
μ = c ^ 2
theorem probability_theory.variance_def' {Ω : Type u_1} {X : Ω → }  :
= (∫ (a : Ω), (X ^ 2) a) - (∫ (a : Ω), X a) ^ 2
theorem probability_theory.variance_le_expectation_sq {Ω : Type u_1} {X : Ω → } :
∫ (a : Ω), (X ^ 2) a
theorem probability_theory.meas_ge_le_variance_div_sq {Ω : Type u_1} {X : Ω → } {c : } (hc : 0 < c) :
measure_theory.measure_space.volume {ω : Ω | c |X ω - ∫ (a : Ω), X a|}

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

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

theorem probability_theory.indep_fun.variance_sum {Ω : Type u_1} {ι : Type u_2} {X : ι → Ω → } {s : finset ι} (hs : ∀ (i : ι), ) (h : s.pairwise (λ (i j : ι), ) :

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