ShiftedG2Lane

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

The 𝒢₂ proportion lane re-based at an arbitrary scale m₀

ABK26, §4.1, l.ratio.of.good.scales.for.mathcal.E, composed into e.no.bad.scales.applied.for.lambdas and read on the window {m₀,…,m₀+n} rather than on {0,…,n}.

The proved 𝒢₂ lane is stated at base 0: its window is the Finset.Icc (0:ℤ) (n:ℤ) inside IndicatorDensity.scaleProp. The manuscript's own reduction of the general window to that one is "translate the array", carried out once and generically in ShiftedConcentration. This module runs the 𝒢₂ lane through that translation.

Contents

• ratioTail_Xcal_shift — the 𝒢₂ lemma-level tail on {m₀,…,m₀+n}. Its hypothesis list is the base-0 lane's, with the base m₀ added and the deterministic reduction asked at every scale m : ℤ instead of only at m ≥ 0.
• hreduce_eventG2_all — the 𝒢₂ row reduction of G2RowConversion with its unused sign binder dropped, so that it can be instantiated at a negative scale.

Scope

Provider material: proved local helpers.

References

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

1. The 𝒢₂ lemma-level tail on the window {m₀,…,m₀+n}

theorem Algsuperdiff.Section4.Provider.Proportion.ratioTail_Xcal_shift {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (D : ℝ) {A1 A2 p theta c1 Q : ℝ} {r : ℕ} (Ev : ℤ → Set (Section3.Cutoff.CutoffSample d)) (m0 : ℤ) (hA1 : 0 < A1) (hA2 : 0 < A2) (hD : 0 < D) (hp : 1 ≤ p) (hs1 : ↑s ≤ 1) (hsp : 1 ≤ ↑s / 4 * p) (hr1 : 1 ≤ r) (hQ : 1 ≤ Q) (htheta0 : 0 < theta) (hthetar : theta * (↑r + 1) < 1) (hc1 : 0 ≤ c1) (hrate : Real.log (Q * ↑r) + c1 * ↑r ≤ ↑s / 4 * p * theta / (16 * ↑r)) (hcube : ∀ (n : ℤ), Section3.Probability.IsTwoTermBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma (1 / 2)) (Support.annularErrorObservable M n s) A1 A2) (hnorm : HCPolySupport.IndependentSums.gammaMomentConst 1 * p * xcalScaleOne d (↑s) A1 + HCPolySupport.IndependentSums.gammaMomentConst (1 / 4) * p ^ 4 * xcalScaleQuarter d (↑s) A2 ≤ D) (hrgap : 3 + 2 * 3 ^ (1 - 2) * √↑d ≤ 3 ^ r) (hreduce : ∀ (m : ℤ), ∀ omega ∈ (Ev m)ᶜ, 9 * (↑s / 4)⁻¹ * Probability.ScalesConcentration.Cstar ^ (1 / p) * theta ^ (-1 / p) < Probability.ScalesConcentration.Yk (xcalArray M s D) (↑s / 4) m omega) (n : ℕ) : ↑(Section3.Cutoff.cutoffSampleLaw M) {omega : Section3.Cutoff.CutoffSample d | theta < Probability.IndicatorDensity.scaleProp (fun (k : ℤ) => (Ev (m0 + k))ᶜ) n omega} ≤ ENNReal.ofReal (Real.exp (-c1 * ↑n) / Q)

The 𝒢₂-lane proportion tail at an arbitrary base scale m₀.

For every window {m₀,…,m₀+n} — including the short windows n < r that p.concentration.for.scales does not reach (closed by the proved ratioTail_of_concentration with no extra hypothesis) —

ℙ[ θ < (proportion of scales m₀+k, k ≤ n, at which Ev fails) ] ≤ exp(−c₁ n) / Q .

This is the base-0 𝒢₂ lemma-level tail with the base added: the same hypothesis list, except that the deterministic reduction is asked at every scale m : ℤ rather than only at m ≥ 0, which is what the lane in fact proves. The translation of the Appendix-D array is ratioTail_of_concentration_shift.

2. The reduction at every scale

theorem Algsuperdiff.Section4.Provider.Proportion.hreduce_eventG2_all {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) {ep p theta D : ℝ} (hD : 0 < D) (hthr : 9 * (↑s / 4)⁻¹ * Probability.ScalesConcentration.Cstar ^ (1 / p) * theta ^ (-1 / p) ≤ D⁻¹ * (ep ^ 2 / ↑s)) (m : ℤ) (omega : Section3.Cutoff.CutoffSample d) (homega : omega ∈ (Support.eventG2 M m s ep ∪ (goodRowSetG2 M s)ᶜ)ᶜ) : 9 * (↑s / 4)⁻¹ * Probability.ScalesConcentration.Cstar ^ (1 / p) * theta ^ (-1 / p) < Probability.ScalesConcentration.Yk (xcalArray M s D) (↑s / 4) m omega

The hreduce slot of the 𝒢₂ concentration assembly, for the enlarged family, at every scale.

This is the 𝒢₂ row reduction with its unused sign binder 0 ≤ m dropped, so that it can be instantiated at a negative scale. The proof runs on the public, sign-condition-free G2RowConversion.lt_Yk_of_notMem_eventG2.

hthr is the lane's threshold identification: the Appendix-D level 9 s'^{-1}C_⋆^{1/p}θ^{-1/p} at s' = ¼s must sit below D^{-1}ε²s^{-1}.