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
Main definitions #
Main results #
ℝ≥0∞-valued variance of a real-valued random variable defined as the Lebesgue integral of
(X - 𝔼[X])^2.
ℝ-valued variance of a real-valued random variable defined by applying
Chebyshev's inequality for
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.
The variance of a finite sum of pairwise independent random variables is the sum of the