Step3

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

The Step-3 arithmetic of the annular decomposition

Local helpers for ABK26, Section 4.1, proof of Proposition p.mathcalE.annular.decomp, Step 3: the two arithmetic cores behind the constants that convert the intermediate five-term estimate e.mathcalE.annular.decomp.pre.zero into the final four-term display.

Everything here is a proved conditional helper over abstract reals. The caller-supplied inequalities (the three field-level order-of-summation interchanges, the sigma-bar continuity sum, the l^1/W^{2,infty} sums) are conditional A obligations, not source premises; no source node is claimed, realized or closed by this module.

Contents

• poly2_geom_tail_le -- the polynomial-times-geometric summation core sum_i (i+1)^2 r^i <= 2 (1-r)^(-3), the origin of the C s^(-3) constants of the three Step-3 interchanges (1 - 3^(-s/2) is comparable to s).
• sub_four_gamma_inv_cube_le -- the (s - 4 gamma)^(-3) <= 8 s^(-3) absorption under the standing hypothesis s >= 8 gamma, which is what lets both G_1^b interchanges be quoted with the single constant C s^(-3).

The polynomial-times-geometric summation core

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

Polynomial-times-geometric tail (abstract reals). For r in [0,1), sum_i (i+1)^2 r^i <= 2 (1-r)^(-3), via sum_i C(i+2,2) r^i = (1-r)^(-3) and the termwise bound (i+1)^2 <= 2 C(i+2,2). With 1 - r comparable to s (base r = 3^(-s/2)) this is the origin of the C s^(-3) factors of Step 3.

The (s - 4 gamma)^(-3) absorption

theorem Algsuperdiff.Section4.Provider.Annular.sub_four_gamma_inv_cube_le {s gamma : ℝ} (hs : 0 < s) (hsg : 8 * gamma ≤ s) : ((s - 4 * gamma) ^ 3)⁻¹ ≤ 8 * (s ^ 3)⁻¹

The (s - 4 gamma)^(-3) -> s^(-3) absorption. The second Step-3 interchange produces the constant C (s - 4 gamma)^(-3); under the standing hypothesis s >= 8 gamma one has s - 4 gamma >= s/2, hence (s - 4 gamma)^(-3) <= 8 s^(-3), so both interchanges may be quoted with the single constant C s^(-3).