Positive semidefiniteness of the explicit Gaussian limit covariance

The four-point Fourier coefficient is a bilinear Gram form. Combining its bilinear and Hermitian specializations shows that limitVar is the integral of the square of the real part of a finite profile combination, which proves positive semidefiniteness of gaussianLimitLaw.

Elementary symmetries of the four-point coefficient

theorem Anderson4D.fourPointHCoeff_swap_pairs (α₁ β₁ α₂ β₂ : Z4) : fourPointHCoeff α₁ β₁ α₂ β₂ = fourPointHCoeff α₂ β₂ α₁ β₁

Swapping the two pairs of external modes leaves the four-point coefficient unchanged.

theorem Anderson4D.fourPointHCoeff_cross_swap (α₁ β₁ α₂ β₂ : Z4) : fourPointHCoeff α₁ β₁ (-α₂) (-β₂) = fourPointHCoeff α₂ β₂ (-α₁) (-β₁)

After negating the second pair, swapping the two unnegated pairs preserves the coefficient.

theorem Anderson4D.fourPointHCoeff_im_eq_zero (α₁ β₁ α₂ β₂ : Z4) : (fourPointHCoeff α₁ β₁ α₂ β₂).im = 0

Every four-point Fourier coefficient is real.

theorem Anderson4D.limitPseudoCov_comm (lam : ℝ) {s : ℕ} (modes : Fin s → Z4 × Z4) (i j : Fin s) : limitPseudoCov lam modes i j = limitPseudoCov lam modes j i

theorem Anderson4D.limitConjCov_comm (lam : ℝ) {s : ℕ} (modes : Fin s → Z4 × Z4) (i j : Fin s) : limitConjCov lam modes i j = limitConjCov lam modes j i

theorem Anderson4D.limitPseudoCov_im_eq_zero (lam : ℝ) {s : ℕ} (modes : Fin s → Z4 × Z4) (i j : Fin s) : (limitPseudoCov lam modes i j).im = 0

theorem Anderson4D.limitConjCov_im_eq_zero (lam : ℝ) {s : ℕ} (modes : Fin s → Z4 × Z4) (i j : Fin s) : (limitConjCov lam modes i j).im = 0

theorem Anderson4D.limitCovMatrix_isHermitian (lam : ℝ) {s : ℕ} (modes : Fin s → Z4 × Z4) : (limitCovMatrix lam modes).IsHermitian

The block matrix obtained by realifying the complex covariance is symmetric (hence Hermitian over ℝ).

Real vectors as complex coefficients

def Anderson4D.complexCoeffOfRealified {s : ℕ} (v : Fin s × Bool → ℝ) (i : Fin s) : ℂ

Inverse to realifiedLinearCoeff: the minus sign compensates for the convention used by Re (cᵢ Zᵢ).

Equations

• Anderson4D.complexCoeffOfRealified v i = ↑(v (i, false)) - Complex.I * ↑(v (i, true))

@[simp]

theorem Anderson4D.realifiedLinearCoeff_complexCoeffOfRealified {s : ℕ} (v : Fin s × Bool → ℝ) : realifiedLinearCoeff (complexCoeffOfRealified v) = v

The bilinear profile identity

theorem Anderson4D.integrable_fourPointProfileCombination_mul_self {s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : MeasureTheory.Integrable (fun (z : T4) => fourPointProfileCombination modes c z * fourPointProfileCombination modes c z) paperMeasure

theorem Anderson4D.sum_fourPointHCoeff_eq_profileCombination_sq {s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : ∑ i : Fin s, ∑ j : Fin s, c i * c j * fourPointHCoeff (modes i).1 (modes i).2 (modes j).1 (modes j).2 = ∫ (z : T4), fourPointProfileCombination modes c z * fourPointProfileCombination modes c z ∂paperMeasure

The non-Hermitian finite four-point form is the integral of the square (without conjugation) of the same profile combination.

The scalar variance as an integral of a square

theorem Anderson4D.limitVar_eq_integral_re_sq (lam : ℝ) {s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : limitVar lam modes c = limitPrefactor lam * ∫ (z : T4), (fourPointProfileCombination modes c z).re ^ 2 ∂paperMeasure

The explicit scalar variance is the positive prefactor times the integral of the square of the real part of a profile combination.

theorem Anderson4D.limitPrefactor_pos (lam : ℝ) (hlam : lam ^ 2 < 2 * Real.pi ^ 2) : 0 < limitPrefactor lam

The scalar multiplying the limiting four-point covariance is strictly positive throughout the subcritical parameter range.

theorem Anderson4D.limitVar_nonneg (lam : ℝ) {s : ℕ} (modes : Fin s → Z4 × Z4) (hlam : lam ^ 2 < 2 * Real.pi ^ 2) (c : Fin s → ℂ) : 0 ≤ limitVar lam modes c

Direct nonnegativity of the scalar limit variance, with no separate matrix-positivity hypothesis.

Positive semidefiniteness and unconditional corollaries

theorem Anderson4D.limitCovMatrix_posSemidef (lam : ℝ) {s : ℕ} (modes : Fin s → Z4 × Z4) (hlam : lam ^ 2 < 2 * Real.pi ^ 2) : (limitCovMatrix lam modes).PosSemidef

PSD completion of node D-limit. The explicit realified covariance matrix is positive semidefinite for every subcritical coupling.

theorem Anderson4D.charFun_gaussianLimitLaw_of_subcritical (lam : ℝ) {s : ℕ} (modes : Fin s → Z4 × Z4) (hlam : lam ^ 2 < 2 * Real.pi ^ 2) (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 Gaussian limit, now discharged solely from the subcritical parameter inequality.

theorem Anderson4D.covariance_gaussianLimitLaw_of_subcritical (lam : ℝ) {s : ℕ} (modes : Fin s → Z4 × Z4) (hlam : lam ^ 2 < 2 * Real.pi ^ 2) (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 Gaussian limit, with the PSD obligation discharged.

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

Scalar characteristic-function formula for Re ∑ᵢ cᵢ Zᵢ, without an extra PSD hypothesis.