SuccessorMoment

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

Successor moment bound for the localized regularity

The pointwise regularity estimate is combined with moments of its minimal-scale factor and of the localized error. The logarithmic loss in the exponent keeps the doubled exponent inside both available moment ranges.

theorem Algsuperdiff.Section4.Provider.s5_regularity_moment_bound_v2_provider (d : ℕ) (cstar : ℝ) (hcstar : 0 < cstar) : ∃ (gamma0 : ℝ) (c : ℝ) (C : ℝ), 0 < gamma0 ∧ 0 < c ∧ 0 < C ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∀ (n : ℤ) (y : HCPolySupport.Vec d), ∫⁻ (omega : Section3.Cutoff.CutoffSample d), Section5.Support.localizedRegularity M n y omega ^ (c * M.gamma⁻¹ * |Real.log M.gamma| ^ (-6)) ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal C ^ (c * M.gamma⁻¹ * |Real.log M.gamma| ^ (-6))

The localized regularity moment bound at the successor logarithmic exponent.