The smooth nonzero-lattice remainder of the torus Green kernel

On the open principal cube, the periodized heat kernel is the Euclidean zero-lattice summand plus a uniformly smooth sum over nonzero lattice translates. This file establishes the absolute summability needed to differentiate that remainder twice.

@[reducible, inline]

abbrev Anderson4D.NZ4 : Type

Nonzero lattice points.

Equations

• Anderson4D.NZ4 = { k : Anderson4D.Z4 // k ≠ 0 }

noncomputable def Anderson4D.latticeTranslate (x : R4) (k : Z4) : R4

Translation of a Euclidean lift by the period indexed by k.

Equations

• Anderson4D.latticeTranslate x k i = x i + 2 * Real.pi * ↑(k i)

noncomputable def Anderson4D.latticeBesselTerm (x : R4) (k : Z4) : ℝ

The k-th Euclidean Bessel summand of the periodized Green kernel.

Equations

• Anderson4D.latticeBesselTerm x k = Anderson4D.euclideanBessel4 (Anderson4D.latticeTranslate x k)

noncomputable def Anderson4D.latticeBesselGrad (x : R4) (k : Z4) (i : Fin dim) : ℝ

First-coordinate derivative of a lattice Bessel summand.

Equations

• Anderson4D.latticeBesselGrad x k i = Anderson4D.euclideanBesselGrad (Anderson4D.latticeTranslate x k) i

noncomputable def Anderson4D.latticeBesselHess (x : R4) (k : Z4) (i j : Fin dim) : ℝ

Coordinate Hessian entry of a lattice Bessel summand.

Equations

• Anderson4D.latticeBesselHess x k i j = Anderson4D.euclideanBesselHess (Anderson4D.latticeTranslate x k) i j

def Anderson4D.latticeL1 (k : Z4) : ℕ

Sum of absolute integer coordinates.

Equations

• Anderson4D.latticeL1 k = ∑ i : Fin Anderson4D.dim, (k i).natAbs

def Anderson4D.latticeSq (k : Z4) : ℝ

Squared Euclidean lattice length.

Equations

• Anderson4D.latticeSq k = ∑ i : Fin Anderson4D.dim, ↑(k i) ^ 2

noncomputable def Anderson4D.latticeGeomWeight (k : Z4) : ℝ

Product-geometric lattice majorant. Its square polynomial factor absorbs all numerators appearing through the Hessian.

Equations

• Anderson4D.latticeGeomWeight k = ∏ i : Fin Anderson4D.dim, (↑(k i).natAbs + 1) ^ 2 * Real.exp (-(1 / 2)) ^ (k i).natAbs

theorem Anderson4D.summable_latticeGeomWeight : Summable latticeGeomWeight

def Anderson4D.InClosedPrincipalCube (x : R4) : Prop

Closed principal cube, used for uniform lattice estimates.

Equations

• Anderson4D.InClosedPrincipalCube x = ∀ (i : Fin Anderson4D.dim), |x i| ≤ Real.pi

def Anderson4D.InOpenPrincipalCube (x : R4) : Prop

Open principal cube, where the quotient lift is locally smooth.

Equations

• Anderson4D.InOpenPrincipalCube x = ∀ (i : Fin Anderson4D.dim), |x i| < Real.pi

theorem Anderson4D.latticeTranslate_sq_lower {x : R4} (hx : InClosedPrincipalCube x) (k : Z4) : Real.pi ^ 2 * ∑ i : Fin dim, ↑(k i) ^ 2 ≤ euclideanDistSq (latticeTranslate x k)

theorem Anderson4D.one_le_lattice_sq {k : Z4} (hk : k ≠ 0) : 1 ≤ latticeSq k

noncomputable def Anderson4D.latticeTimeScale (k : Z4) : ℝ

Time scale furnished by a nonzero lattice translate.

Equations

• Anderson4D.latticeTimeScale k = Real.pi ^ 2 * Anderson4D.latticeSq k / 8

theorem Anderson4D.abs_latticeBesselTerm_le {x : R4} (hx : InClosedPrincipalCube x) {k : Z4} (hk : k ≠ 0) : |latticeBesselTerm x k| ≤ latticeGeomWeight k

A nonzero Bessel summand is controlled by the common geometric lattice majorant, uniformly on the closed principal cube.

theorem Anderson4D.abs_latticeBesselGrad_le {x : R4} (hx : InClosedPrincipalCube x) {k : Z4} (hk : k ≠ 0) (i : Fin dim) : |latticeBesselGrad x k i| ≤ latticeGeomWeight k

The first derivative of a nonzero Bessel summand has the same uniform geometric lattice majorant.

theorem Anderson4D.abs_latticeBesselHess_le {x : R4} (hx : InClosedPrincipalCube x) {k : Z4} (hk : k ≠ 0) (i j : Fin dim) : |latticeBesselHess x k i j| ≤ 2 * latticeGeomWeight k

The Hessian of a nonzero Bessel summand is uniformly dominated by twice the common geometric lattice weight.

theorem Anderson4D.summable_nz_latticeGeomWeight : Summable fun (k : NZ4) => latticeGeomWeight ↑k

theorem Anderson4D.summable_latticeBesselTerm {x : R4} (hx : InClosedPrincipalCube x) : Summable fun (k : NZ4) => latticeBesselTerm x ↑k

theorem Anderson4D.summable_latticeBesselGrad {x : R4} (hx : InClosedPrincipalCube x) (i : Fin dim) : Summable fun (k : NZ4) => latticeBesselGrad x (↑k) i

theorem Anderson4D.summable_latticeBesselHess {x : R4} (hx : InClosedPrincipalCube x) (i j : Fin dim) : Summable fun (k : NZ4) => latticeBesselHess x (↑k) i j

def Anderson4D.coordPrincipalInterval (x : R4) (i : Fin dim) : Set ℝ

Scalar shifts that keep the selected coordinate inside the open principal interval.

Equations

• Anderson4D.coordPrincipalInterval x i = Set.Ioo (-Real.pi - x i) (Real.pi - x i)

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

The actual nonzero-lattice part of the periodized Bessel kernel.

Equations

• Anderson4D.nonzeroLatticeRemainder x = ∑' (k : Anderson4D.NZ4), Anderson4D.latticeBesselTerm x ↑k

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

Coordinate derivative series of the nonzero-lattice remainder.

Equations

• Anderson4D.nonzeroLatticeRemainderGrad x i = ∑' (k : Anderson4D.NZ4), Anderson4D.latticeBesselGrad x (↑k) i

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

Coordinate Hessian series of the nonzero-lattice remainder.

Equations

• Anderson4D.nonzeroLatticeRemainderHess x i j = ∑' (k : Anderson4D.NZ4), Anderson4D.latticeBesselHess x (↑k) i j

noncomputable def Anderson4D.nonzeroLatticeRemainderBound : ℝ

A global finite constant controlling the nonzero-lattice remainder and its first two coordinate derivatives on the principal cube.

Equations

• Anderson4D.nonzeroLatticeRemainderBound = ∑' (k : Anderson4D.NZ4), Anderson4D.latticeGeomWeight ↑k

theorem Anderson4D.hasDerivAt_nonzeroLatticeRemainder_coord_at {x : R4} (hx : InOpenPrincipalCube x) (i : Fin dim) {s : ℝ} (hs : s ∈ coordPrincipalInterval x i) : HasDerivAt (fun (r : ℝ) => nonzeroLatticeRemainder (coordLine x i r)) (nonzeroLatticeRemainderGrad (coordLine x i s) i) s

The nonzero-lattice series can be differentiated termwise on every coordinate interval contained in the open principal cube.

theorem Anderson4D.hasDerivAt_nonzeroLatticeRemainderGrad_coord_at {x : R4} (hx : InOpenPrincipalCube x) (i j : Fin dim) {s : ℝ} (hs : s ∈ coordPrincipalInterval x j) : HasDerivAt (fun (r : ℝ) => nonzeroLatticeRemainderGrad (coordLine x j r) i) (nonzeroLatticeRemainderHess (coordLine x j s) i j) s

The first-derivative series is differentiable termwise, with Hessian given by the absolutely convergent second-derivative series.

theorem Anderson4D.hasDerivAt_nonzeroLatticeRemainder_coord {x : R4} (hx : InOpenPrincipalCube x) (i : Fin dim) : HasDerivAt (fun (r : ℝ) => nonzeroLatticeRemainder (coordLine x i r)) (nonzeroLatticeRemainderGrad x i) 0

theorem Anderson4D.hasDerivAt_nonzeroLatticeRemainderGrad_coord {x : R4} (hx : InOpenPrincipalCube x) (i j : Fin dim) : HasDerivAt (fun (r : ℝ) => nonzeroLatticeRemainderGrad (coordLine x j r) i) (nonzeroLatticeRemainderHess x i j) 0

theorem Anderson4D.nonzeroLatticeRemainderBound_nonneg : 0 ≤ nonzeroLatticeRemainderBound

theorem Anderson4D.abs_nonzeroLatticeRemainder_le {x : R4} (hx : InClosedPrincipalCube x) : |nonzeroLatticeRemainder x| ≤ nonzeroLatticeRemainderBound

theorem Anderson4D.abs_nonzeroLatticeRemainderGrad_le {x : R4} (hx : InClosedPrincipalCube x) (i : Fin dim) : |nonzeroLatticeRemainderGrad x i| ≤ nonzeroLatticeRemainderBound

theorem Anderson4D.abs_nonzeroLatticeRemainderHess_le {x : R4} (hx : InClosedPrincipalCube x) (i j : Fin dim) : |nonzeroLatticeRemainderHess x i j| ≤ 2 * nonzeroLatticeRemainderBound

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

theorem Anderson4D.greenLocalLift_eq_bessel_add_nonzeroRemainder {x : R4} (hx : ∀ (i : Fin dim), x i ∈ Set.Ico (-Real.pi) Real.pi) (hx0 : euclideanDistSq x ≠ 0) : greenLocalLift x = euclideanBessel4 x + nonzeroLatticeRemainder x

On the principal cell away from its singular point, the heat-kernel definition of the torus Green function is exactly the zero Euclidean Bessel term plus the absolutely convergent nonzero-lattice remainder.

theorem Anderson4D.greenLocalRemainder_eq_nonzeroLatticeRemainder {x : R4} (hx : ∀ (i : Fin dim), x i ∈ Set.Ico (-Real.pi) Real.pi) (hx0 : euclideanDistSq x ≠ 0) : greenLocalRemainder x = nonzeroLatticeRemainder x

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

Actual first-coordinate derivative of the regular part of the local Green kernel.

Equations

• Anderson4D.greenLocalRemainderGrad x i = Anderson4D.nonzeroLatticeRemainderGrad x i

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

Actual coordinate Hessian entry of the regular part.

Equations

• Anderson4D.greenLocalRemainderHess x i j = Anderson4D.nonzeroLatticeRemainderHess x i j

theorem Anderson4D.hasDerivAt_greenLocalRemainder_coord {x : R4} (hx : InOpenPrincipalCube x) (hx0 : euclideanDistSq x ≠ 0) (i : Fin dim) : HasDerivAt (fun (s : ℝ) => greenLocalRemainder (coordLine x i s)) (greenLocalRemainderGrad x i) 0

theorem Anderson4D.hasDerivAt_greenLocalRemainderGrad_coord {x : R4} (hx : InOpenPrincipalCube x) (i j : Fin dim) : HasDerivAt (fun (s : ℝ) => greenLocalRemainderGrad (coordLine x j s) i) (greenLocalRemainderHess x i j) 0

theorem Anderson4D.abs_greenLocalRemainder_le {x : R4} (hx : ∀ (i : Fin dim), x i ∈ Set.Ico (-Real.pi) Real.pi) (hx0 : euclideanDistSq x ≠ 0) : |greenLocalRemainder x| ≤ nonzeroLatticeRemainderBound

theorem Anderson4D.abs_greenLocalRemainderGrad_le {x : R4} (hx : InClosedPrincipalCube x) (i : Fin dim) : |greenLocalRemainderGrad x i| ≤ nonzeroLatticeRemainderBound

theorem Anderson4D.abs_greenLocalRemainderHess_le {x : R4} (hx : InClosedPrincipalCube x) (i j : Fin dim) : |greenLocalRemainderHess x i j| ≤ 2 * nonzeroLatticeRemainderBound

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

Coordinate gradient entry of the full local Green kernel.

Equations

• Anderson4D.greenLocalGrad x i = Anderson4D.euclideanBesselGrad x i + Anderson4D.greenLocalRemainderGrad x i

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

Coordinate Hessian entry of the full local Green kernel.

Equations

• Anderson4D.greenLocalHess x i j = Anderson4D.euclideanBesselHess x i j + Anderson4D.greenLocalRemainderHess x i j

theorem Anderson4D.hasDerivAt_greenLocalLift_coord {x : R4} (hx : InOpenPrincipalCube x) (hx0 : euclideanDistSq x ≠ 0) (i : Fin dim) : HasDerivAt (fun (s : ℝ) => greenLocalLift (coordLine x i s)) (greenLocalGrad x i) 0

theorem Anderson4D.hasDerivAt_greenLocalGrad_coord {x : R4} (hx : InOpenPrincipalCube x) (hx0 : euclideanDistSq x ≠ 0) (i j : Fin dim) : HasDerivAt (fun (s : ℝ) => greenLocalGrad (coordLine x j s) i) (greenLocalHess x i j) 0

theorem Anderson4D.abs_euclideanBessel4_le_laplaceFundamental4 {x : R4} (hx : euclideanDistSq x ≠ 0) : |euclideanBessel4 x| ≤ laplaceFundamental4 x

theorem Anderson4D.abs_greenLocalLift_le {x : R4} (hx : ∀ (i : Fin dim), x i ∈ Set.Ico (-Real.pi) Real.pi) (hx0 : euclideanDistSq x ≠ 0) : |greenLocalLift x| ≤ laplaceFundamental4 x + nonzeroLatticeRemainderBound

Zeroth-order singular estimate for the actual local Green kernel, with the bounded periodization remainder kept explicit.

theorem Anderson4D.abs_greenLocalGrad_le {x : R4} (hx : InClosedPrincipalCube x) (hx0 : euclideanDistSq x ≠ 0) (i : Fin dim) : |greenLocalGrad x i| ≤ |x i| / (2 * Real.pi ^ 2) * (euclideanDistSq x)⁻¹ ^ 2 + nonzeroLatticeRemainderBound

First-order |x|⁻³-scale singular estimate, plus the global smooth periodization constant.

theorem Anderson4D.abs_greenLocalHess_le {x : R4} (hx : InClosedPrincipalCube x) (hx0 : euclideanDistSq x ≠ 0) (i j : Fin dim) : |greenLocalHess 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 + 2 * nonzeroLatticeRemainderBound

Second-order |x|⁻⁴-scale singular estimate, plus the global smooth periodization constant.

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

The Euclidean part left after subtracting the exact four-dimensional Laplace singularity.

Equations

• Anderson4D.euclideanBesselLaplaceRemainder x = Anderson4D.euclideanBessel4 x - Anderson4D.laplaceFundamental4 x

theorem Anderson4D.euclideanBesselLaplaceRemainder_eq_integral {x : R4} (hx : euclideanDistSq x ≠ 0) : euclideanBesselLaplaceRemainder x = ∫ (t : ℝ) in Set.Ioi 0, (Real.exp (-t) - 1) * euclideanHeatKernel4 t x

theorem Anderson4D.abs_euclideanBesselLaplaceRemainder_le {x : R4} (hx : euclideanDistSq x ≠ 0) : |euclideanBesselLaplaceRemainder x| ≤ (16 * Real.pi ^ 2)⁻¹ * (2 * (√(euclideanDistSq x / 4))⁻¹ + 1)

Improved |x|⁻¹-scale estimate for the Euclidean Bessel kernel after subtracting its exact Laplace singularity. The right-hand side is kept in the natural heat-time scale a = |x|²/4.

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

Full near-diagonal remainder from paper (4.1), in principal coordinates.

Equations

• Anderson4D.greenLocalImprovedRemainder x = Anderson4D.greenLocalLift x - Anderson4D.laplaceFundamental4 x

theorem Anderson4D.greenLocalImprovedRemainder_decomposition {x : R4} (hx : ∀ (i : Fin dim), x i ∈ Set.Ico (-Real.pi) Real.pi) (hx0 : euclideanDistSq x ≠ 0) : greenLocalImprovedRemainder x = euclideanBesselLaplaceRemainder x + nonzeroLatticeRemainder x

theorem Anderson4D.abs_greenLocalImprovedRemainder_raw_le {x : R4} (hx : ∀ (i : Fin dim), x i ∈ Set.Ico (-Real.pi) Real.pi) (hx0 : euclideanDistSq x ≠ 0) : |greenLocalImprovedRemainder x| ≤ (16 * Real.pi ^ 2)⁻¹ * (2 * (√(euclideanDistSq x / 4))⁻¹ + 1) + nonzeroLatticeRemainderBound

noncomputable def Anderson4D.greenLocalImprovedBound : ℝ

Explicit global coefficient for the |x|⁻¹ improved bound on the principal cube.

Equations

• Anderson4D.greenLocalImprovedBound = 4 * (16 * Real.pi ^ 2)⁻¹ + 2 * Real.pi * ((16 * Real.pi ^ 2)⁻¹ + Anderson4D.nonzeroLatticeRemainderBound)

theorem Anderson4D.greenLocalImprovedBound_pos : 0 < greenLocalImprovedBound

theorem Anderson4D.abs_greenLocalImprovedRemainder_le {x : R4} (hx : ∀ (i : Fin dim), x i ∈ Set.Ico (-Real.pi) Real.pi) (hx0 : euclideanDistSq x ≠ 0) : |greenLocalImprovedRemainder x| ≤ greenLocalImprovedBound * (√(euclideanDistSq x))⁻¹

Paper (4.1), improved zeroth-order near-diagonal estimate: G(x) - (4π²|x|²)⁻¹ = O(|x|⁻¹).

noncomputable def Anderson4D.greenLocalValueSingularBound : ℝ

Explicit constants for the three singular estimates in paper (4.1), for coordinate derivatives of order 0, 1, and 2.

Equations

• Anderson4D.greenLocalValueSingularBound = (4 * Real.pi ^ 2)⁻¹ + 4 * Real.pi ^ 2 * Anderson4D.nonzeroLatticeRemainderBound

noncomputable def Anderson4D.greenLocalGradSingularBound : ℝ

Equations

• Anderson4D.greenLocalGradSingularBound = (2 * Real.pi ^ 2)⁻¹ + (2 * Real.pi) ^ 3 * Anderson4D.nonzeroLatticeRemainderBound

noncomputable def Anderson4D.greenLocalHessSingularBound : ℝ

Equations

• Anderson4D.greenLocalHessSingularBound = 5 / (2 * Real.pi ^ 2) + 2 * (2 * Real.pi) ^ 4 * Anderson4D.nonzeroLatticeRemainderBound

theorem Anderson4D.abs_greenLocalLift_singular {x : R4} (hx : ∀ (i : Fin dim), x i ∈ Set.Ico (-Real.pi) Real.pi) (hx0 : euclideanDistSq x ≠ 0) : |greenLocalLift x| ≤ greenLocalValueSingularBound * (euclideanDistSq x)⁻¹

theorem Anderson4D.abs_greenLocalGrad_singular {x : R4} (hx : InClosedPrincipalCube x) (hx0 : euclideanDistSq x ≠ 0) (i : Fin dim) : |greenLocalGrad x i| ≤ greenLocalGradSingularBound * (√(euclideanDistSq x))⁻¹ ^ 3

theorem Anderson4D.abs_greenLocalHess_singular {x : R4} (hx : InClosedPrincipalCube x) (hx0 : euclideanDistSq x ≠ 0) (i j : Fin dim) : |greenLocalHess x i j| ≤ greenLocalHessSingularBound * (√(euclideanDistSq x))⁻¹ ^ 4