The finite-dimensional Gaussian limit law

This file implements node D-limit at the statement/construction level. A complex family of s Fourier modes is realified as the Euclidean space indexed by Fin s × Bool, with false denoting the real coordinate and true the imaginary coordinate. The covariance and pseudo-covariance prescribed by paper (1.3), (3.25), and (3.28) are expanded into the four real covariance blocks.

gaussianLimitLaw is total: outside λ² < 2π² it is the Dirac mass at zero. Inside that range it is mathlib's multivariate Gaussian for the explicit matrix below. Positive semidefiniteness follows from the Gram form of the four-point kernel.

noncomputable def Anderson4D.limitPrefactor (lam : ℝ) : ℝ

The scalar multiplying the four-point covariance in paper (1.3).

Equations

• Anderson4D.limitPrefactor lam = 2 * Real.pi ^ 2 / (2 * Real.pi ^ 2 - lam ^ 2)

noncomputable def Anderson4D.limitPseudoCov (lam : ℝ) {s : ℕ} (modes : Fin s → Z4 × Z4) (i j : Fin s) : ℂ

Complex pseudo-covariance E[Zᵢ Zⱼ] of the proposed limit.

Equations

• Anderson4D.limitPseudoCov lam modes i j = ↑(Anderson4D.limitPrefactor lam) * Anderson4D.fourPointHCoeff (modes i).1 (modes i).2 (modes j).1 (modes j).2

noncomputable def Anderson4D.limitConjCov (lam : ℝ) {s : ℕ} (modes : Fin s → Z4 × Z4) (i j : Fin s) : ℂ

Complex covariance E[Zᵢ conj Zⱼ], obtained by adjoining the conjugate (negated) mode.

Equations

• Anderson4D.limitConjCov lam modes i j = ↑(Anderson4D.limitPrefactor lam) * Anderson4D.fourPointHCoeff (modes i).1 (modes i).2 (-(modes j).1) (-(modes j).2)

noncomputable def Anderson4D.limitCovMatrix (lam : ℝ) {s : ℕ} (modes : Fin s → Z4 × Z4) : Matrix (Fin s × Bool) (Fin s × Bool) ℝ

Real covariance matrix of the realification (Re Zᵢ, Im Zᵢ). For Pᵢⱼ = E[ZᵢZⱼ] and Qᵢⱼ = E[Zᵢ conj Zⱼ], the four blocks are

• E[Re Zᵢ Re Zⱼ] = Re(Pᵢⱼ + Qᵢⱼ)/2,
• E[Re Zᵢ Im Zⱼ] = Im(Pᵢⱼ - Qᵢⱼ)/2,
• E[Im Zᵢ Re Zⱼ] = Im(Pᵢⱼ + Qᵢⱼ)/2,
• E[Im Zᵢ Im Zⱼ] = Re(Qᵢⱼ - Pᵢⱼ)/2.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Anderson4D.limitVar (lam : ℝ) {s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : ℝ

Limit variance quadratic form (node D-limit): the variance of Re ∑ⱼ cⱼ Zⱼ, expressed directly through covariance and pseudo-covariance.

Equations

• One or more equations did not get rendered due to their size.

def Anderson4D.realifiedLinearCoeff {s : ℕ} (c : Fin s → ℂ) : Fin s × Bool → ℝ

Coefficients of the real linear functional z ↦ Re ∑ⱼ cⱼ zⱼ on the realified mode space.

Equations

• Anderson4D.realifiedLinearCoeff c (j, false) = (c j).re
• Anderson4D.realifiedLinearCoeff c (j, true) = -(c j).im

noncomputable def Anderson4D.gaussianLimitLaw (lam : ℝ) {s : ℕ} (modes : Fin s → Z4 × Z4) : MeasureTheory.ProbabilityMeasure (EuclideanSpace ℝ (Fin s × Bool))

The explicit centered Gaussian law on the realified mode space. Outside the subcritical denominator range it is junk-totalized to δ₀, as fixed in DESIGN §2.2 and §5.7.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.gaussianLimitLaw_of_sq_lt (lam : ℝ) {s : ℕ} (modes : Fin s → Z4 × Z4) (hlam : lam ^ 2 < 2 * Real.pi ^ 2) : ↑(gaussianLimitLaw lam modes) = ProbabilityTheory.multivariateGaussian 0 (limitCovMatrix lam modes)

theorem Anderson4D.gaussianLimitLaw_of_sq_not_lt (lam : ℝ) {s : ℕ} (modes : Fin s → Z4 × Z4) (hlam : ¬lam ^ 2 < 2 * Real.pi ^ 2) : ↑(gaussianLimitLaw lam modes) = MeasureTheory.Measure.dirac 0

theorem Anderson4D.charFun_gaussianLimitLaw (lam : ℝ) {s : ℕ} (modes : Fin s → Z4 × Z4) (hlam : lam ^ 2 < 2 * Real.pi ^ 2) (hPSD : (limitCovMatrix lam modes).PosSemidef) (t : EuclideanSpace ℝ (Fin s × Bool)) : MeasureTheory.charFun (↑(gaussianLimitLaw lam modes)) t = Complex.exp (-↑(t.ofLp ⬝ᵥ (limitCovMatrix lam modes).mulVec t.ofLp) / 2)

Characteristic function of the explicit limit law, conditional only on the analytic PSD obligation for its covariance matrix.

theorem Anderson4D.covariance_gaussianLimitLaw (lam : ℝ) {s : ℕ} (modes : Fin s → Z4 × Z4) (hlam : lam ^ 2 < 2 * Real.pi ^ 2) (hPSD : (limitCovMatrix lam modes).PosSemidef) (p q : Fin s × Bool) : ProbabilityTheory.covariance (fun (x : EuclideanSpace ℝ (Fin s × Bool)) => x.ofLp p) (fun (x : EuclideanSpace ℝ (Fin s × Bool)) => x.ofLp q) ↑(gaussianLimitLaw lam modes) = limitCovMatrix lam modes p q

Coordinate covariance of the explicit limit law, again separated cleanly from the four-point-kernel PSD proof.