Continuity of Variance for Finite Linear Combinations

Proved

FunctionalInequalities.Probability.tendsto_variance_finite_linear_combination_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is a finite-dimensional coefficient-continuity lemma for variance.

Let $\mu$ be a probability measure on a measurable space $\alpha$ , let $I$ be a finite index type, and let $f_i:\alpha\to\mathbb R$ satisfy $f_i\in L^2(\mu)$ for every $i$ . If $c_k(i)\to b(i)$ for every $i\in I$ , then

\operatorname{Var}_{\mu}\!\left(x\mapsto\sum_i c_k(i)f_i(x)\right) \longrightarrow \operatorname{Var}_{\mu}\!\left(x\mapsto\sum_i b(i)f_i(x)\right).

The conclusion is an ordinary real-valued limit of variances and is useful for passing coefficient approximations through quadratic or matrix observables.

Original Lean declaration header

Within namespace FunctionalInequalities.Probability. Shown in its original module context. Proof omitted.

theorem tendsto_variance_finite_linear_combination
    {alpha I : Type*} [MeasurableSpace alpha] [Fintype I]
    (mu : ProbabilityMeasure alpha) (f : I → alpha → ℝ)
    (hf : ∀ i, MemLp (f i) 2 (mu : Measure alpha))
    (c : ℕ → I → ℝ) (b : I → ℝ)
    (hc : ∀ i, Tendsto (fun k => c k i) atTop (𝓝 (b i))) :
    Tendsto (fun k => ProbabilityTheory.variance (fun x => ∑ i, c k i * f i x) (mu : Measure alpha))
      atTop (𝓝 (ProbabilityTheory.variance (fun x => ∑ i, b i * f i x) (mu : Measure alpha)))

Module navigation

Module: L2/MeanVariance.

Previous: inner_center_center.

Source excerpt, lines 358–365 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_L2_MeanVariance

open MeasureTheory Filter
open scoped Topology

Formal statement

theorem FunctionalInequalities.Probability.tendsto_variance_finite_linear_combination_readable
    {alpha I : Type*} [MeasurableSpace alpha] [Fintype I]
    (mu : ProbabilityMeasure alpha) (f : I → alpha → ℝ)
    (hf : ∀ i, MemLp (f i) 2 (mu : Measure alpha))
    (c : ℕ → I → ℝ) (b : I → ℝ)
    (hc : ∀ i, Tendsto (fun k => c k i) atTop (𝓝 (b i))) :
    Tendsto (fun k => ProbabilityTheory.variance (fun x => ∑ i, c k i * f i x) (mu : Measure alpha))
      atTop (𝓝 (ProbabilityTheory.variance (fun x => ∑ i, b i * f i x) (mu : Measure alpha))) := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/L2/MeanVariance.lean#L358-L388 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.L2.MeanVariance`, declaration `FunctionalInequalities.Probability.tendsto_variance_finite_linear_combination`; the repository is private at upload time).

View graph