G2Arith

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

The closed s-power evaluation of the 𝒢₂ Step-2 Orlicz scales

ABK26, §4.1, the closed forms the manuscript writes in e.Xj.Orlicz.bound without proof:

X_j ≤ 𝒪_{Γ_1}( C K₂ c⋆^{−2} s^{−4} ε^{−2} γ )
    + 𝒪_{Γ_{1/4}}( C K₂ s^{−5} ε^{−2} exp(−C^{−1}c⋆³γ^{−1}) ) .

G2AtomTail.isTwoTermBigOWith_Xcal produces those two scales as the weighted penalty series

Σ_{i ≥ 0} 3^{−¼s(i+1)} (1 + d(i+2)log 3)^k · A ,     k = 1, 4 ,

(xcalScaleOne and xcalScaleQuarter of G2Moments). This module evaluates both in closed form, at C(d)·s^{−(k+1)}: s^{−2} at k = 1 and s^{−5} at k = 4. Since the Γ_2-lane per-cube amplitude A₁ itself carries one power of s^{−1} and enters squared, the composed lane scales are the manuscript's s^{−4} and s^{−5}.

This is the 𝒢₂ twin of RatioTailArith.tsum_weightThird_mul_annulusPenaltyThird_le (the 𝒢₀ lane's γ^{−4} closed form), and it is not optional: without an explicit majorant for the two scales the Appendix-D threshold identification of the lane endpoint cannot be closed at all.

Route

Three ingredients, exactly as on the 𝒢₀ lane:

• the penalty bound 1 + d(i+2)log 3 ≤ (1 + 2d log 3)(i+1), so the growing lattice-max penalty is a polynomial in the offset at a dimensional constant;
• (i+1)^k ≤ k!·binom(i+k,k) and Mathlib's tsum_choose_mul_geometric_of_norm_lt_one k, giving k!/(1−w)^{k+1};
• the spectral gap 1 − 3^{−s/4} ≥ s/8, valid on the whole standing window s ∈ (0,1] (the 𝒢₀ lane's version is stated at γ ≤ 1/4; the 𝒢₂ lane needs it up to s = 1, and the same convexity argument delivers it).

Per the elaboration discipline the single transcendental step (the spectral gap) is confined to an abstract-real private helper and no numeric tactic ever sees Real.rpow, Real.exp or Real.log applied to a variable.

Scope

Provider material: proved local helpers.

References

• ABK26, l.ratio.of.good.scales.for.mathcal.E.

1. The spectral gap of the 𝒢₂ weight, on the whole window

2. The two elementary combinatorial bounds

3. The two dimensional constants

noncomputable def Algsuperdiff.Section4.Provider.Proportion.xcalNormOne (d : ℕ) : ℝ

The dimensional constant of the Γ_1-lane closed form.

Equations

• Algsuperdiff.Section4.Provider.Proportion.xcalNormOne d = 64 * (1 + 2 * ↑d * Real.log 3)

noncomputable def Algsuperdiff.Section4.Provider.Proportion.xcalNormQuarter (d : ℕ) : ℝ

The dimensional constant of the Γ_{1/4}-lane closed form.

Equations

• Algsuperdiff.Section4.Provider.Proportion.xcalNormQuarter d = 786432 * (1 + 2 * ↑d * Real.log 3) ^ 4

theorem Algsuperdiff.Section4.Provider.Proportion.xcalNormOne_pos (d : ℕ) : 0 < xcalNormOne d

theorem Algsuperdiff.Section4.Provider.Proportion.xcalNormQuarter_pos (d : ℕ) : 0 < xcalNormQuarter d

4. The penalty bound

5. The two closed forms

theorem Algsuperdiff.Section4.Provider.Proportion.tsum_weightThird_mul_annulusPenalty_one_le (d : ℕ) {s A : ℝ} (hs0 : 0 < s) (hs1 : s ≤ 1) (hA : 0 ≤ A) : ∑' (i : ℕ), weightThird (s / 4) (i + 1) * (annulusPenalty d 1 (i + 1) * A) ≤ xcalNormOne d / s ^ 2 * A

The Γ_1-lane weighted penalty series, in closed form: C(d)·s^{−2}.

theorem Algsuperdiff.Section4.Provider.Proportion.tsum_weightThird_mul_annulusPenalty_quarter_le (d : ℕ) {s A : ℝ} (hs0 : 0 < s) (hs1 : s ≤ 1) (hA : 0 ≤ A) : ∑' (i : ℕ), weightThird (s / 4) (i + 1) * (annulusPenalty d (1 / 4) (i + 1) * A) ≤ xcalNormQuarter d / s ^ 5 * A

The Γ_{1/4}-lane weighted penalty series, in closed form: C(d)·s^{−5}.

6. The two lane scales, in closed form

theorem Algsuperdiff.Section4.Provider.Proportion.xcalScaleOne_le (d : ℕ) {s A1 : ℝ} (hs0 : 0 < s) (hs1 : s ≤ 1) : xcalScaleOne d s A1 ≤ HCPolySupport.IndependentSums.gammaTriangleConst 1 * (xcalNormOne d / s ^ 2 * (2 * A1 ^ 2))

xcalScaleOne ≤ C(d)·s^{−2}·A₁² — the closed evaluation of the Γ_1-lane Step-2 scale. Composed with the per-cube amplitude A₁ ∼ C c⋆^{−1}s^{−1}√γ of the anchor this is the manuscript's C K₂ c⋆^{−2}s^{−4}ε^{−2}γ.

theorem Algsuperdiff.Section4.Provider.Proportion.xcalScaleQuarter_le (d : ℕ) {s A2 : ℝ} (hs0 : 0 < s) (hs1 : s ≤ 1) : xcalScaleQuarter d s A2 ≤ HCPolySupport.IndependentSums.gammaTriangleConst (1 / 4) * (xcalNormQuarter d / s ^ 5 * (2 * A2 ^ 2))

xcalScaleQuarter ≤ C(d)·s^{−5}·A₂² — the closed evaluation of the Γ_{1/4}-lane Step-2 scale, the manuscript's C K₂ s^{−5}ε^{−2}exp(−C^{−1}c⋆³γ^{−1}) (the per-cube amplitude A₂ carries no power of s).