Step3Producers

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

The three Step-3 resummation producers

Local helpers for ABK26, Section 4.1, proof of Proposition p.mathcalE.annular.decomp, Step 3. The manuscript's Step 3 consists of three displays, each resumming one of the last three terms of e.mathcalE.annular.decomp.pre.zero:

The three are produced here at abstract nonnegative fields, in the shapes the Step-3 regrouping slots hgrad, hL2 and hsig consume. All the resummation arithmetic (the annulus multiplicity, the scale-weight collapses, the geometric constants) is discharged by Step3Arith. What is carried as an explicit caller hypothesis is exactly the manuscript's own structural input at each display: the triangle inequality over the layer sum k_b - k_a = sum_{l in (a,b]} j_l followed by Cauchy--Schwarz on the finite k-block and the per-k cube comparison (for the two shell displays), and the e.shom.m.vs.shom.n display (for the sigma-bar sum).

The two shell producers share one core

step3_shell_resummation is the shared statement: the (j,n)-content is the multiplicity (m-n+2) times a growth factor 3^(theta (m-n)) times the finite k-block sum of squared shell brackets; the output is 72 (s/2 - theta)^(-3) times the target geometric shell sum. The gradient display is theta = 0 (its 3^(2(1-gamma)(n-k)) <= 9 is absorbed into the caller's constant); the L^2 display is theta = 2 gamma, whose (s - 4 gamma)^(-3) is folded to s^(-3) by the proved sub_four_gamma_inv_cube_le.

The manuscript pulls the k-block out of the annular double sum by an interchange of summation. The route here does the same work without a Fubini step: the finite block is compared against the target sum's own geometric weight (shellBlock_le_zpow_mul_target), which costs the factor 3^(s(m-n+2)/2) and is exactly absorbed by the annular weight 3^(-s(m-n)), leaving the residual rate s/2 - theta.

The k-block index convention

The manuscript's inner block is k in [n-1, m]. Everything below writes it in the depth parametrization k = m - v, v in {0, ..., m-n+1}, i.e. as Finset.range ((m-n).toNat + 2) -- the same block, and the parametrization in which the target sum sum_v 3^(-s v/2) A(m-v)^2 is written.

The finite block against the target geometric shell sum

theorem Algsuperdiff.Section4.Provider.Annular.shellBlock_le_zpow_mul_target {s : ℝ} {m : ℤ} {A : ℤ → ℝ} (hs0 : 0 < s) (hsum : Summable fun (v : ℕ) => 3 ^ (-(s / 2) * ↑v) * A (m - ↑v) ^ 2) (N : ℕ) : ∑ v ∈ Finset.range N, A (m - ↑v) ^ 2 ≤ 3 ^ (s / 2 * ↑N) * ∑' (v : ℕ), 3 ^ (-(s / 2) * ↑v) * A (m - ↑v) ^ 2

The finite k-block is dominated by the target shell sum.

Every A(m-v)^2 with v < N is 3^(s v / 2) times the target's own term, and 3^(s v / 2) <= 3^(s N / 2). This is the step that lets the k-block be pulled out of the annular double sum with no interchange of summation.

The shared shell resummation

theorem Algsuperdiff.Section4.Provider.Annular.step3_shell_resummation {m : ℤ} {s theta Kcs : ℝ} {A : ℤ → ℝ} {T : ℤ → ℤ → ℝ} (hs0 : 0 < s) (hs1 : s ≤ 1) (htheta0 : 0 ≤ theta) (hc0 : 0 < s / 2 - theta) (hKcs : 0 ≤ Kcs) (hT0 : ∀ (j n : ℤ), 0 ≤ T j n) (hsum : Summable fun (v : ℕ) => 3 ^ (-(s / 2) * ↑v) * A (m - ↑v) ^ 2) (hcs : ∀ (j n : ℤ), j ≤ m → n ≤ j - 1 → T j n ≤ Kcs * (↑(m - n) + 2) * 3 ^ (theta * ↑(m - n)) * ∑ v ∈ Finset.range ((m - n).toNat + 2), A (m - ↑v) ^ 2) : (annDouble m fun (j n : ℤ) => 3 ^ (-(s * ↑(m - n))) * T j n) ≤ 72 * Kcs / (s / 2 - theta) ^ 3 * ∑' (v : ℕ), 3 ^ (-(s / 2) * ↑v) * A (m - ↑v) ^ 2

The shared Step-3 shell resummation.

If the annular (j,n)-content obeys

T j n <= Kcs (m - n + 2) 3^(theta (m-n)) sum_{v < (m-n)+2} A(m-v)^2 ,

then the annular double sum of 3^(-s(m-n)) T j n is at most 72 Kcs (s/2 - theta)^(-3) times the target shell sum sum_v 3^(-s v/2) A(m-v)^2.

Step 3: the gradient resummation

theorem Algsuperdiff.Section4.Provider.Annular.step3_grad_resummation {m : ℤ} {s Kcs : ℝ} {A : ℤ → ℝ} {T : ℤ → ℤ → ℝ} (hs0 : 0 < s) (hs1 : s ≤ 1) (hKcs : 0 ≤ Kcs) (hT0 : ∀ (j n : ℤ), 0 ≤ T j n) (hsum : Summable fun (v : ℕ) => 3 ^ (-(s / 2) * ↑v) * A (m - ↑v) ^ 2) (hcs : ∀ (j n : ℤ), j ≤ m → n ≤ j - 1 → T j n ≤ Kcs * (↑(m - n) + 2) * ∑ v ∈ Finset.range ((m - n).toNat + 2), A (m - ↑v) ^ 2) : (annDouble m fun (j n : ℤ) => 3 ^ (-(s * ↑(m - n))) * T j n) ≤ 576 * Kcs * (s ^ 3)⁻¹ * ∑' (v : ℕ), 3 ^ (-(s / 2) * ↑v) * A (m - ↑v) ^ 2

The gradient resummation.

The theta = 0 instance of the shared core: the caller's Kcs carries the manuscript's 3^(2(1-gamma)(n-k)) <= 9 cube comparison.

Step 3: the L^2 resummation

theorem Algsuperdiff.Section4.Provider.Annular.step3_kL2_resummation {m : ℤ} {s gamma Kcs : ℝ} {A : ℤ → ℝ} {T : ℤ → ℤ → ℝ} (hs0 : 0 < s) (hs1 : s ≤ 1) (hgamma0 : 0 ≤ gamma) (hsg : 8 * gamma ≤ s) (hKcs : 0 ≤ Kcs) (hT0 : ∀ (j n : ℤ), 0 ≤ T j n) (hsum : Summable fun (v : ℕ) => 3 ^ (-(s / 2) * ↑v) * A (m - ↑v) ^ 2) (hcs : ∀ (j n : ℤ), j ≤ m → n ≤ j - 1 → T j n ≤ Kcs * (↑(m - n) + 2) * 3 ^ (2 * gamma * ↑(m - n)) * ∑ v ∈ Finset.range ((m - n).toNat + 2), A (m - ↑v) ^ 2) : (annDouble m fun (j n : ℤ) => 3 ^ (-(s * ↑(m - n))) * T j n) ≤ 4608 * Kcs * (s ^ 3)⁻¹ * ∑' (v : ℕ), 3 ^ (-(s / 2) * ↑v) * A (m - ↑v) ^ 2

The L^2 resummation.

The theta = 2 gamma instance: the residual rate is (s - 4 gamma)/2, which is the origin of the manuscript's (s - 4 gamma)^(-3); the standing hypothesis s >= 8 gamma folds it into s^(-3) through the proved sub_four_gamma_inv_cube_le.

Step 3: the sigma-bar ratio sum

theorem Algsuperdiff.Section4.Provider.Annular.step3_sigma_ratio_core {m : ℤ} {s gamma K1 K0 : ℝ} {sig : ℤ → ℝ} (hs0 : 0 < s) (hs1 : s ≤ 1) (hgamma0 : 0 ≤ gamma) (hsg : 8 * gamma ≤ s) (hsig0 : ∀ (n : ℤ), 0 ≤ sig n) (hshom : ∀ n ≤ m - 1, sig n ≤ (K1 * ↑(m - n) + K0) ^ 2 * 3 ^ (2 * gamma * ↑(m - n))) : (annDouble m fun (x n : ℤ) => 3 ^ (-(s * ↑(m - n))) * sig n) ≤ 1024 * K1 ^ 2 / s ^ 4 + 16 * K0 ^ 2 / s ^ 2

The sigma-bar ratio sum, arithmetic core.

From the e.shom.m.vs.shom.n display in the form |sigma_m sigma_{n-2}^{-1} - 1|^2 <= (K1 (m-n) + K0)^2 3^(2 gamma (m-n)), the annular double sum is at most 1024 K1^2 s^(-4) + 16 K0^2 s^(-2).

theorem Algsuperdiff.Section4.Provider.Annular.step3_sigma_ratio_slot {m : ℤ} {s gamma cstar Cshom : ℝ} {sig : ℤ → ℝ} (hs0 : 0 < s) (hs1 : s ≤ 1) (hgamma0 : 0 ≤ gamma) (hsg : 8 * gamma ≤ s) (hcstar0 : 0 < cstar) (hcstar4 : cstar ^ 4 ≤ 6) (hlog : 1 ≤ |Real.log gamma|) (hsig0 : ∀ (n : ℤ), 0 ≤ sig n) (hshom : ∀ n ≤ m - 1, sig n ≤ (Cshom * gamma * ↑(m - n) + Cshom * (2 * gamma + (cstar ^ 2)⁻¹ * (gamma * |Real.log gamma| ^ 2))) ^ 2 * 3 ^ (2 * gamma * ↑(m - n))) : (annDouble m fun (x n : ℤ) => 3 ^ (-(s * ↑(m - n))) * sig n) ≤ 7000 * Cshom ^ 2 * s⁻¹ * (s ^ 3)⁻¹ * (cstar ^ 4)⁻¹ * (gamma ^ 2 * |Real.log gamma| ^ 4)

The sigma-bar ratio sum, in the hsig slot shape of the Step-3 regrouping.

The caller supplies e.shom.m.vs.shom.n in the manuscript's own shape, at the sigma-bar index pair (m, n-2) (whose two-scale shift is the 2 gamma summand) and at the parameter choice E ≍ cstar^(-1):

|sigma_m sigma_{n-2}^{-1} - 1|^2
  <= ( Cshom gamma (m-n) + Cshom (2 gamma + cstar^(-2) gamma |log gamma|^2) )^2
     3^(2 gamma (m-n)) .

The output is the hsig slot at the free constant Csig = 7000 Cshom^2 s^(-1).

The two side conditions are honest and discharged in-repo at the caller: |log gamma| >= 1 holds for gamma <= 1/8 (indeed for gamma <= e^(-1)), and cstar^4 <= 6 follows from the proved cstar <= 3/2.