mathlib documentation

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:

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
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 Ω) :
theorem probability_theory.variance_smul {Ω : Type u_1} {m : measurable_space Ω} (c : ) (f : Ω → ) (μ : measure_theory.measure Ω) :
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 Ω) :

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 a finite sum of pairwise independent random variables is the sum of the variances.