BaseCaseMStarError

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

The corrected shifted base-case error tail below the second landmark

This module proves the error half of the corrected Section 3.2 base case on the range m <= m*. The cutoff response square is bounded almost everywhere by a deterministic plateau plus the linearly weighted descendant mass. The plateau has square root at most one on this range, so it fits inside the source's deterministic shift 2. The weighted mass has a one-sided Gamma_1 tail whose square-root scale gives the exact shifted Gamma_2 amplitude, with one dimension-only constant chosen before every model and scale parameter.

Main results

• cutoffHomogenizationError_isDeterministicShiftOneSidedOrlicz_le_mStar proves the direct model-specific shifted tail, with the amplitude displayed explicitly in terms of cutoffMassSqrtConst, cstarPlus M and baseLoss.

theorem Algsuperdiff.Section3.Provider.Base.cutoffHomogenizationError_isDeterministicShiftOneSidedOrlicz_le_mStar {d : ℕ} (M : ABKModel d) (m : ℤ) (hm : m ≤ mStar M) (s : { s : ℝ // s ∈ Set.Ioo 0 1 }) : Probability.IsDeterministicShiftOneSidedOrlicz (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (Observable.cutoffHomogenizationError M m ⟨↑s, ⋯⟩) 2 (cutoffMassSqrtConst d * (√(Disorder.cstarPlus M))⁻¹ * √(baseLoss d s))

Below m*, the cutoff homogenization error has the corrected shifted one-sided Gamma_2 tail with its explicit dimension-only constant.