G2ThresholdArith

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

The closed-form parameters of the 𝒢₂ proportion lane

ABK26, §4.1, the constant-selection sentence e.K.and.p.choices read as a condition on ε rather than as a choice of K₂.

The 𝒢₂ lane endpoints deliver the tail from a threshold on: after (r, M, s, θ, c₁) they produce some ε₀ > 0 and assert the tail for every ε ≥ ε₀. The threshold is not an artefact — Support.eventG2 grows with ε, so the small-ε side is genuinely the hard one — but the existential hides which condition on the parameters actually makes it hold. This module puts the parameters that condition is written in into closed form.

Contents

• g2MomentExponent — the lane's moment exponent p, in closed form (max{1, 4/s, 64rΛ/(sθ)}, Λ = log(3r) + c₁r), chosen after c₁;
• g2Normalizer — the lane's Appendix-D normalizer D, in closed form: the two Step-2 Orlicz scales at the closed s-power evaluations of G2Arith and the two per-cube amplitudes of the Section 3 anchor;
• g2MomentExponent_le and g2MomentExponent_rpow_four_le — the closed majorants of the exponent and of its fourth power;
• g2ThresholdConstOne, g2ThresholdConstTwo — the two d-only constants κ₁(d), κ₂(d) in which the lane's sufficient parameter condition is written (G2SharpArith).

Scope

Provider material: proved local helpers. Every transcendental step is an abstract-real private helper.

References

• ABK26, l.ratio.of.good.scales.for.mathcal.E, in particular the constant-selection sentence.

1. Abstract-real helpers

2. The three closed-form lane parameters

noncomputable def Algsuperdiff.Section4.Provider.Proportion.g2MomentExponent (r : ℕ) (s theta c1 : ℝ) : ℝ

The 𝒢₂ lane's moment exponent, in closed form. This is the p the proved endpoint constructs inside its existential: max{1, 4/s, 64rΛ/(sθ)} with Λ = log(3r) + c₁r. It is chosen after the rate c₁, which is why the lane carries no rate ceiling.

Equations

• Algsuperdiff.Section4.Provider.Proportion.g2MomentExponent r s theta c1 = max 1 (max (4 / s) (64 * ↑r * (Real.log (3 * ↑r) + c1 * ↑r) / (s * theta)))

noncomputable def Algsuperdiff.Section4.Provider.Proportion.g2Normalizer (d r : ℕ) (C : ℝ) (M : Section3.ABKModel d) (s theta c1 : ℝ) : ℝ

The 𝒢₂ lane's Appendix-D normalizer, in closed form. This is the D the proved endpoint constructs inside its existential: the two Step-2 Orlicz scales at the closed s-power evaluations xcalNormOne d · s^{−2} and xcalNormQuarter d · s^{−5} of G2Arith, at the two per-cube amplitudes cubeAmpOne, cubeAmpTwo of the Section 3 anchor.

Equations

• One or more equations did not get rendered due to their size.

3. Positivity

theorem Algsuperdiff.Section4.Provider.Proportion.one_le_g2MomentExponent (r : ℕ) (s theta c1 : ℝ) : 1 ≤ g2MomentExponent r s theta c1

theorem Algsuperdiff.Section4.Provider.Proportion.g2MomentExponent_pos (r : ℕ) (s theta c1 : ℝ) : 0 < g2MomentExponent r s theta c1

theorem Algsuperdiff.Section4.Provider.Proportion.four_div_le_g2MomentExponent (r : ℕ) (s theta c1 : ℝ) : 4 / s ≤ g2MomentExponent r s theta c1

theorem Algsuperdiff.Section4.Provider.Proportion.rate_le_g2MomentExponent (r : ℕ) (s theta c1 : ℝ) : 64 * ↑r * (Real.log (3 * ↑r) + c1 * ↑r) / (s * theta) ≤ g2MomentExponent r s theta c1

theorem Algsuperdiff.Section4.Provider.Proportion.cubeAmpOne_pos_of {d : ℕ} {C : ℝ} (hC : 0 < C) (M : Section3.ABKModel d) {s : ℝ} (hs : 0 < s) : 0 < cubeAmpOne d C M s

Positivity of the Γ₂-lane per-cube amplitude. (The proved lanes keep their own copies private, so this one is re-derived rather than reused.)

theorem Algsuperdiff.Section4.Provider.Proportion.cubeAmpTwo_pos_of {d : ℕ} (C : ℝ) (M : Section3.ABKModel d) : 0 < cubeAmpTwo d C M

Positivity of the Γ_{1/2}-lane per-cube amplitude.

theorem Algsuperdiff.Section4.Provider.Proportion.g2Normalizer_pos {d : ℕ} {C s : ℝ} (hC : 0 < C) (M : Section3.ABKModel d) (r : ℕ) (hs : 0 < s) (theta c1 : ℝ) : 0 < g2Normalizer d r C M s theta c1

4. The closed majorant of the moment exponent

theorem Algsuperdiff.Section4.Provider.Proportion.g2MomentExponent_le {r : ℕ} {s theta c1 : ℝ} (hr1 : 1 ≤ r) (hs0 : 0 < s) (hs1 : s ≤ 1) (hth0 : 0 < theta) (hth1 : theta ≤ 1) (hc1 : 0 ≤ c1) : g2MomentExponent r s theta c1 ≤ 192 * ↑r ^ 2 * (1 + c1) / (s * theta)

The moment exponent is at most 192 r²(1+c₁)/(sθ). All three branches of the max are paid by that single monomial: the constant branch by sθ ≤ 1, the 4/s branch by θ ≤ 1, and the rate branch by log(3r) ≤ 3r − 1.

theorem Algsuperdiff.Section4.Provider.Proportion.g2MomentExponent_rpow_four_le {r : ℕ} {s theta c1 : ℝ} (hr1 : 1 ≤ r) (hs0 : 0 < s) (hs1 : s ≤ 1) (hth0 : 0 < theta) (hth1 : theta ≤ 1) (hc1 : 0 ≤ c1) : g2MomentExponent r s theta c1 ^ 4 ≤ 1358954496 * ↑r ^ 8 * (1 + c1) ^ 4 / (s ^ 4 * theta ^ 4)

The fourth power of the majorant of the moment exponent, expanded.

6. The two threshold constants

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

The d-only constant of the binding (Γ₂-lane) clause of the 𝒢₂ threshold condition.

Equations

• One or more equations did not get rendered due to their size.

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

The d-only constant of the exponentially small (Γ_{1/2}-lane) clause of the 𝒢₂ threshold condition.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section4.Provider.Proportion.g2ThresholdConstOne_pos (d : ℕ) : 0 < g2ThresholdConstOne d

theorem Algsuperdiff.Section4.Provider.Proportion.g2ThresholdConstTwo_pos (d : ℕ) : 0 < g2ThresholdConstTwo d