HomSpineGamma0

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

Theorem B, §4.5, Step 1: collapsing the hY gates to one γ₀

The target

This file closes hY (HomMomentTail.homY_moment_bound) modulo THREE displayed gates,

  hratio: 3^{(1-α)2p} e^{-θ} ≤ 1/2,      θ = (1-α)²/(C γ),
  htrunc: 3^{(1-α)2p N₀} ≤ 2^p,
  hsmall: 2 (C e^{(1-α)²/γ}) (3^{(1-α)2p} e^{-θ})^{N₀+1} ≤ 1,

with N₀ a free cut. This module collapses them to ONE γ-threshold plus the theorem's own p-range. Nothing analytic is added: every step is the elementary comparison of a logarithm with a power of γ.

The choices, and why they are forced

htrunc wants N₀ SMALL (N₀ s log 3 ≤ log 2) while hsmall wants N₀ LARGE. The tension is resolved by the shape of the Theorem-C tail P{X ≥ N} ≤ C e^{-(1-α)²(N-C)/(Cγ)}, whose turn-on is at N ≈ C: the cut must be placed just past it and nowhere else. Hence

  N₀:= ⌈C⌉₊ + 2          (homGateCut),
  C₁:= 16 C (N₀+1) log 3 (homGateRangeConst) — the p-range constant,

and then a:= (1-α)(2p) = s p obeys a (N₀+1) log 3 ≤ θ/4 EXACTLY (the choice of C₁ makes this an equality of the two majorants), while N₀+1 ≥ C+3 makes the hsmall exponent Cθ - θ(N₀+1) ≤ -3θ. With θ ≥ 2(log 2 + log 2C) the three gates follow.

The single threshold

  HomGammaGate C γ:=  γ (log γ)² ≤ κ(C)  ∧  N₀ log 3 ≤ |log γ| log 2,
      κ(C) = (8 C (log 2 + log 2C))⁻¹,

and homGamma0Gate C:= min ((κ/16)², exp(-N₀ log 3 / log 2)) is an EXPLICIT positive witness: γ ≤ homGamma0Gate C ⟹ HomGammaGate C γ (homGammaGate_of_le_homGamma0). The first clause uses only the absLog_le_four_div_quarticRoot, i.e. γ(log γ)² ≤ 16√γ; the second is monotonicity of log. So the three displayed gates become the single hypothesis M.gamma ≤ homGamma0Gate C.

1. The three gates as logarithmic inequalities

theorem Algsuperdiff.Section4.Provider.Homogenization.gate_ratio_of_log {a theta : ℝ} (h : a * Real.log 3 + Real.log 2 ≤ theta) : 3 ^ a * Real.exp (-theta) ≤ 1 / 2

hratio from one linear inequality between logarithms.

theorem Algsuperdiff.Section4.Provider.Homogenization.gate_trunc_of_log {a p : ℝ} (h : a * Real.log 3 ≤ p * Real.log 2) : 3 ^ a ≤ 2 ^ p

htrunc from one linear inequality between logarithms.

theorem Algsuperdiff.Section4.Provider.Homogenization.gate_small_of_log {Cst a theta : ℝ} {N : ℕ} (hCst : 0 < Cst) (h : Real.log (2 * Cst) + Cst * theta + Real.log 3 * a * ↑N - theta * ↑N ≤ 0) : 2 * (Cst * Real.exp (Cst * theta) * (3 ^ a * Real.exp (-theta)) ^ N) ≤ 1

hsmall from one linear inequality between logarithms.

2. The cut, the range constant, and the threshold

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.homGateCut (Cst : ℝ) : ℕ

The cut N₀:= ⌈C⌉₊ + 2, placed just past the Theorem-C tail's turn-on N ≈ C. Any smaller cut breaks hsmall, any larger one breaks htrunc.

Equations

• Algsuperdiff.Section4.Provider.Homogenization.homGateCut Cst = ⌈Cst⌉₊ + 2

theorem Algsuperdiff.Section4.Provider.Homogenization.homGateCut_ge (Cst : ℝ) : Cst + 2 ≤ ↑(homGateCut Cst)

theorem Algsuperdiff.Section4.Provider.Homogenization.one_le_homGateCut (Cst : ℝ) : 1 ≤ ↑(homGateCut Cst)

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.homGateRangeConst (Cst : ℝ) : ℝ

The p-range constant C₁:= 16 C (N₀+1) log 3.

Equations

• Algsuperdiff.Section4.Provider.Homogenization.homGateRangeConst Cst = 16 * Cst * (↑(Algsuperdiff.Section4.Provider.Homogenization.homGateCut Cst) + 1) * Real.log 3

theorem Algsuperdiff.Section4.Provider.Homogenization.homGateRangeConst_pos {Cst : ℝ} (hCst : 1 ≤ Cst) : 0 < homGateRangeConst Cst

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.homGateKappa (Cst : ℝ) : ℝ

κ(C) = (8 C (log 2 + log 2C))⁻¹, the γ(log γ)² budget.

Equations

• Algsuperdiff.Section4.Provider.Homogenization.homGateKappa Cst = (8 * Cst * (Real.log 2 + Real.log (2 * Cst)))⁻¹

theorem Algsuperdiff.Section4.Provider.Homogenization.homGateKappa_pos {Cst : ℝ} (hCst : 1 ≤ Cst) : 0 < homGateKappa Cst

def Algsuperdiff.Section4.Provider.Homogenization.HomGammaGate (Cst gamma : ℝ) : Prop

THE SINGLE γ-THRESHOLD PREDICATE. Both clauses are pure smallness of γ; together with the theorem's own p-range they imply all three displayed gates (homGates_of_gammaGate).

Equations

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

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.homGamma0Gate (Cst : ℝ) : ℝ

The explicit threshold γ₀(C).

Equations

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

theorem Algsuperdiff.Section4.Provider.Homogenization.homGamma0Gate_pos {Cst : ℝ} (hCst : 1 ≤ Cst) : 0 < homGamma0Gate Cst

theorem Algsuperdiff.Section4.Provider.Homogenization.gamma_mul_sq_log_le {gamma : ℝ} (hg : 0 < gamma) (hg1 : gamma < 1) : gamma * Real.log gamma ^ 2 ≤ 16 * √gamma

γ (log γ)² ≤ 16 √γ for 0 < γ < 1 — the quartic-root comparison, the only place a logarithm meets a power of γ.

theorem Algsuperdiff.Section4.Provider.Homogenization.homGammaGate_of_le_homGamma0 {Cst gamma : ℝ} (hCst : 1 ≤ Cst) (hg : 0 < gamma) (hle : gamma ≤ homGamma0Gate Cst) : HomGammaGate Cst gamma

γ ≤ γ₀(C) implies the single gate.

3. The three gates at the §4.5 parameter web

theorem Algsuperdiff.Section4.Provider.Homogenization.homGates_of_gammaGate {d : ℕ} (M : Section3.ABKModel d) {Cst p : ℝ} (hCst : 1 ≤ Cst) (hp : 1 ≤ p) (hL : 4 ≤ |Real.log M.gamma|) (hgate : HomGammaGate Cst M.gamma) (hrange : p ≤ (homGateRangeConst Cst)⁻¹ * M.gamma⁻¹ * |Real.log M.gamma|⁻¹) : 3 ^ ((1 - homAlpha M) * (2 * p)) * Real.exp (-((1 - homAlpha M) ^ 2 / (Cst * M.gamma))) ≤ 1 / 2 ∧ 3 ^ ((1 - homAlpha M) * (2 * p) * ↑(homGateCut Cst)) ≤ 2 ^ p ∧ 2 * (Cst * Real.exp ((1 - homAlpha M) ^ 2 / M.gamma) * (3 ^ ((1 - homAlpha M) * (2 * p)) * Real.exp (-((1 - homAlpha M) ^ 2 / (Cst * M.gamma)))) ^ (homGateCut Cst + 1)) ≤ 1

THE COLLAPSE. At the §4.5 web 1 - α = s/2, s = |log γ|⁻¹, the single threshold HomGammaGate C γ together with the theorem's own p-range p ≤ C₁⁻¹ γ⁻¹ |log γ|⁻¹ implies all THREE displayed gates of homY_moment_bound, at the cut N₀ = homGateCut C.

4. hY under the single threshold

theorem Algsuperdiff.Section4.Provider.Homogenization.homY_moment_bound_of_gamma_le {d : ℕ} (M : Section3.ABKModel d) {X : Section3.Cutoff.CutoffSample d → ℕ∞} (hX : Measurable X) {Cst p : ℝ} (hCst : 1 ≤ Cst) (hp : 1 ≤ p) (hL : 4 ≤ |Real.log M.gamma|) (hgamma : M.gamma ≤ homGamma0Gate Cst) (hrange : p ≤ (homGateRangeConst Cst)⁻¹ * M.gamma⁻¹ * |Real.log M.gamma|⁻¹) (htail : ∀ (N : ℕ), ↑(Section3.Cutoff.cutoffSampleLaw M) {omega : Section3.Cutoff.CutoffSample d | ↑N ≤ X omega} ≤ ENNReal.ofReal (Cst * Real.exp (-((1 - homAlpha M) ^ 2 * (↑N - Cst)) / (Cst * M.gamma)))) : ∫⁻ (omega : Section3.Cutoff.CutoffSample d), homMinimalScaleFactor (1 - homAlpha M) X omega ^ (2 * p) ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal 2 ^ (2 * p)

hY, with the three displayed gates replaced by ONE γ-threshold.

homY_moment_bound with hratio, htrunc, hsmall discharged from M.gamma ≤ homGamma0Gate Cst and the theorem's own p-range. Cst is the C(d,c⋆) of Theorem C, so homGamma0Gate Cst is a γ₀(d,c⋆).