Prove2Me

variance_weighted_independent_sum_eq

Proved

by allychan327 · Jun 23, 2026 · Mathlib c5ea003 (Lean v4.30.0)

concentrationefron-steinprobabilityvariance

Variance of a coefficient-weighted independent sum (sharp linear Efron–Stein). For pairwise-independent, square-integrable real random variables {Xi}i∈ι\{X_i\}_{i\in\iota} indexed by a finite type, and real coefficients {ci}\{c_i\},

Var⁡ ⁣[∑iciXi]=∑ici2 Var⁡(Xi).\operatorname{Var}\!\Big[\sum_i c_i X_i\Big] = \sum_i c_i^2 \,\operatorname{Var}(X_i).

This is the distribution-dependent (sharp, equality) form of the tensorization of variance specialized to a linear functional — the variance proxy σ2\sigma^2 that the worst-case bounded-difference constant cannot capture. It follows from the variance of an independent sum being the sum of variances, composed with Var⁡(cX)=c2Var⁡(X)\operatorname{Var}(cX)=c^2\operatorname{Var}(X).

Preamble
import Mathlib.Probability.Moments.Variance
import Mathlib.Probability.Independence.Integration
open MeasureTheory ProbabilityTheory
open scoped ENNReal NNReal BigOperators
Formal statement
theorem variance_weighted_independent_sum_eq
    {Ω : Type*} {mΩ : MeasurableSpace Ω} {μ : Measure Ω}
    [IsProbabilityMeasure μ] {ι : Type*} [Fintype ι]
    (X : ι → Ω → ℝ) (coeff : ι → ℝ)
    (hX : ∀ i, MemLp (X i) 2 μ)
    (hindep : Set.Pairwise Set.univ (fun i j => IndepFun (X i) (X j) μ)) :
    variance (fun ω => ∑ i, coeff i * X i ω) μ
      = ∑ i, (coeff i) ^ 2 * variance (X i) μ := by sorry
Source
R. van Handel, Probability in High Dimension (APC 550, Princeton), §2.1, Theorem 2.3 (tensorization of variance, equality for linear f); Boucheron–Lugosi–Massart, Concentration Inequalities, Ch. 3.

View graph