Iterated singular convolutions on the four-dimensional torus

This file packages the induction implicit in paper (5.4). The hard analytic input is the uniform threefold-convolution estimate proved in Continuum/SingularConv.lean. Every additional |z|⁻² factor costs only its finite L¹ mass, so all convolution chains of length at least three are uniformly bounded, with an exponential constant in the chain length.

This is the reusable chain form of blueprint node I-singconv. It is still only the translation-invariant analytic core of paper (5.3)--(5.4); the cell supports and rescaling factors belong to node R-51.

def Anderson4D.singularChain : ℕ → T4 → ℝ

The n-fold convolution chain of the model kernel |z|⁻².

The values at lengths 0 and 1 are totalized as 0 and invSqKer. For n ≥ 2, the recursion adds one kernel on the left.

Equations

• Anderson4D.singularChain 0 = fun (x : Anderson4D.T4) => 0
• Anderson4D.singularChain 1 = Anderson4D.invSqKer
• Anderson4D.singularChain n.succ.succ = fun (x : Anderson4D.T4) => ∫ (z : Anderson4D.T4), Anderson4D.invSqKer (x - z) * Anderson4D.singularChain (n + 1) z ∂Anderson4D.paperMeasure

theorem Anderson4D.singularChain_nonneg (n : ℕ) (x : T4) : 0 ≤ singularChain n x

Every convolution chain is pointwise nonnegative.

theorem Anderson4D.singularChain_three (x : T4) : singularChain 3 x = ∫ (z₁ : T4), ∫ (z₂ : T4), invSqKer (x - z₁) * invSqKer (z₁ - z₂) * invSqKer z₂ ∂paperMeasure ∂paperMeasure

The length-three chain is exactly the nested integral used by triple_conv_invSqKer_le.

noncomputable def Anderson4D.invSqKerMass : ℝ

The finite L¹ mass of the model singular kernel.

Equations

• Anderson4D.invSqKerMass = ∫ (z : Anderson4D.T4), Anderson4D.invSqKer z ∂Anderson4D.paperMeasure

theorem Anderson4D.invSqKerMass_nonneg : 0 ≤ invSqKerMass

theorem Anderson4D.integral_invSqKer_sub_left (x : T4) : ∫ (z : T4), invSqKer (x - z) ∂paperMeasure = invSqKerMass

Translation invariance of the L¹ mass, in the orientation used by singularChain.

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

The shifted kernel in the left-convolution orientation is integrable.

theorem Anderson4D.singularChain_le_pow : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), 3 ≤ n → ∀ (x : T4), singularChain n x ≤ C ^ n

Uniform chain bound (paper (5.4), analytic core).

There is one absolute constant C > 0 such that every convolution chain of length at least three is bounded by Cⁿ, uniformly in its endpoint. The base case is triple_conv_invSqKer_le; the induction uses only the finite L¹ mass of one additional kernel.