Heat-kernel and Green's function estimates (blueprint node I-green)

Basic estimates for the periodized heat kernel heatKernelT4 and the Green's function greenFn:

• summability of the periodization (summable_heatKernel_terms), positivity (heatKernelT4_pos) and symmetry (heatKernelT4_memE);
• the paper's bound (4.1) for k = 0: greenFn z ≤ C / torusDistSq z (greenFn_le), via the split |z̃ + 2πk|² ≥ |z̃|²/2 + π²|k|²/2 and the exact identity ∫_0^∞ t⁻² e^{-a/t} dt = a⁻¹;
• greenFn_memE and greenFn_nonneg.

theorem Anderson4D.latticeDistSq_nonneg (z : T4) (k : Z4) : 0 ≤ latticeDistSq z k

Summability of the periodization

theorem Anderson4D.summable_heatKernel_terms {t : ℝ} (ht : 0 < t) (z : T4) : Summable fun (k : Z4) => (4 * Real.pi * t) ^ (-2) * Real.exp (-latticeDistSq z k / (4 * t))

Positivity

theorem Anderson4D.heatKernelT4_nonneg (t : ℝ) (z : T4) : 0 ≤ heatKernelT4 t z

theorem Anderson4D.heatKernelT4_pos {t : ℝ} (ht : 0 < t) (z : T4) : 0 < heatKernelT4 t z

Symmetry: the heat kernel lies in the class 𝓔

theorem Anderson4D.heatKernelT4_memE (t : ℝ) : MemEClassT4 (heatKernelT4 t)

The heat kernel lies in the hyperoctahedral symmetry class 𝓔 (paper Def. 2.1) for every t.

The Gaussian-sum bound ∑_{m∈ℤ} e^{-cm²} ≤ 2(1 + c⁻¹)

Pointwise heat-kernel bound

theorem Anderson4D.pointwise_bound {t : ℝ} (ht : 0 < t) (z : T4) : Real.exp (-t) * heatKernelT4 t z ≤ 256 / Real.pi ^ 2 * ((t ^ 2)⁻¹ * Real.exp (-(torusDistSq z / 8 / t)))

The integrand bound feeding (4.1): for t > 0, e⁻ᵗ Θ(t,z) ≤ (256/π²) t⁻² e^{-|z̃|²/(8t)}.

The exact time integral ∫_0^∞ t⁻² e^{-a/t} dt = a⁻¹

theorem Anderson4D.integral_inv_sq_exp {a : ℝ} (ha : 0 < a) : ∫ (t : ℝ) in Set.Ioi 0, (t ^ 2)⁻¹ * Real.exp (-(a / t)) = a⁻¹

theorem Anderson4D.integrableOn_inv_sq_exp {a : ℝ} (ha : 0 < a) : MeasureTheory.IntegrableOn (fun (t : ℝ) => (t ^ 2)⁻¹ * Real.exp (-(a / t))) (Set.Ioi 0) MeasureTheory.volume

Green's function: positivity, symmetry, and the (4.1) bound

theorem Anderson4D.greenFn_nonneg (z : T4) : 0 ≤ greenFn z

theorem Anderson4D.greenFn_memE : MemEClassT4 greenFn

The Green's function lies in the symmetry class 𝓔 (blueprint node I-green; inherited from heatKernelT4_memE under the time integral).

theorem Anderson4D.greenFn_le : ∃ (C : ℝ), 0 < C ∧ ∀ (z : T4), torusDistSq z ≠ 0 → greenFn z ≤ C / torusDistSq z

Paper estimate (4.1) for the free Green's function (k = 0 case): G(z) ≤ C |z̃|⁻² with an explicit constant, where |z̃|² = torusDistSq z is the squared canonical lift.