G2AtomTail

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

The 𝒢₂ tail lane: Step 1 (the squared annular maximum) and Step 2 (X_j)

ABK26, §4.1, e.mathcalE.squared.max.bound and e.Xj.Orlicz.bound.

max_{z ∈ 3^nℤ^d ∩ (□_j∖□_{j−1})} 𝓔_{s,2,2}(z+□_n;𝐚_{n−2},σ_{n−2})²
   ≤ 𝒪_{Γ_1}( C(j−n+1) c⋆^{−2}s^{−2}γ ) + 𝒪_{Γ_{1/4}}( C(j−n+1)⁴ exp(−C^{−1}c⋆³γ^{−1}) ) ,

X_j = K₂ε^{−2} Σ_{n ≤ j−1} 3^{−¼s(j−n)} (that maximum)
   ≤ 𝒪_{Γ_1}( CK₂c⋆^{−2}s^{−4}ε^{−2}γ ) + 𝒪_{Γ_{1/4}}( CK₂s^{−5}ε^{−2}exp(−C^{−1}c⋆³γ^{−1}) ) .

What is derived, and from what

The manuscript's Step 1 cites four inputs. Three of them are performed here:

• e.powerofGammasigma — squaring moves the Orlicz indices (2, 1/2) to (1, 1/4) and squares the amplitudes.
• e.maxy.bound — the union bound over the annulus centres.
• the lattice centre z — stationarity, not a new estimate: the per-cube atom at z is the origin atom read at the translated sample, and AtomTail.isBigOWith_comp_measurePreserving transports the tail at every real z. No per-z instance of any Section 3 statement is used.

The fourth input, Proposition p.induction.bounds composed with "subadditivity of 𝓔", is NOT derived here and is carried as the explicit hypothesis hcube of isTwoTermBigOWith_errorAnnMax. See the Frontier note below.

Step 2 is the two-term countable generalized triangle inequality isTwoTermBigOWith_wsum, proved here. The 𝒢₀ lane's one-term device (SeriesTail.isBigOWith_wsum) does not suffice: the two Orlicz indices are never merged in the manuscript, and merging them at σ = 1/4 would replace the linear p of Step 3's first term by p⁴ and break the verification E[X_j^p] ≤ 1. The device splits each summand, T = min(Y⁺, T) + (T − min(Y⁺, T)), so that the two ℝ≥0∞ series add up to the original one on the nose and the .toReal domination holds everywhere, including at the sample points where a series diverges.

Frontier (declared, not smuggled)

hcube is the display

𝓔_{s,2,2}(□_n; 𝐚_{n−2}, σ_{n−2}) ≤ 𝒪_{Γ_2}(A₁) + 𝒪_{Γ_{1/2}}(A₂)

at the O cube. The Section 3 anchor p.induction.bounds (Frozen.Section3.induction_bounds) supplies exactly this shape, but at the DIAGONAL triple (coefficient scale, domain scale, comparator scale) = (m,m,m) and at the exponent pair (∞,2); the 𝒢₂ atom needs (n−2, n, n−2) at (2,2). It is therefore taken as a hypothesis, not improvised. Note that the standing regime γ ≤ C^{−10}c⋆^{10} needed to instantiate the anchor is, per the graph, discharged at the caller and does not appear here at all.

Scope

Provider material: proved local helpers. hcube is a conditional A obligation, not a source premise.

References

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

1. Two elementary devices

theorem Algsuperdiff.Section4.Provider.Proportion.fmax_le_add_fmax {iota : Type u_2} (S : Finset iota) (T Y Z : iota → ℝ) (h : ∀ i ∈ S, T i ≤ Y i + Z i) : fmax S T ≤ fmax S Y + fmax S Z

A 0-floored maximum of a pointwise sum splits. No sign condition on the summands is needed: the 0-floor of the right side does the work.

theorem Algsuperdiff.Section4.Provider.Proportion.sq_add_le_two_mul (a b : ℝ) : (a + b) ^ 2 ≤ 2 * a ^ 2 + 2 * b ^ 2

(a+b)² ≤ 2a² + 2b², the elementary inequality that turns a two-term 𝒪_{Γ}-display into a two-term display for the square.

2. The two-term countable generalized triangle inequality

def Algsuperdiff.Section4.Provider.Proportion.splitLow {Omega : Type u_1} (T Y : Omega → ℝ) (omega : Omega) : ℝ

The Γ_{σ₁}-half of the exact splitting of a nonnegative atom.

Equations

• Algsuperdiff.Section4.Provider.Proportion.splitLow T Y omega = min (max (Y omega) 0) (T omega)

def Algsuperdiff.Section4.Provider.Proportion.splitHigh {Omega : Type u_1} (T Y : Omega → ℝ) (omega : Omega) : ℝ

The Γ_{σ₂}-half; by construction T = splitLow + splitHigh exactly.

Equations

• Algsuperdiff.Section4.Provider.Proportion.splitHigh T Y omega = T omega - Algsuperdiff.Section4.Provider.Proportion.splitLow T Y omega

theorem Algsuperdiff.Section4.Provider.Proportion.isTwoTermBigOWith_wsum {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure mu] {T : ℕ → Omega → ℝ} {c a1 a2 : ℕ → ℝ} {sigma1 sigma2 : ℝ} (hsigma1 : 0 < sigma1) (hsigma2 : 0 < sigma2) (hT0 : ∀ (i : ℕ) (omega : Omega), 0 ≤ T i omega) (hTm : ∀ (i : ℕ), Measurable (T i)) (hc : ∀ (i : ℕ), 0 < c i) (ha1 : ∀ (i : ℕ), 0 < a1 i) (ha2 : ∀ (i : ℕ), 0 < a2 i) (hsum1 : Summable fun (i : ℕ) => c i * a1 i) (hsum2 : Summable fun (i : ℕ) => c i * a2 i) (hT : ∀ (i : ℕ), Section3.Probability.IsTwoTermBigOWith mu (HCPolySupport.IndependentSums.gammaSigma sigma1) (HCPolySupport.IndependentSums.gammaSigma sigma2) (T i) (a1 i) (a2 i)) : Section3.Probability.IsTwoTermBigOWith mu (HCPolySupport.IndependentSums.gammaSigma sigma1) (HCPolySupport.IndependentSums.gammaSigma sigma2) (wsum T c) (HCPolySupport.IndependentSums.gammaTriangleConst sigma1 * ∑' (i : ℕ), c i * a1 i) (HCPolySupport.IndependentSums.gammaTriangleConst sigma2 * ∑' (i : ℕ), c i * a2 i)

The two-term countable generalized triangle inequality (e.Gamma.sigma.triangle, both lanes at once).

For nonnegative measurable atoms T_i with a two-term weak-Orlicz display at per-summand scales a₁ i, a₂ i, positive weights c_i, and both weighted scale series summable, the total ℝ≥0∞ series wsum T c has a two-term display at the scales gammaTriangleConst σ_k · Σ_i c_i a_k i.

This is the device Step 2 needs and the ambient library does not have: the library's Γ_σ triangle inequality is one-term, and applying it twice is not possible because the two witnesses of a two-term display are not themselves series of the summands' witnesses. The exact splitting splitLow/splitHigh removes that obstruction.

3. Step 1 — the squared annular maximum

theorem Algsuperdiff.Section4.Provider.Proportion.isTwoTermBigOWith_errorAnnMax {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) {A1 A2 : ℝ} (j n : ℤ) (hcube : Section3.Probability.IsTwoTermBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma (1 / 2)) (Support.annularErrorObservable M n s) A1 A2) : Section3.Probability.IsTwoTermBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 1) (HCPolySupport.IndependentSums.gammaSigma (1 / 4)) (errorAnnMax M s j n) (annulusPenalty d 1 (j - n).toNat * (2 * A1 ^ 2)) (annulusPenalty d (1 / 4) (j - n).toNat * (2 * A2 ^ 2))

Step 1, e.mathcalE.squared.max.bound.

hcube is the conditional A obligation described in the module docstring; the lattice translation and the squaring are performed here.

4. Summability of the weighted penalties

theorem Algsuperdiff.Section4.Provider.Proportion.annulusPenalty_natPow (d : ℕ) {N : ℕ} (hN : 0 < N) (p : ℕ) : annulusPenalty d (↑N)⁻¹ p = (1 + ↑d * (↑p + 1) * Real.log 3) ^ N

The lattice penalty at a reciprocal-integer Orlicz index is a natural power: at σ = 1 it is the manuscript's linear (j−n+1) and at σ = 1/4 its fourth power.

theorem Algsuperdiff.Section4.Provider.Proportion.summable_weightThird_mul_annulusPenalty (d : ℕ) {sprime A : ℝ} {N : ℕ} (hsprime : 0 < sprime) (hN : 0 < N) (hA : 0 ≤ A) : Summable fun (i : ℕ) => weightThird sprime (i + 1) * (annulusPenalty d (↑N)⁻¹ (i + 1) * A)

The weighted lattice penalties of the 𝒢₂ lane are summable, at every positive rate and every reciprocal-integer Orlicz index. This is the input the countable triangle inequality consumes; the manuscript performs the same estimate implicitly when it writes the closed forms s^{-4} and s^{-5}.

5. Step 2 — the X_j Orlicz bound

theorem Algsuperdiff.Section4.Provider.Proportion.isTwoTermBigOWith_Xcal {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (j : ℤ) {A1 A2 : ℝ} (hA1 : 0 < A1) (hA2 : 0 < A2) (hcube : ∀ n ≤ j - 1, Section3.Probability.IsTwoTermBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma (1 / 2)) (Support.annularErrorObservable M n s) A1 A2) : Section3.Probability.IsTwoTermBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 1) (HCPolySupport.IndependentSums.gammaSigma (1 / 4)) (fun (omega : Section3.Cutoff.CutoffSample d) => (XcalE M s j omega).toReal) (HCPolySupport.IndependentSums.gammaTriangleConst 1 * ∑' (i : ℕ), weightThird (↑s / 4) (i + 1) * (annulusPenalty d 1 (i + 1) * (2 * A1 ^ 2))) (HCPolySupport.IndependentSums.gammaTriangleConst (1 / 4) * ∑' (i : ℕ), weightThird (↑s / 4) (i + 1) * (annulusPenalty d (1 / 4) (i + 1) * (2 * A2 ^ 2)))

Step 2, e.Xj.Orlicz.bound.

The atom X_j (without the lane prefactor K₂ε^{−2}) inherits a two-term display from Step 1 through the countable generalized triangle inequality, applied at σ = 1 and σ = 1/4 simultaneously.

hcube is the per-inner-scale conditional A obligation of Step 1.