mathlib3 documentation

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 #

Main results #

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.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) :
probability_theory.variance X μ = (x : Ω), (X ^ 2) x μ
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 μ) :
probability_theory.variance X μ = (x : Ω), ((X - λ (ω : Ω), (x : Ω), X x μ) ^ 2) x μ
theorem probability_theory.evariance_eq_zero_iff {Ω : Type u_1} {m : measurable_space Ω} {X : Ω } {μ : measure_theory.measure Ω} (hX : ae_measurable X μ) :
probability_theory.evariance X μ = 0 X =ᵐ[μ] λ (ω : Ω), (x : Ω), X 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 μ

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.