Step3Arith

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

The Step-3 resummation arithmetic of the annular double sum

Local helpers for ABK26, Section 4.1, proof of Proposition p.mathcalE.annular.decomp, Step 3. The three Step-3 displays all resum the same object: a guarded annular double sum sum_{j <= m} sum_{n <= j-1} whose (j,n)-content is bounded by a polynomial in the scale gap q = m - n times a geometric weight 3^(-c q). This module proves that arithmetic once, at abstract nonnegative fields.

The two structural facts

• annDouble_eq_natIterated -- the guarded annular double sum is the iterated N-sum sum_{u} sum_{i} under j = m - u, n = m - u - 1 - i, so that the scale gap is q = m - n = u + i + 1. The j-multiplicity the manuscript writes as (m - n + 1) is exactly the number of (u,i) pairs with a given u + i; no multiplicity is inserted or dropped by hand.
• annDouble_le_of_linear_geom / annDouble_le_of_quadratic_geom -- the two resummation bounds, at a linear and at a quadratic polynomial content. The constants c^(-3) and c^(-4) are the honest ones: a degree-p polynomial content against 3^(-cq) over the annular region costs c^(-(p+2)), one power of c for the q-sum and one for the annulus multiplicity.

Where the manuscript's constants come from

Step 3's three displays are instances:

• the sigma-bar sum has quadratic content gamma^2 (m-n)^2 + cstar^(-4) gamma^2 |log gamma|^4 at rate c = s - 2 gamma, hence gamma^2 (s-2gamma)^(-4) + cstar^(-4) gamma^2 |log gamma|^4 (s-2gamma)^(-2).
• the two G_1^b displays have linear content (m - n + 2) at rate c = s/2 resp. c = (s - 4 gamma)/2, hence s^(-3) resp. (s - 4 gamma)^(-3).

The 1 - 3^(-c) >= c/2 input

Every constant below is produced from half_le_one_sub_threeRpow_neg (the proved convexity input of the resummation module), so no numeric tactic ever enters a Real.rpow or Real.log term.

Polynomial-times-geometric sums on N

theorem Algsuperdiff.Section4.Provider.Annular.summable_geom_nat {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) : Summable fun (i : ℕ) => r ^ i

Summability of (i+1)^0 r^i.

theorem Algsuperdiff.Section4.Provider.Annular.summable_poly1_geom {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) : Summable fun (i : ℕ) => (↑i + 1) * r ^ i

Summability of (i+1) r^i.

theorem Algsuperdiff.Section4.Provider.Annular.tsum_poly1_geom {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) : ∑' (i : ℕ), (↑i + 1) * r ^ i = 1 / (1 - r) ^ 2

sum_i (i+1) r^i = (1-r)^(-2).

theorem Algsuperdiff.Section4.Provider.Annular.summable_poly2_geom {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) : Summable fun (i : ℕ) => (↑i + 1) ^ 2 * r ^ i

Summability of (i+1)^2 r^i.

The N x N product sums

theorem Algsuperdiff.Section4.Provider.Annular.summable_prodFam_of_nonneg {A B : ℕ → ℝ} (hA0 : ∀ (u : ℕ), 0 ≤ A u) (hB0 : ∀ (i : ℕ), 0 ≤ B i) (hA : Summable A) (hB : Summable B) : Summable fun (p : ℕ × ℕ) => A p.1 * B p.2

The product-family summability used by every bound below.

theorem Algsuperdiff.Section4.Provider.Annular.tsum_prodFam_of_nonneg {A B : ℕ → ℝ} (hA0 : ∀ (u : ℕ), 0 ≤ A u) (hB0 : ∀ (i : ℕ), 0 ≤ B i) (hA : Summable A) (hB : Summable B) : ∑' (p : ℕ × ℕ), A p.1 * B p.2 = (∑' (u : ℕ), A u) * ∑' (i : ℕ), B i

The product-family sum.

The guarded-sum to N-shift bridge

theorem Algsuperdiff.Section4.Provider.Annular.tsum_int_guard_le (g : ℤ → ℝ) (b : ℤ) : (∑' (n : ℤ), if n ≤ b then g n else 0) = ∑' (i : ℕ), g (b - ↑i)

The guarded Z-sum as an N-sum. A sum over {n : n <= b} is the N-sum along n = b - i.

theorem Algsuperdiff.Section4.Provider.Annular.annDouble_eq_natIterated (m : ℤ) (h : ℤ → ℤ → ℝ) : annDouble m h = ∑' (u : ℕ) (i : ℕ), h (m - ↑u) (m - ↑u - 1 - ↑i)

The guarded annular double sum as an iterated N-sum. Under j = m - u and n = m - u - 1 - i the annular region {(j,n): j <= m, n <= j - 1} is exactly N x N, and the scale gap is m - n = u + i + 1.

theorem Algsuperdiff.Section4.Provider.Annular.gap_natIterated (m : ℤ) (u i : ℕ) : ↑(m - (m - ↑u - 1 - ↑i)) = ↑u + ↑i + 1

The scale gap along the N x N parametrization.

The abstract resummation bound

theorem Algsuperdiff.Section4.Provider.Annular.annDouble_le_of_natMajorant {m : ℤ} {h : ℤ → ℤ → ℝ} {F : ℕ × ℕ → ℝ} (hh0 : ∀ (j n : ℤ), 0 ≤ h j n) (hF : Summable F) (hle : ∀ (u i : ℕ), h (m - ↑u) (m - ↑u - 1 - ↑i) ≤ F (u, i)) : annDouble m h ≤ ∑' (p : ℕ × ℕ), F p

The annular resummation bound at an N x N majorant.

The two polynomial rates

theorem Algsuperdiff.Section4.Provider.Annular.annDouble_le_of_linear_geom {m : ℤ} {h : ℤ → ℤ → ℝ} {K1 K0 c : ℝ} (hc0 : 0 < c) (hc1 : c ≤ 1) (hK1 : 0 ≤ K1) (hK0 : 0 ≤ K0) (hh0 : ∀ (j n : ℤ), 0 ≤ h j n) (hle : ∀ (j n : ℤ), j ≤ m → n ≤ j - 1 → h j n ≤ (K1 * ↑(m - n) + K0) * 3 ^ (-(c * ↑(m - n)))) : annDouble m h ≤ 16 * K1 / c ^ 3 + 4 * K0 / c ^ 2

Linear content. If the annular (j,n)-content is bounded by (K1 (m-n) + K0) 3^(-c(m-n)) then the double sum is at most 16 K1 c^(-3) + 4 K0 c^(-2).

theorem Algsuperdiff.Section4.Provider.Annular.annDouble_le_of_quadratic_geom {m : ℤ} {h : ℤ → ℤ → ℝ} {K2 K0 c : ℝ} (hc0 : 0 < c) (hc1 : c ≤ 1) (hK2 : 0 ≤ K2) (hK0 : 0 ≤ K0) (hh0 : ∀ (j n : ℤ), 0 ≤ h j n) (hle : ∀ (j n : ℤ), j ≤ m → n ≤ j - 1 → h j n ≤ (K2 * ↑(m - n) ^ 2 + K0) * 3 ^ (-(c * ↑(m - n)))) : annDouble m h ≤ 128 * K2 / c ^ 4 + 4 * K0 / c ^ 2

Quadratic content. If the annular (j,n)-content is bounded by (K2 (m-n)^2 + K0) 3^(-c(m-n)) then the double sum is at most 128 K2 c^(-4) + 4 K0 c^(-2).