Fourier coefficients of the four-point Green kernel

This file fixes the deterministic coefficient used in Proposition 3.6 and the limiting Gaussian law. It belongs to the continuum layer: no random parametrix or external probabilistic input is needed to state it.

noncomputable def Anderson4D.fourPointHCoeff (α₁ β₁ α₂ β₂ : Z4) : ℂ

Mode coefficients of the four-point kernel H (paper (3.25)): the pairing of fourPointH with characters in all four external variables, against paperMeasure in each. The iterated Bochner integrals use mathlib's standard junk value outside the integrable regime; downstream continuum lemmas prove the required integrability and compute the coefficient.

Equations

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