Continuity of Variance for Quadratic Matrix Forms

This formalizes the coefficient-continuity part of Lemma A.2 of Letwin (arXiv:2607.24164v1), cited as “Reduction to invertible $M$.”

Let $\mu$ be a probability measure on $E=\mathrm{EuclideanSpace}\,\mathbb R\,(\mathrm{Fin}\,n)$ with finite fourth moment. Let $A_k$ and $A$ be real $n\times n$ matrices with $A_k\to A$ entrywise (equivalently in the finite-dimensional matrix topology). Then

The declaration supplies the fourth-moment continuity needed in singular extensions of matrix variance bounds; it does not itself assert a numerical variance estimate.

Original Lean declaration header

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

set_option maxHeartbeats 500000 in
theorem tendsto_variance_quadratic_matrix_forms {n : ℕ}
    (mu : ProbabilityMeasure (EuclideanSpace ℝ (Fin n)))
    (h4 : MemLp (id : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) 4 (mu : Measure _))
    {seq : ℕ → Matrix (Fin n) (Fin n) ℝ} {A : Matrix (Fin n) (Fin n) ℝ}
    (hseq : Tendsto seq atTop (𝓝 A)) :
    Tendsto (fun k => ProbabilityTheory.variance
      (fun x : EuclideanSpace ℝ (Fin n) => ∑ i, ∑ j, seq k i j * x i * x j) (mu : Measure _))
      atTop (𝓝 (ProbabilityTheory.variance
        (fun x : EuclideanSpace ℝ (Fin n) => ∑ i, ∑ j, A i j * x i * x j) (mu : Measure _)))

Module navigation

Module: Probability/QuadraticVariance.

Supporting theorems: tendsto_variance_finite_linear_combination.

Next: quadratic_variance_le_centered_noise_convolution.

Source excerpt, lines 23–32 · Frozen source 408915f.