The realified Gaussian quadratic form

This file identifies the matrix quadratic form of limitCovMatrix with the scalar variance limitVar used in the characteristic-function statement of the main theorem.

theorem Anderson4D.realifiedLinearCoeff_quadratic (lam : ℝ) {s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : realifiedLinearCoeff c ⬝ᵥ (limitCovMatrix lam modes).mulVec (realifiedLinearCoeff c) = limitVar lam modes c

The real covariance matrix has exactly the scalar quadratic form specified by limitVar.

theorem Anderson4D.limitVar_nonneg_of_posSemidef (lam : ℝ) {s : ℕ} (modes : Fin s → Z4 × Z4) (hPSD : (limitCovMatrix lam modes).PosSemidef) (c : Fin s → ℂ) : 0 ≤ limitVar lam modes c

Positive semidefiniteness of the real covariance matrix implies the nonnegativity of every scalar variance used by the main theorem.

theorem Anderson4D.charFun_gaussianLimitLaw_realifiedLinearCoeff (lam : ℝ) {s : ℕ} (modes : Fin s → Z4 × Z4) (hlam : lam ^ 2 < 2 * Real.pi ^ 2) (hPSD : (limitCovMatrix lam modes).PosSemidef) (c : Fin s → ℂ) : MeasureTheory.charFun (↑(gaussianLimitLaw lam modes)) (WithLp.toLp 2 (realifiedLinearCoeff c)) = Complex.exp (-(↑(limitVar lam modes c) / 2))

Characteristic function of the explicit limit evaluated at the real-linear coefficient vector corresponding to Re ∑ⱼ cⱼ Zⱼ.