Derivatives of the local Euclidean part of the Green kernel

The singular summand of the periodized Bessel kernel is the k = 0 Euclidean heat kernel. This file differentiates that summand under its time integral. The resulting first- and second-coordinate derivative formulas, together with explicit |x|⁻³ and |x|⁻⁴ majorants, are the singular part of paper (4.1).

noncomputable def Anderson4D.euclideanBessel4 (x : R4) : ℝ

The k = 0 Euclidean contribution to the Bessel Green kernel.

Equations

• Anderson4D.euclideanBessel4 x = ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-t) * Anderson4D.euclideanHeatKernel4 t x

noncomputable def Anderson4D.euclideanHeatGrad (t : ℝ) (x : R4) (i : Fin dim) : ℝ

Coordinate derivative of the Euclidean heat kernel.

Equations

• Anderson4D.euclideanHeatGrad t x i = -x i / (2 * t) * Anderson4D.euclideanHeatKernel4 t x

noncomputable def Anderson4D.euclideanHeatHess (t : ℝ) (x : R4) (i j : Fin dim) : ℝ

Coordinate Hessian entry of the Euclidean heat kernel.

Equations

• Anderson4D.euclideanHeatHess t x i j = (x i * x j / (4 * t ^ 2) - if i = j then (2 * t)⁻¹ else 0) * Anderson4D.euclideanHeatKernel4 t x

noncomputable def Anderson4D.euclideanBesselGrad (x : R4) (i : Fin dim) : ℝ

First-coordinate derivative candidate after the Bessel time integral.

Equations

• Anderson4D.euclideanBesselGrad x i = ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-t) * Anderson4D.euclideanHeatGrad t x i

noncomputable def Anderson4D.euclideanBesselHess (x : R4) (i j : Fin dim) : ℝ

Coordinate Hessian candidate after the Bessel time integral.

Equations

• Anderson4D.euclideanBesselHess x i j = ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-t) * Anderson4D.euclideanHeatHess t x i j

noncomputable def Anderson4D.greenLocalLift (x : R4) : ℝ

The Green function pulled back along the coordinatewise quotient ℝ⁴ → 𝕋⁴. On the principal cube its singular summand is euclideanBessel4.

Equations

• Anderson4D.greenLocalLift x = Anderson4D.greenFn fun (i : Fin Anderson4D.dim) => ↑(x i)

noncomputable def Anderson4D.greenLocalPoint (x : R4) : T4

Coordinatewise quotient point associated with a Euclidean lift.

Equations

• Anderson4D.greenLocalPoint x i = ↑(x i)

noncomputable def Anderson4D.greenLocalRemainder (x : R4) : ℝ

The regular part left after removing the local Euclidean Bessel summand from the pulled-back torus Green function.

Equations

• Anderson4D.greenLocalRemainder x = Anderson4D.greenLocalLift x - Anderson4D.euclideanBessel4 x

theorem Anderson4D.greenLocalLift_eq (x : R4) : greenLocalLift x = greenFn (greenLocalPoint x)

theorem Anderson4D.greenLocalLift_decomposition (x : R4) : greenLocalLift x = euclideanBessel4 x + greenLocalRemainder x

theorem Anderson4D.torusLift_greenLocalPoint {x : R4} (hx : ∀ (i : Fin dim), x i ∈ Set.Ico (-Real.pi) Real.pi) : torusLift (greenLocalPoint x) = x

theorem Anderson4D.latticeDistSq_greenLocalPoint_zero {x : R4} (hx : ∀ (i : Fin dim), x i ∈ Set.Ico (-Real.pi) Real.pi) : latticeDistSq (greenLocalPoint x) 0 = euclideanDistSq x

theorem Anderson4D.euclideanHeatKernel4_eq_greenLocalTerm_zero {x : R4} (hx : ∀ (i : Fin dim), x i ∈ Set.Ico (-Real.pi) Real.pi) (t : ℝ) : euclideanHeatKernel4 t x = (4 * Real.pi * t) ^ (-2) * Real.exp (-latticeDistSq (greenLocalPoint x) 0 / (4 * t))

On the principal cube, the Euclidean heat kernel is exactly the zero lattice summand of the heat kernel defining greenLocalLift.

theorem Anderson4D.euclideanHeatKernel4_le_heatKernelT4_greenLocal {x : R4} (hx : ∀ (i : Fin dim), x i ∈ Set.Ico (-Real.pi) Real.pi) {t : ℝ} (ht : 0 < t) : euclideanHeatKernel4 t x ≤ heatKernelT4 t (greenLocalPoint x)

The local Euclidean heat kernel is a genuine summand, rather than an auxiliary comparison kernel: it is bounded by the periodized heat kernel whose Bessel integral defines greenFn.

def Anderson4D.coordLine (x : R4) (i : Fin dim) (s : ℝ) : R4

Coordinate line through a Euclidean lift.

Equations

• Anderson4D.coordLine x i s = x + s • Pi.single i 1

theorem Anderson4D.hasDerivAt_euclideanHeatKernel4_coord {t : ℝ} (ht : t ≠ 0) (x : R4) (i : Fin dim) : HasDerivAt (fun (s : ℝ) => euclideanHeatKernel4 t (coordLine x i s)) (euclideanHeatGrad t x i) 0

theorem Anderson4D.hasDerivAt_euclideanHeatKernel4_coord_at {t : ℝ} (ht : t ≠ 0) (x : R4) (i : Fin dim) (s : ℝ) : HasDerivAt (fun (r : ℝ) => euclideanHeatKernel4 t (coordLine x i r)) (euclideanHeatGrad t (coordLine x i s) i) s

theorem Anderson4D.hasDerivAt_euclideanHeatGrad_coord {t : ℝ} (ht : t ≠ 0) (x : R4) (i j : Fin dim) : HasDerivAt (fun (s : ℝ) => euclideanHeatGrad t (coordLine x j s) i) (euclideanHeatHess t x i j) 0

theorem Anderson4D.hasDerivAt_euclideanHeatGrad_coord_at {t : ℝ} (ht : t ≠ 0) (x : R4) (i j : Fin dim) (s : ℝ) : HasDerivAt (fun (r : ℝ) => euclideanHeatGrad t (coordLine x j r) i) (euclideanHeatHess t (coordLine x j s) i j) s

theorem Anderson4D.abs_euclideanHeatGrad {t : ℝ} (ht : 0 < t) (x : R4) (i : Fin dim) : |euclideanHeatGrad t x i| = |x i| / (32 * Real.pi ^ 2) * ((t ^ 3)⁻¹ * Real.exp (-(euclideanDistSq x / 4 / t)))

theorem Anderson4D.integrableOn_euclideanHeatGrad {x : R4} (hx : euclideanDistSq x ≠ 0) (i : Fin dim) : MeasureTheory.IntegrableOn (fun (t : ℝ) => euclideanHeatGrad t x i) (Set.Ioi 0) MeasureTheory.volume

theorem Anderson4D.integral_abs_euclideanHeatGrad {x : R4} (hx : euclideanDistSq x ≠ 0) (i : Fin dim) : ∫ (t : ℝ) in Set.Ioi 0, |euclideanHeatGrad t x i| = |x i| / (2 * Real.pi ^ 2) * (euclideanDistSq x)⁻¹ ^ 2

theorem Anderson4D.abs_euclideanHeatHess_le {t : ℝ} (ht : 0 < t) (x : R4) (i j : Fin dim) : |euclideanHeatHess t x i j| ≤ |x i * x j| / (64 * Real.pi ^ 2) * ((t ^ 4)⁻¹ * Real.exp (-(euclideanDistSq x / 4 / t))) + 1 / (32 * Real.pi ^ 2) * ((t ^ 3)⁻¹ * Real.exp (-(euclideanDistSq x / 4 / t)))

theorem Anderson4D.integrableOn_euclideanHeatHess {x : R4} (hx : euclideanDistSq x ≠ 0) (i j : Fin dim) : MeasureTheory.IntegrableOn (fun (t : ℝ) => euclideanHeatHess t x i j) (Set.Ioi 0) MeasureTheory.volume

theorem Anderson4D.integral_abs_euclideanHeatHess_le {x : R4} (hx : euclideanDistSq x ≠ 0) (i j : Fin dim) : ∫ (t : ℝ) in Set.Ioi 0, |euclideanHeatHess t x i j| ≤ |x i * x j| / (64 * Real.pi ^ 2) * (2 * (euclideanDistSq x / 4)⁻¹ ^ 3) + 1 / (32 * Real.pi ^ 2) * (euclideanDistSq x / 4)⁻¹ ^ 2

theorem Anderson4D.hasDerivAt_euclideanBessel4_coord {x : R4} (hx : euclideanDistSq x ≠ 0) (i : Fin dim) : HasDerivAt (fun (s : ℝ) => euclideanBessel4 (coordLine x i s)) (euclideanBesselGrad x i) 0

The k = 0 Bessel contribution is genuinely differentiable in every coordinate away from its singular point, with derivative obtained by differentiating the heat kernel under the time integral.

theorem Anderson4D.abs_euclideanBesselGrad_le {x : R4} (hx : euclideanDistSq x ≠ 0) (i : Fin dim) : |euclideanBesselGrad x i| ≤ |x i| / (2 * Real.pi ^ 2) * (euclideanDistSq x)⁻¹ ^ 2

Explicit |x|⁻³-scale bound for each coordinate derivative of the local Bessel contribution. The anisotropic numerator is useful in the later Taylor contraction and is exactly the time-integrated Gaussian bound.

theorem Anderson4D.hasDerivAt_euclideanBesselGrad_coord {x : R4} (hx : euclideanDistSq x ≠ 0) (i j : Fin dim) : HasDerivAt (fun (s : ℝ) => euclideanBesselGrad (coordLine x j s) i) (euclideanBesselHess x i j) 0

The time-integrated first derivative is itself differentiable away from the singularity; its coordinate derivative is the time-integrated Hessian. This is the genuine k = 2 local Bessel part of (4.1).

theorem Anderson4D.abs_euclideanBesselHess_le {x : R4} (hx : euclideanDistSq x ≠ 0) (i j : Fin dim) : |euclideanBesselHess x i j| ≤ |x i * x j| / (64 * Real.pi ^ 2) * (2 * (euclideanDistSq x / 4)⁻¹ ^ 3) + 1 / (32 * Real.pi ^ 2) * (euclideanDistSq x / 4)⁻¹ ^ 2

Explicit |x|⁻⁴-scale anisotropic majorant for every Hessian entry of the local Bessel contribution.