Step1

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Step 1 of the annular decomposition: the lattice cover and the centre term

ABK26, Section 4.1, e.mathcalE.annular.decomp.pre. Step 1 turns a full-grid weighted scale sum into an annular double sum. Its two ingredients are

2. the centre-term resummation: the centre z = 0 contributes J(□_n), which is pushed back into the annular shape by subadditivity plus the geometric factor sum_{n=k+1}^{m} 3^(-2s(m-n) - d(n-1-k)) <=^(-2s(m-k)).

This module proves both, plus the comparison of the diagonal slice of the annular double sum with the double sum itself, and assembles them into Resum.IsAnnularDecompPre.

The honest range

The manuscript prints the claim for s in (0, d/2] and its proof writes Since s <= 1/2. Nothing is lost for the Section 4.1 caller, which uses s <= 1/2 and d >= 2.

The two interchanges

The manuscript performs two order-of-summation interchanges. The cover interchange is carried here as the named slot hcov of annularDecompPre_of; the centre interchange is carried as the slot hcen, whose constant is the geometric factor 3^{2s}(1 - 3^{2s-d})^{-1}.

Part A -- the lattice annular cover

theorem Algsuperdiff.Section4.Provider.Annular.openCubeSet_originCube_subset {d : ℕ} {k l : ℤ} (hkl : k ≤ l) : HCPolySupport.openCubeSet (HCPolySupport.originCube d k) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d l)

The origin cubes are nested in the scale.

theorem Algsuperdiff.Section4.Provider.Annular.triadicLatticePoint_notMem_openCubeSet {d : ℕ} {n : ℤ} {v : Fin d → ℤ} (hv : v ≠ 0) : Support.triadicLatticePoint n v ∉ HCPolySupport.openCubeSet (HCPolySupport.originCube d n)

A nonzero scale-n lattice point is outside □_n. Its nonzero coordinate has absolute value at least 3^n, while □_n only reaches 3^n / 2.

theorem Algsuperdiff.Section4.Provider.Annular.exists_mem_latticeAnnulusSet {d : ℕ} {n m : ℤ} {v : Fin d → ℤ} (hv : v ≠ 0) (hmem : v ∈ Support.latticeCubeSet d n m) : ∃ (j : ℤ), n + 1 ≤ j ∧ j ≤ m ∧ v ∈ Support.latticeAnnulusSet d n j (j - 1)

The lattice annular cover.

Every nonzero scale-n lattice point of □_m lies in exactly one triadic annulus □_j ∖ □_{j-1} with n + 1 <= j <= m, namely the one indexed by the least j with the point in □_j.

theorem Algsuperdiff.Section4.Provider.Annular.zero_mem_latticeCubeSet {d : ℕ} (n m : ℤ) : 0 ∈ Support.latticeCubeSet d n m

The centre 0 of the scale-n lattice is in □_m for every n <= m (indeed for every m): the manuscript's {0} component of the cover.

Part C -- the diagonal slice of the annular double sum

theorem Algsuperdiff.Section4.Provider.Annular.tsum_diag_le_annDouble {m : ℤ} {h : ℤ → ℤ → ℝ} (hh0 : ∀ (j n : ℤ), 0 ≤ h j n) (hsum : Summable (annFam m h)) : ∑' (u : ℕ), h (m - ↑u) (m - ↑u - 1) ≤ annDouble m h

The diagonal slice of the annular double sum.

The pairs (j, j-1) -- the innermost annulus at each scale -- form the i = 0 slice of the N x N parametrization, so their weighted sum is at most the whole annular double sum. This is what receives the resummed centre term (: the relabelling k -> n, k+1 -> j proves at n = j - 1).

Part D -- the Step-1 assembly

theorem Algsuperdiff.Section4.Provider.Annular.annularDecompPre_of {s Ccov Ccen C : ℝ} {m : ℤ} {Jgrid Jcen Jcov : ℤ → ℝ} {Jann : ℤ → ℤ → ℝ} (hJann0 : ∀ (j n : ℤ), 0 ≤ Jann j n) (hCcen : 0 ≤ Ccen) (hsum : Summable (annFam m fun (j n : ℤ) => 3 ^ (-(2 * s * ↑(m - n))) * Jann j n)) (hgrid : ∀ n ≤ m, Jgrid n ≤ Jcov n + Jcen n) (hcov : (∑' (n : ℤ), if n ≤ m then 3 ^ (-(2 * s * ↑(m - n))) * Jcov n else 0) ≤ Ccov * annDouble m fun (j n : ℤ) => 3 ^ (-(2 * s * ↑(m - n))) * Jann j n) (hcen : (∑' (n : ℤ), if n ≤ m then 3 ^ (-(2 * s * ↑(m - n))) * Jcen n else 0) ≤ Ccen * ∑' (u : ℕ), 3 ^ (-(2 * s * ↑(m - (m - ↑u - 1)))) * Jann (m - ↑u) (m - ↑u - 1)) (hsplit : Summable fun (n : ℤ) => if n ≤ m then 3 ^ (-(2 * s * ↑(m - n))) * Jcov n else 0) (hsplit2 : Summable fun (n : ℤ) => if n ≤ m then 3 ^ (-(2 * s * ↑(m - n))) * Jcen n else 0) (hJgrid0 : ∀ (n : ℤ), 0 ≤ Jgrid n) (hC : Ccov + Ccen ≤ C) : IsAnnularDecompPre s m Jgrid Jann C

The Step-1 assembly.

The manuscript's proof splits the full-grid weighted scale sum into the annular-cover part and the centre part, bounds the first by the annular double sum (the cover interchange, hcov) and pushes the second back into the diagonal of the same double sum (the subadditivity iteration, hcen). The output is Resum.IsAnnularDecompPre, the shape Resum.preZero_of_pre_and_ugly consumes.

Both slots are conditional A obligations on the caller: hcov is the cover interchange and hcen the resummed centre term.