BaseCaseAllScaleError

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

The corrected all-scale base-case error tail

This module proves the error half of the corrected Section 3.2 base case at every integer scale. The cutoff response square is bounded almost everywhere by a deterministic plateau plus the linearly weighted descendant mass. Both square roots have the same all-scale core, so the one-term square-root transform gives a Gamma_2 tail at the exact corrected first amplitude. Promoting that tail with a zero Gamma_4 witness gives the source's two-term conclusion at the two exact corrected amplitudes.

Main results

• cutoffHomogenizationError_isOneSidedOrlicz_allScale proves the stronger direct one-sided Gamma_2 tail used internally.
• cutoffHomogenizationError_isTwoTermBigOWith_allScale proves the corrected source-facing all-scale two-term tail.

theorem Algsuperdiff.Section3.Provider.Base.cutoffHomogenizationError_isOneSidedOrlicz_allScale {d : ℕ} (M : ABKModel d) (m : ℤ) (s : { s : ℝ // s ∈ Set.Ioo 0 1 }) : Probability.IsOneSidedOrlicz (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (Observable.cutoffHomogenizationError M m ⟨↑s, ⋯⟩) (baseCaseMStarStarErrorConst d * M.nu⁻¹ * (√M.gamma)⁻¹ * 3 ^ (M.gamma * ↑m) * √(baseLoss d s))

At every integer scale, the cutoff homogenization error has a corrected one-sided Gamma_2 tail at the first all-scale amplitude.

theorem Algsuperdiff.Section3.Provider.Base.cutoffHomogenizationError_isTwoTermBigOWith_allScale {d : ℕ} (M : ABKModel d) (m : ℤ) (s : { s : ℝ // s ∈ Set.Ioo 0 1 }) : Probability.IsTwoTermBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma 4) (Observable.cutoffHomogenizationError M m ⟨↑s, ⋯⟩) (baseCaseMStarStarErrorConst d * M.nu⁻¹ * (√M.gamma)⁻¹ * 3 ^ (M.gamma * ↑m) * √(baseLoss d s)) (baseCaseMStarStarErrorConst d * (√M.nu)⁻¹ * (√√M.gamma)⁻¹ * 3 ^ (M.gamma * ↑m / 2) * √√(baseLoss d s))

At every integer scale, the cutoff homogenization error satisfies the corrected two-term Gamma_2/Gamma_4 base-case tail.