Singular-kernel toolkit on the torus (paper §5.1, blueprint node I-singconv)

Paper: I-singconv — (5.3)–(5.4) — the chain-convolution toolkit

The abstract integrability/convolution machinery behind the paper's (5.3)–(5.4) chain reductions, stated for the model kernel |z|⁻² on 𝕋⁴ (invSqKer). Contents:

• torusDistSq z = ∑ i (z̃ i)², the squared Euclidean length of the canonical lift z̃ = torusLift z ∈ [-π,π)⁴, and the bridge torusDistSq_eq_sum_norm_sq identifying it with ∑ i ‖z i‖² for the quotient norm on AddCircle (2π) — the canonical representative of a point of ℝ/2πℤ has absolute value ≤ π, hence realizes the norm;
• invSqKer z = (torusDistSq z)⁻¹, junk-totalized per DESIGN §5.7: at z = 0 the value is 0⁻¹ = 0 (mathlib's junk value), and all estimates below are one-sided bounds unaffected by this branch;
• the measure dictionary paperMeasure_eq_volume : paperMeasure = volume (the pi MeasureSpace structure on 𝕋⁴ built from mathlib's AddCircle volume, which is Haar of total mass 2π per coordinate);
• the crux integrability integrable_invSqKer (|z|⁻² is integrable in dimension 4 > 2), proved by transporting to the cube (-π,π]⁴ along AddCircle.measurePreserving_mk (componentwise, via measurePreserving_pi) and applying MeasureTheory.integrableOn_ball_of_norm_le_rpow on ℝ⁴;
• translation invariance integrable_invSqKer_sub.

Stage 2 (ball, annulus, triple-convolution bounds) builds on the same cube transport.

The model kernel

noncomputable def Anderson4D.torusDistSq (z : T4) : ℝ

Squared Euclidean distance of z ∈ 𝕋⁴ to 0, computed on the canonical componentwise lift to [-π, π)⁴.

Equations

• Anderson4D.torusDistSq z = ∑ i : Fin Anderson4D.dim, Anderson4D.torusLift z i ^ 2

noncomputable def Anderson4D.invSqKer (z : T4) : ℝ

The model singular kernel |z|⁻² on the torus. Junk-totalized: the value at z = 0 is 0⁻¹ = 0.

Equations

• Anderson4D.invSqKer z = (Anderson4D.torusDistSq z)⁻¹

The lift and the AddCircle norm

theorem Anderson4D.torusLift_mem_Ico (z : T4) (i : Fin dim) : torusLift z i ∈ Set.Ico (-Real.pi) Real.pi

The canonical lift lies in [-π, π) in each coordinate.

theorem Anderson4D.norm_eq_abs_torusLift (z : T4) (i : Fin dim) : ‖z i‖ = |torusLift z i|

The canonical representative realizes the quotient norm on ℝ/2πℤ: ‖z i‖ = |torusLift z i| (its absolute value is ≤ π, half the period).

theorem Anderson4D.torusDistSq_eq_sum_norm_sq (z : T4) : torusDistSq z = ∑ i : Fin dim, ‖z i‖ ^ 2

torusDistSq as a sum of squared AddCircle norms; the geometric workhorse (symmetry, triangle-type estimates come from norm axioms).

theorem Anderson4D.torusDistSq_nonneg (z : T4) : 0 ≤ torusDistSq z

theorem Anderson4D.torusDistSq_le (z : T4) : torusDistSq z ≤ 4 * Real.pi ^ 2

The torus has finite extent: torusDistSq ≤ 4π².

theorem Anderson4D.torusDistSq_eq_zero_iff (z : T4) : torusDistSq z = 0 ↔ z = 0

theorem Anderson4D.torusDistSq_neg (z : T4) : torusDistSq (-z) = torusDistSq z

Symmetry of the kernel geometry (via norms — note the lift itself is not odd on the boundary, but its absolute value is even).

theorem Anderson4D.invSqKer_nonneg (z : T4) : 0 ≤ invSqKer z

theorem Anderson4D.invSqKer_neg (z : T4) : invSqKer (-z) = invSqKer z

theorem Anderson4D.invSqKer_sub_comm (x y : T4) : invSqKer (x - y) = invSqKer (y - x)

The kernel is symmetric in the difference variable.

Measurability

theorem Anderson4D.measurable_torusLift : Measurable torusLift

theorem Anderson4D.measurable_torusDistSq : Measurable torusDistSq

theorem Anderson4D.measurable_invSqKer : Measurable invSqKer

The measure dictionary: paperMeasure is the pi volume

theorem Anderson4D.paperMeasure_eq_volume : paperMeasure = MeasureTheory.volume

The normalization-ledger identity: the paper's reference measure on 𝕋⁴ is mathlib's pi volume (per coordinate, AddCircle volume is Haar of total mass 2π).

Transport to the cube (-π, π]⁴

Integrability of the model kernel (the crux: 2 < 4 = dim)

theorem Anderson4D.integrable_invSqKer : MeasureTheory.Integrable invSqKer paperMeasure

Integrability of the model kernel |z|⁻² on 𝕋⁴ (blueprint I-singconv; the dimension count is 2 < 4).

Translation invariance

theorem Anderson4D.measurePreserving_sub_paper (w : T4) : MeasureTheory.MeasurePreserving (fun (z : T4) => z - w) paperMeasure paperMeasure

Translation invariance of the reference measure, packaged for the kernel-shift arguments of §5.1.

theorem Anderson4D.integrable_invSqKer_sub (w : T4) : MeasureTheory.Integrable (fun (z : T4) => invSqKer (z - w)) paperMeasure

Shifted kernels z ↦ |z - w|⁻² are integrable (uniformly in the shift, by translation invariance of Haar measure).

Stage 2: comparison of torusDistSq with the sup norm on 𝕋⁴

T4 carries the pi (sup) norm built from the AddCircle quotient norm; torusDistSq is squeezed between ‖z‖² and 4‖z‖², and the sup norm has an honest triangle inequality — all region arguments below use it.

theorem Anderson4D.sq_norm_le_torusDistSq (z : T4) : ‖z‖ ^ 2 ≤ torusDistSq z

theorem Anderson4D.torusDistSq_le_four_mul_sq_norm (z : T4) : torusDistSq z ≤ 4 * ‖z‖ ^ 2

Stage 2: radial computations on the cube

Stage 2: transporting integral bounds to the torus

instance Anderson4D.instIsFiniteMeasureT4PaperMeasure : MeasureTheory.IsFiniteMeasure paperMeasure

Stage 2 (a): the ball bound

theorem Anderson4D.setIntegral_invSqKer_ball_le : ∃ (C : ℝ), 0 < C ∧ ∀ (r : ℝ), 0 < r → ∫ (z : T4) in {z : T4 | torusDistSq z ≤ r ^ 2}, invSqKer z ∂paperMeasure ≤ C * r ^ 2

Ball bound (paper §5.1 machinery): the model kernel integrates to O(r²) over balls of radius r, uniformly.

Stage 2 (b): the annulus bound

theorem Anderson4D.setIntegral_invSqKer_sq_annulus_le : ∃ (C : ℝ), 0 < C ∧ ∀ (r : ℝ), 0 < r → r ≤ 1 → ∫ (z : T4) in {z : T4 | r ^ 2 ≤ torusDistSq z}, invSqKer z ^ 2 ∂paperMeasure ≤ C * (1 + |Real.log r|)

Annulus bound ((4.11)-adjacent): the square of the model kernel — critical in d = 4 — integrates to O(1 + |log r|) outside a ball of radius r ≤ 1.

Stage 2 (c): auxiliary kernel family d(z)^{-b}

Stage 2 (c): a.e. positivity of the distance

Stage 2 (c): pointwise region estimates

Stage 2 (c): the convolution bounds

theorem Anderson4D.integrable_invSqKer_sub_mul_invSqKer_of_ne {z₁ : T4} (hz₁ : z₁ ≠ 0) : MeasureTheory.Integrable (fun (z₂ : T4) => invSqKer (z₁ - z₂) * invSqKer z₂) paperMeasure

A binary inverse-square convolution is genuinely integrable away from the coincident-endpoint diagonal. This is the fixed-endpoint counterpart of the joint Green-path integrability theorem; the restriction is sharp in dimension four.

theorem Anderson4D.integrable_invSqKer_two_center_of_ne {x y : T4} (hxy : x ≠ y) : MeasureTheory.Integrable (fun (z : T4) => invSqKer (x - z) * invSqKer (z - y)) paperMeasure

Translation-invariant two-centre form of integrable_invSqKer_sub_mul_invSqKer_of_ne.

theorem Anderson4D.binary_conv_invSqKer_le : ∃ (C : ℝ), 0 < C ∧ ∀ (x : T4), x ≠ 0 → ∫ (z : T4), invSqKer (x - z) * invSqKer z ∂paperMeasure ≤ C * invSqKer x

A binary inverse-square convolution preserves the off-diagonal inverse-square majorant. The deliberately coarse power d⁻¹/⁴ in inner_bound is still dominated by 1 + d⁻¹; compactness of the torus then absorbs the constant term into d⁻¹.

theorem Anderson4D.binary_conv_invSqKer_log_le : ∃ (C : ℝ), 0 < C ∧ ∀ (x : T4), x ≠ 0 → ∫ (z : T4), invSqKer (x - z) * invSqKer z ∂paperMeasure ≤ C * (1 + |Real.log ‖x‖|)

The binary inverse-square convolution has its sharp critical logarithmic singularity. Unlike the deliberately coarse public binary_conv_invSqKer_le, this form retains the logarithm needed when the convolution is averaged against an ε-scale inserted kernel.

theorem Anderson4D.triple_conv_invSqKer_le : ∃ (C : ℝ), 0 < C ∧ ∀ (x : T4), ∫ (z₁ : T4), ∫ (z₂ : T4), invSqKer (x - z₁) * invSqKer (z₁ - z₂) * invSqKer z₂ ∂paperMeasure ∂paperMeasure ≤ C

Triple convolution bound (paper (5.3)–(5.4) machinery): the threefold convolution of the model kernel |·|⁻² on 𝕋⁴ is uniformly bounded — the exponent count 3·(−2) + 2·4 = 2 > 0 is strictly subcritical, unlike the binary (log-critical) convolution.

Stage 3: the regularized cubic singularity

The second summand in the primitive-kernel majorant is (torusDistSq z + ε²)⁻³. Its four-dimensional integral has the subcritical scale ε⁻². The proof below keeps the dimensional scaling explicit: transport to the fundamental cube, dominate by the corresponding integral on ℝ⁴, and rescale.

noncomputable def Anderson4D.regularizedInvCube (ε : ℝ) (z : T4) : ℝ

The regularized cubic singularity used in the primitive-kernel majorant.

Equations

• Anderson4D.regularizedInvCube ε z = (Anderson4D.torusDistSq z + ε ^ 2)⁻¹ ^ 3

theorem Anderson4D.regularizedInvCube_nonneg (ε : ℝ) (z : T4) : 0 ≤ regularizedInvCube ε z

theorem Anderson4D.measurable_regularizedInvCube (ε : ℝ) : Measurable (regularizedInvCube ε)

theorem Anderson4D.integrable_regularizedInvCube (ε : ℝ) (hε : 0 < ε) : MeasureTheory.Integrable (regularizedInvCube ε) paperMeasure

The regularized cubic singularity is integrable at every positive scale. This is recorded separately from its quantitative bound so that later integral algebra never relies on the Bochner integral's junk value.

theorem Anderson4D.integral_regularizedInvCube_le : ∃ (C : ℝ), 0 < C ∧ ∀ (ε : ℝ), 0 < ε → ∫ (z : T4), regularizedInvCube ε z ∂paperMeasure ≤ C * ε⁻¹ ^ 2

Regularized cubic integral bound (the second term in the R-3.22 primitive majorant): in four dimensions its integral is O(ε⁻²).