Variance of random variables

We define the variance of a real-valued random variable as Var[X] = 𝔼[(X - 𝔼[X])^2] (in the ProbabilityTheory locale).

Main definitions

• ProbabilityTheory.evariance: the variance of a real-valued random variable as an extended non-negative real.
• ProbabilityTheory.variance: the variance of a real-valued random variable as a real number.

Main results

• ProbabilityTheory.variance_le_expectation_sq: the inequality Var[X] ≤ 𝔼[X^2].
• ProbabilityTheory.meas_ge_le_variance_div_sq: Chebyshev's inequality, i.e., ℙ {ω | c ≤ |X ω - 𝔼[X]|} ≤ ENNReal.ofReal (Var[X] / c ^ 2).
• ProbabilityTheory.meas_ge_le_evariance_div_sq: Chebyshev's inequality formulated with evariance without requiring the random variables to be L².
• ProbabilityTheory.IndepFun.variance_add: the variance of the sum of two independent random variables is the sum of the variances.
• ProbabilityTheory.IndepFun.variance_sum: the variance of a finite sum of pairwise independent random variables is the sum of the variances.

def ProbabilityTheory.evariance {Ω : Type u_1} : {x : MeasurableSpace Ω} → (Ω → ℝ) → MeasureTheory.Measure Ω → ENNReal

The ℝ≥0∞-valued variance of a real-valued random variable defined as the Lebesgue integral of (X - 𝔼[X])^2.

def ProbabilityTheory.variance {Ω : Type u_1} : {x : MeasurableSpace Ω} → (Ω → ℝ) → MeasureTheory.Measure Ω → ℝ

The ℝ-valued variance of a real-valued random variable defined by applying ENNReal.toReal to evariance.

theorem MeasureTheory.Memℒp.evariance_lt_top {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.Memℒp X 2) : ProbabilityTheory.evariance X μ < ⊤

theorem ProbabilityTheory.evariance_eq_top {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (hXm : MeasureTheory.AEStronglyMeasurable X μ) (hX : ¬MeasureTheory.Memℒp X 2) : ProbabilityTheory.evariance X μ = ⊤

theorem ProbabilityTheory.evariance_lt_top_iff_memℒp {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.AEStronglyMeasurable X μ) : ProbabilityTheory.evariance X μ < ⊤ ↔ MeasureTheory.Memℒp X 2

theorem MeasureTheory.Memℒp.ofReal_variance_eq {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.Memℒp X 2) : ENNReal.ofReal (ProbabilityTheory.variance X μ) = ProbabilityTheory.evariance X μ

theorem ProbabilityTheory.evariance_eq_lintegral_ofReal {Ω : Type u_1} {m : MeasurableSpace Ω} (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω) : ProbabilityTheory.evariance X μ = ∫⁻ (ω : Ω), ENNReal.ofReal ((X ω - ∫ (x : Ω), X x ∂μ) ^ 2) ∂μ

theorem MeasureTheory.Memℒp.variance_eq_of_integral_eq_zero {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (hX : MeasureTheory.Memℒp X 2) (hXint : ∫ (x : Ω), X x ∂μ = 0) : ProbabilityTheory.variance X μ = ∫ (x : Ω), (X ^ 2) x ∂μ

theorem MeasureTheory.Memℒp.variance_eq {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.Memℒp X 2) : ProbabilityTheory.variance X μ = ∫ (x : Ω), ((X - fun x => ∫ (x : Ω), X x ∂μ) ^ 2) x ∂μ

@[simp]

theorem ProbabilityTheory.evariance_zero {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} : ProbabilityTheory.evariance 0 μ = 0

theorem ProbabilityTheory.evariance_eq_zero_iff {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (hX : AEMeasurable X) : ProbabilityTheory.evariance X μ = 0 ↔ X =ᶠ[MeasureTheory.Measure.ae μ] fun x => ∫ (x : Ω), X x ∂μ

theorem ProbabilityTheory.evariance_mul {Ω : Type u_1} {m : MeasurableSpace Ω} (c : ℝ) (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω) : ProbabilityTheory.evariance (fun ω => c * X ω) μ = ENNReal.ofReal (c ^ 2) * ProbabilityTheory.evariance X μ

def ProbabilityTheory.«termEVar[_]» : Lean.ParserDescr

@[simp]

theorem ProbabilityTheory.variance_zero {Ω : Type u_1} {m : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω) : ProbabilityTheory.variance 0 μ = 0

theorem ProbabilityTheory.variance_nonneg {Ω : Type u_1} {m : MeasurableSpace Ω} (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω) : 0 ≤ ProbabilityTheory.variance X μ

theorem ProbabilityTheory.variance_mul {Ω : Type u_1} {m : MeasurableSpace Ω} (c : ℝ) (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω) : ProbabilityTheory.variance (fun ω => c * X ω) μ = c ^ 2 * ProbabilityTheory.variance X μ

theorem ProbabilityTheory.variance_smul {Ω : Type u_1} {m : MeasurableSpace Ω} (c : ℝ) (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω) : ProbabilityTheory.variance (c • X) μ = c ^ 2 * ProbabilityTheory.variance X μ

theorem ProbabilityTheory.variance_smul' {Ω : Type u_1} {m : MeasurableSpace Ω} {A : Type u_2} [CommSemiring A] [Algebra A ℝ] (c : A) (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω) : ProbabilityTheory.variance (c • X) μ = c ^ 2 • ProbabilityTheory.variance X μ

def ProbabilityTheory.«termVar[_]» : Lean.ParserDescr

theorem ProbabilityTheory.variance_def' {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {X : Ω → ℝ} (hX : MeasureTheory.Memℒp X 2) : ProbabilityTheory.variance X MeasureTheory.volume = (∫ (a : Ω), (X ^ 2) a) - (∫ (a : Ω), X a) ^ 2

theorem ProbabilityTheory.variance_le_expectation_sq {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {X : Ω → ℝ} (hm : MeasureTheory.AEStronglyMeasurable X MeasureTheory.volume) : ProbabilityTheory.variance X MeasureTheory.volume ≤ ∫ (a : Ω), (X ^ 2) a

theorem ProbabilityTheory.evariance_def' {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {X : Ω → ℝ} (hX : MeasureTheory.AEStronglyMeasurable X MeasureTheory.volume) : ProbabilityTheory.evariance X MeasureTheory.volume = (∫⁻ (ω : Ω), ↑(‖X ω‖₊ ^ 2)) - ENNReal.ofReal ((∫ (a : Ω), X a) ^ 2)

theorem ProbabilityTheory.meas_ge_le_evariance_div_sq {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] {X : Ω → ℝ} (hX : MeasureTheory.AEStronglyMeasurable X MeasureTheory.volume) {c : NNReal} (hc : c ≠ 0) : ↑↑MeasureTheory.volume {ω | ↑c ≤ |X ω - ∫ (a : Ω), X a|} ≤ ProbabilityTheory.evariance X MeasureTheory.volume / ↑(c ^ 2)

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

theorem ProbabilityTheory.meas_ge_le_variance_div_sq {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsFiniteMeasure MeasureTheory.volume] {X : Ω → ℝ} (hX : MeasureTheory.Memℒp X 2) {c : ℝ} (hc : 0 < c) : ↑↑MeasureTheory.volume {ω | c ≤ |X ω - ∫ (a : Ω), X a|} ≤ ENNReal.ofReal (ProbabilityTheory.variance X MeasureTheory.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 ProbabilityTheory.IndepFun.variance_add {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {X : Ω → ℝ} {Y : Ω → ℝ} (hX : MeasureTheory.Memℒp X 2) (hY : MeasureTheory.Memℒp Y 2) (h : ProbabilityTheory.IndepFun X Y) : ProbabilityTheory.variance (X + Y) MeasureTheory.volume = ProbabilityTheory.variance X MeasureTheory.volume + ProbabilityTheory.variance Y MeasureTheory.volume

The variance of the sum of two independent random variables is the sum of the variances.

theorem ProbabilityTheory.IndepFun.variance_sum {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {ι : Type u_2} {X : ι → Ω → ℝ} {s : Finset ι} (hs : ∀ (i : ι), i ∈ s → MeasureTheory.Memℒp (X i) 2) (h : Set.Pairwise ↑s fun i j => ProbabilityTheory.IndepFun (X i) (X j)) : ProbabilityTheory.variance (Finset.sum s fun i => X i) MeasureTheory.volume = Finset.sum s fun i => ProbabilityTheory.variance (X i) MeasureTheory.volume

The variance of a finite sum of pairwise independent random variables is the sum of the variances.