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 inequalityVar[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.
@[simp]
theorem
probability_theory.variance_zero
{Ω : Type u_1}
{m : measurable_space Ω}
(μ : measure_theory.measure Ω) :
probability_theory.variance 0 μ = 0
theorem
probability_theory.variance_nonneg
{Ω : Type u_1}
{m : measurable_space Ω}
(f : Ω → ℝ)
(μ : measure_theory.measure Ω) :
0 ≤ probability_theory.variance f μ
theorem
probability_theory.variance_mul
{Ω : Type u_1}
{m : measurable_space Ω}
(c : ℝ)
(f : Ω → ℝ)
(μ : measure_theory.measure Ω) :
probability_theory.variance (λ (ω : Ω), c * f ω) μ = c ^ 2 * probability_theory.variance f μ
theorem
probability_theory.variance_smul
{Ω : Type u_1}
{m : measurable_space Ω}
(c : ℝ)
(f : Ω → ℝ)
(μ : measure_theory.measure Ω) :
probability_theory.variance (c • f) μ = c ^ 2 * probability_theory.variance f μ
theorem
probability_theory.variance_smul'
{A : Type u_1}
[comm_semiring A]
[algebra A ℝ]
{Ω : Type u_2}
{m : measurable_space Ω}
(c : A)
(f : Ω → ℝ)
(μ : measure_theory.measure Ω) :
probability_theory.variance (c • f) μ = c ^ 2 • probability_theory.variance f μ
theorem
probability_theory.variance_def'
{Ω : Type u_1}
[measure_theory.measure_space Ω]
[measure_theory.is_probability_measure measure_theory.measure_space.volume]
{X : Ω → ℝ}
(hX : measure_theory.mem_ℒp X 2 measure_theory.measure_space.volume) :
probability_theory.variance X measure_theory.measure_space.volume = (∫ (a : Ω), (X ^ 2) a) - (∫ (a : Ω), X a) ^ 2
theorem
probability_theory.variance_le_expectation_sq
{Ω : Type u_1}
[measure_theory.measure_space Ω]
[measure_theory.is_probability_measure measure_theory.measure_space.volume]
{X : Ω → ℝ} :
probability_theory.variance X measure_theory.measure_space.volume ≤ ∫ (a : Ω), (X ^ 2) a
theorem
probability_theory.meas_ge_le_variance_div_sq
{Ω : Type u_1}
[measure_theory.measure_space Ω]
[measure_theory.is_probability_measure measure_theory.measure_space.volume]
{X : Ω → ℝ}
(hX : measure_theory.mem_ℒp X 2 measure_theory.measure_space.volume)
{c : ℝ}
(hc : 0 < c) :
⇑measure_theory.measure_space.volume {ω : Ω | c ≤ |X ω - ∫ (a : Ω), X a|} ≤ ennreal.of_real (probability_theory.variance X measure_theory.measure_space.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
probability_theory.indep_fun.variance_add
{Ω : Type u_1}
[measure_theory.measure_space Ω]
[measure_theory.is_probability_measure measure_theory.measure_space.volume]
{X Y : Ω → ℝ}
(hX : measure_theory.mem_ℒp X 2 measure_theory.measure_space.volume)
(hY : measure_theory.mem_ℒp Y 2 measure_theory.measure_space.volume)
(h : probability_theory.indep_fun X Y measure_theory.measure_space.volume) :
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}
[measure_theory.measure_space Ω]
[measure_theory.is_probability_measure measure_theory.measure_space.volume]
{ι : Type u_2}
{X : ι → Ω → ℝ}
{s : finset ι}
(hs : ∀ (i : ι), i ∈ s → measure_theory.mem_ℒp (X i) 2 measure_theory.measure_space.volume)
(h : ↑s.pairwise (λ (i j : ι), probability_theory.indep_fun (X i) (X j) measure_theory.measure_space.volume)) :
probability_theory.variance (s.sum (λ (i : ι), X i)) measure_theory.measure_space.volume = s.sum (λ (i : ι), probability_theory.variance (X i) measure_theory.measure_space.volume)
The variance of a finite sum of pairwise independent random variables is the sum of the variances.