ShiftedG0Lane

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

The 𝒢₀ proportion tail on a window based at an arbitrary scale m₀

ABK26, §4.1, e.no.bad.scales.applied.for.lambdas for the 𝒢₀ lane, on the window {m₀,…,m₀+n} rather than {0,…,n}.

The level-uniform 𝒢₀ endpoint is stated for the base-0 window that IndicatorDensity.scaleProp hard-codes. Downstream consumers read the proportion over a window that starts at an arbitrary scale m₀, and the manuscript's own reduction is "translate the array". ShiftedConcentration carries out that translation once and generically; this module feeds the 𝒢₀ lane's array and event family through it.

Main results

• hreduce_eventG0_all — the proved deterministic reduction of the 𝒢₀ bad event into the Appendix-D threshold event, at every scale m : ℤ.
• ratioTail_Ycal_shift — the 𝒢₀-lane proportion tail engine on the window {m₀,…,m₀+n}: the base-0 hypothesis list, with the deterministic reduction asked at every m : ℤ.
• exists_ratioTail_eventG0_uniform_shift — the level-uniform endpoint on the window {m₀,…,m₀+n}, with the constant C(d) and the range r(d) chosen before M, before θ and before the base m₀.

The base-independence of the constants

m₀ and the window length n are quantified last, after r, C, the model, the level and the rate. So the numerical package — the three θ-free floors, the budget E = C c⋆^{−1}, the atom exponent u = c⋆²/(C_cg C² γ), the moment exponent p = exp(u/6) and the normalizer D — is built once and does not see the base scale. The base enters only through the diagonal translation of the Appendix-D array, which is what ShiftedConcentration proves is free.

Scope

Provider material: proved local helpers.

References

• ABK26, l.good.scales.ratio.lambda; p.concentration.for.scales.

1. The order-8 opening of the exponential

The abstract-real helper; the only transcendental atom in this file that a numeric step ever sees, and it is discharged before any carrier appears.

2. The deterministic reduction, at every scale

A window based at m₀ < 0 needs the deterministic reduction of the 𝒢₀ bad event at negative scales. The statement below carries no sign condition on m, which costs nothing: RowSumFinite.lt_Yk_of_notMem_eventG0 carries none either.

theorem Algsuperdiff.Section4.Provider.Proportion.hreduce_eventG0_all {d : ℕ} (M : Section3.ABKModel d) (Ccg : ℝ) {p theta D : ℝ} (hD : 0 < D) (hthr : 9 * (M.gamma / 4)⁻¹ * Probability.ScalesConcentration.Cstar ^ (1 / p) * theta ^ (-1 / p) ≤ D⁻¹) (m : ℤ) (omega : Section3.Cutoff.CutoffSample d) (homega : omega ∈ (Support.eventG0 M Ccg m ∪ (goodRowSet M Ccg (M.gamma / 4))ᶜ)ᶜ) : 9 * (M.gamma / 4)⁻¹ * Probability.ScalesConcentration.Cstar ^ (1 / p) * theta ^ (-1 / p) < Probability.ScalesConcentration.Yk (ycalArray M Ccg (M.gamma / 4) D) (M.gamma / 4) m omega

The hreduce slot at every scale m : ℤ. hthr is the manuscript's own threshold identification: the Appendix-D level 9 s'^{-1} C_⋆^{1/p} θ^{-1/p} must sit below the normalizer's reciprocal.

3. The 𝒢₀ engine on a window based at m₀

theorem Algsuperdiff.Section4.Provider.Proportion.ratioTail_Ycal_shift {d : ℕ} (M : Section3.ABKModel d) (Ccg sprime D : ℝ) {sigma p theta c1 Q K : ℝ} {r : ℕ} (Ev : ℤ → Set (Section3.Cutoff.CutoffSample d)) (m0 : ℤ) (hsigma : 0 < sigma) (hK : 0 < K) (hD : 0 < D) (hp : 1 ≤ p) (hs' : 0 < sprime) (hs'1 : sprime ≤ 1) (hsp : 1 ≤ sprime * 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 ≤ sprime * p * theta / (16 * ↑r)) (htail : ∀ (n : ℤ), HCPolySupport.IndependentSums.IsBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma sigma) (Ycal M Ccg sprime n) K) (hnorm : HCPolySupport.IndependentSums.gammaMomentConst sigma * p ^ sigma⁻¹ * K ≤ D) (hrgap : 3 + 2 * 3 ^ (1 - 2) * √↑d ≤ 3 ^ r) (hloc : ∀ (n : ℤ), Measurable (Ycal M Ccg sprime n)) (hreduce : ∀ (m : ℤ), ∀ omega ∈ (Ev m)ᶜ, 9 * sprime⁻¹ * Probability.ScalesConcentration.Cstar ^ (1 / p) * theta ^ (-1 / p) < Probability.ScalesConcentration.Yk (ycalArray M Ccg sprime D) sprime 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 on the window {m₀,…,m₀+n}.

The base-0 hypothesis list of the 𝒢₀ engine, with two changes: an extra base scale m₀ : ℤ, and the deterministic reduction hreduce asked at every scale m : ℤ rather than only at m ≥ 0 (hreduce_eventG0_all supplies exactly that for the 𝒢₀ lane). The conclusion is the same tail bound

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

including the short windows n < r.

The proof is the proved engine with its last step routed through ShiftedConcentration.ratioTail_of_concentration_shift: the four Appendix-D inputs — entrywise measurability, entrywise nonnegativity, the unit moments lintegral_rpow_le_one_Ycal and the r-dependence columnsIndep_Ycal — are supplied for the base array, and the diagonal translation is free.

4. The level-uniform endpoint on a window based at m₀

theorem Algsuperdiff.Section4.Provider.Proportion.exists_ratioTail_eventG0_uniform_shift (d : ℕ) : ∃ (r : ℕ), 1 ≤ r ∧ ∃ (C : ℝ), 6 ≤ C ∧ ∀ (M : Section3.ABKModel d), M.gamma ≤ C⁻¹ ^ 10 * Section3.Disorder.cstar M ^ 10 → ∀ (theta : ℝ), 0 < theta → theta * (↑r + 1) < 1 → C ^ 9 * M.gamma ^ 2 ≤ theta * Section3.Disorder.cstar M ^ 8 → ∀ (c1 : ℝ), 0 ≤ c1 → c1 * M.gamma ≤ 1 → ∀ (m0 : ℤ) (n : ℕ), ↑(Section3.Cutoff.cutoffSampleLaw M) {omega : Section3.Cutoff.CutoffSample d | theta < Probability.IndicatorDensity.scaleProp (fun (k : ℤ) => (Support.eventG0 M (Support.cgEllipLowerConstant d) (m0 + k))ᶜ) n omega} ≤ ENNReal.ofReal (Real.exp (-c1 * ↑n) / 3)