mathlib3documentation

probability.variance

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 inequality Var[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 with evariance without 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.

Equations
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 Ω} (hX : μ) :
theorem probability_theory.evariance_eq_top {Ω : Type u_1} {m : measurable_space Ω} {X : Ω } {μ : measure_theory.measure Ω} (hXm : μ) (hX : ¬) :
theorem measure_theory.mem_ℒp.of_real_variance_eq {Ω : Type u_1} {m : measurable_space Ω} {X : Ω } {μ : measure_theory.measure Ω} (hX : μ) :
theorem probability_theory.evariance_eq_lintegral_of_real {Ω : Type u_1} {m : measurable_space Ω} (X : Ω ) (μ : measure_theory.measure Ω) :
= ∫⁻ (ω : Ω), ennreal.of_real ((X ω - (x : Ω), X x μ) ^ 2) μ
theorem measure_theory.mem_ℒp.variance_eq_of_integral_eq_zero {Ω : Type u_1} {m : measurable_space Ω} {X : Ω } {μ : measure_theory.measure Ω} (hX : μ) (hXint : (x : Ω), X x μ = 0) :
= (x : Ω), (X ^ 2) x μ
theorem measure_theory.mem_ℒp.variance_eq {Ω : Type u_1} {m : measurable_space Ω} {X : Ω } {μ : measure_theory.measure Ω} (hX : μ) :
= (x : Ω), ((X - λ (ω : Ω), (x : Ω), X x μ) ^ 2) x μ
@[simp]
theorem probability_theory.evariance_eq_zero_iff {Ω : Type u_1} {m : measurable_space Ω} {X : Ω } {μ : measure_theory.measure Ω} (hX : μ) :
X =ᵐ[μ] λ (ω : Ω), (x : Ω), X x μ
theorem probability_theory.evariance_mul {Ω : Type u_1} {m : measurable_space Ω} (c : ) (X : Ω ) (μ : measure_theory.measure Ω) :
probability_theory.evariance (λ (ω : Ω), c * X ω) μ =
@[simp]
theorem probability_theory.variance_mul {Ω : Type u_1} {m : measurable_space Ω} (c : ) (X : Ω ) (μ : measure_theory.measure Ω) :
probability_theory.variance (λ (ω : Ω), c * X ω) μ = c ^ 2 *
theorem probability_theory.variance_smul {Ω : Type u_1} {m : measurable_space Ω} (c : ) (X : Ω ) (μ : measure_theory.measure Ω) :
μ = c ^ 2 *
theorem probability_theory.variance_smul' {Ω : Type u_1} {m : measurable_space Ω} {A : Type u_2} [ ] (c : A) (X : Ω ) (μ : 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.evariance_def' {Ω : Type u_1} {X : Ω }  :
= (∫⁻ (ω : Ω), X ω‖₊ ^ 2) - ennreal.of_real (( (a : Ω), X a) ^ 2)
theorem probability_theory.meas_ge_le_evariance_div_sq {Ω : Type u_1} {X : Ω } {c : nnreal} (hc : c 0) :
measure_theory.measure_space.volume {ω : Ω | c |X ω - (a : Ω), X a|}

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

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.