Fourier coefficients of the torus heat and Green kernels

This file supplies the normalization-sensitive part of blueprint node I-green. The intended endpoint is the paper-normalized identity Ĝ(k) = (1 + |k|²)⁻¹. The first ingredient below is a period-p unfolding lemma for integrable functions on ℝ.

The one-dimensional Gaussian coefficient

theorem Anderson4D.heatKernelT4_eq_periodizedGaussian_prod {t : ℝ} (ht : 0 < t) (z : T4) : ↑(heatKernelT4 t z) = ↑((4 * Real.pi * t) ^ (-2)) * ∏ i : Fin dim, Anderson4D.circlePeriodize✝ (2 * Real.pi) (Anderson4D.gaussian1C✝ t) (z i)

Product factorization of the four-dimensional heat kernel into one-dimensional periodized Gaussians.

theorem Anderson4D.paperFourierCoeff_heatKernelT4 {t : ℝ} (ht : 0 < t) (k : Z4) : ∫ (z : T4), charT4 k z * ↑(heatKernelT4 t z) ∂paperMeasure = Complex.exp ↑(-t * ∑ i : Fin dim, ↑(k i) ^ 2)

Paper-normalized Fourier coefficient of the torus heat kernel.

theorem Anderson4D.paperFourierCoeff_greenFn (k : Z4) : ∫ (z : T4), charT4 k z * ↑(greenFn z) ∂paperMeasure = ↑(1 + ∑ i : Fin dim, ↑(k i) ^ 2)⁻¹

Fourier coefficient of the heat-kernel definition of the Green function, with the paper's unnormalized reference measure.

theorem Anderson4D.integral_greenFn_paper : ∫ (z : T4), greenFn z ∂paperMeasure = 1

The Green function has total mass one for the paper's Lebesgue normalization.

theorem Anderson4D.integrable_greenFn_paper : MeasureTheory.Integrable greenFn paperMeasure

In particular, the heat-kernel Green function is Bochner integrable despite its diagonal singularity.