Variance of random variables #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We define the variance of a real-valued random variable as Var[X] = 𝔼[(X - 𝔼[X])^2] (in the
probability_theory locale).
Main definitions #
probability_theory.evariance: the variance of a real-valued random variable as a extended non-negative real.probability_theory.variance: the variance of a real-valued random variable as a real number.
Main results #
probability_theory.variance_le_expectation_sq: the inequalityVar[X] ≤ 𝔼[X^2].probability_theory.meas_ge_le_variance_div_sq: Chebyshev's inequality, i.e.,ℙ {ω | c ≤ |X ω - 𝔼[X]|} ≤ ennreal.of_real (Var[X] / c ^ 2).probability_theory.meas_ge_le_evariance_div_sq: Chebyshev's inequality formulated withevariancewithout requiring the random variables to be L².probability_theory.indep_fun.variance_add: the variance of the sum of two independent random variables is the sum of the variances.probability_theory.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.evariance
{Ω : Type u_1}
{m : measurable_space Ω}
(X : Ω → ℝ)
(μ : measure_theory.measure Ω) :
The ℝ≥0∞-valued variance of a real-valued random variable defined as the Lebesgue integral of
(X - 𝔼[X])^2.
noncomputable
def
probability_theory.variance
{Ω : Type u_1}
{m : measurable_space Ω}
(X : Ω → ℝ)
(μ : measure_theory.measure Ω) :
The ℝ-valued variance of a real-valued random variable defined by applying ennreal.to_real
to evariance.
Equations
theorem
measure_theory.mem_ℒp.evariance_lt_top
{Ω : Type u_1}
{m : measurable_space Ω}
{X : Ω → ℝ}
{μ : measure_theory.measure Ω}
[measure_theory.is_finite_measure μ]
(hX : measure_theory.mem_ℒp X 2 μ) :
theorem
probability_theory.evariance_eq_top
{Ω : Type u_1}
{m : measurable_space Ω}
{X : Ω → ℝ}
{μ : measure_theory.measure Ω}
[measure_theory.is_finite_measure μ]
(hXm : measure_theory.ae_strongly_measurable X μ)
(hX : ¬measure_theory.mem_ℒp X 2 μ) :
theorem
probability_theory.evariance_lt_top_iff_mem_ℒp
{Ω : Type u_1}
{m : measurable_space Ω}
{X : Ω → ℝ}
{μ : measure_theory.measure Ω}
[measure_theory.is_finite_measure μ]
(hX : measure_theory.ae_strongly_measurable X μ) :
probability_theory.evariance X μ < ⊤ ↔ measure_theory.mem_ℒp X 2 μ
theorem
measure_theory.mem_ℒp.of_real_variance_eq
{Ω : Type u_1}
{m : measurable_space Ω}
{X : Ω → ℝ}
{μ : measure_theory.measure Ω}
[measure_theory.is_finite_measure μ]
(hX : measure_theory.mem_ℒp X 2 μ) :
theorem
probability_theory.evariance_eq_lintegral_of_real
{Ω : Type u_1}
{m : measurable_space Ω}
(X : Ω → ℝ)
(μ : measure_theory.measure Ω) :
theorem
measure_theory.mem_ℒp.variance_eq_of_integral_eq_zero
{Ω : Type u_1}
{m : measurable_space Ω}
{X : Ω → ℝ}
{μ : measure_theory.measure Ω}
(hX : measure_theory.mem_ℒp X 2 μ)
(hXint : ∫ (x : Ω), X x ∂μ = 0) :
theorem
measure_theory.mem_ℒp.variance_eq
{Ω : Type u_1}
{m : measurable_space Ω}
{X : Ω → ℝ}
{μ : measure_theory.measure Ω}
[measure_theory.is_finite_measure μ]
(hX : measure_theory.mem_ℒp X 2 μ) :
@[simp]
theorem
probability_theory.evariance_zero
{Ω : Type u_1}
{m : measurable_space Ω}
{μ : measure_theory.measure Ω} :
theorem
probability_theory.evariance_eq_zero_iff
{Ω : Type u_1}
{m : measurable_space Ω}
{X : Ω → ℝ}
{μ : measure_theory.measure Ω}
(hX : ae_measurable X μ) :
theorem
probability_theory.evariance_mul
{Ω : Type u_1}
{m : measurable_space Ω}
(c : ℝ)
(X : Ω → ℝ)
(μ : measure_theory.measure Ω) :
probability_theory.evariance (λ (ω : Ω), c * X ω) μ = ennreal.of_real (c ^ 2) * probability_theory.evariance X μ
@[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 Ω}
(X : Ω → ℝ)
(μ : measure_theory.measure Ω) :
0 ≤ probability_theory.variance X μ
theorem
probability_theory.variance_mul
{Ω : Type u_1}
{m : measurable_space Ω}
(c : ℝ)
(X : Ω → ℝ)
(μ : measure_theory.measure Ω) :
probability_theory.variance (λ (ω : Ω), c * X ω) μ = c ^ 2 * probability_theory.variance X μ
theorem
probability_theory.variance_smul
{Ω : Type u_1}
{m : measurable_space Ω}
(c : ℝ)
(X : Ω → ℝ)
(μ : measure_theory.measure Ω) :
probability_theory.variance (c • X) μ = c ^ 2 * probability_theory.variance X μ
theorem
probability_theory.variance_smul'
{Ω : Type u_1}
{m : measurable_space Ω}
{A : Type u_2}
[comm_semiring A]
[algebra A ℝ]
(c : A)
(X : Ω → ℝ)
(μ : measure_theory.measure Ω) :
probability_theory.variance (c • X) μ = c ^ 2 • probability_theory.variance X μ
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 : Ω → ℝ}
(hm : measure_theory.ae_strongly_measurable X measure_theory.measure_space.volume) :
probability_theory.variance X measure_theory.measure_space.volume ≤ ∫ (a : Ω), (X ^ 2) a
theorem
probability_theory.evariance_def'
{Ω : Type u_1}
[measure_theory.measure_space Ω]
[measure_theory.is_probability_measure measure_theory.measure_space.volume]
{X : Ω → ℝ}
(hX : measure_theory.ae_strongly_measurable X measure_theory.measure_space.volume) :
probability_theory.evariance X measure_theory.measure_space.volume = (∫⁻ (ω : Ω), ↑‖X ω‖₊ ^ 2) - ennreal.of_real ((∫ (a : Ω), X a) ^ 2)
theorem
probability_theory.meas_ge_le_evariance_div_sq
{Ω : Type u_1}
[measure_theory.measure_space Ω]
{X : Ω → ℝ}
(hX : measure_theory.ae_strongly_measurable X measure_theory.measure_space.volume)
{c : nnreal}
(hc : c ≠ 0) :
⇑measure_theory.measure_space.volume {ω : Ω | ↑c ≤ |X ω - ∫ (a : Ω), X a|} ≤ probability_theory.evariance X measure_theory.measure_space.volume / ↑c ^ 2
Chebyshev's inequality for ℝ≥0∞-valued variance.
theorem
probability_theory.meas_ge_le_variance_div_sq
{Ω : Type u_1}
[measure_theory.measure_space Ω]
[measure_theory.is_finite_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.