BaseCaseMStarStarError

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

The corrected base-case error tail below the first 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 latter has a one-sided Gamma_1 tail. The one-term square-root transform turns these two inputs into the exact one-sided Gamma_2 bound, with one explicit dimension-only constant chosen before the model and all scale parameters.

Main results

• baseCaseMStarStarErrorConst is the explicit positive dimension-only constant for this branch.
• cutoffHomogenizationError_isOneSidedOrlicz_le_mStarStar proves the direct model-specific tail at that constant.
• exists_baseCaseMStarStarErrorConst packages the residual clause with the constant chosen before M, m, and s.

noncomputable def Algsuperdiff.Section3.Provider.Base.baseCaseMStarStarErrorConst (d : ℕ) : ℝ

The explicit dimension-only constant in the corrected m <= m** error tail.

Equations

• Algsuperdiff.Section3.Provider.Base.baseCaseMStarStarErrorConst d = Algsuperdiff.Section3.Provider.Tail.gammaTwoAdditionConst * Algsuperdiff.Section3.Provider.Base.cutoffBaseSqrtConst d

theorem Algsuperdiff.Section3.Provider.Base.baseCaseMStarStarErrorConst_pos (d : ℕ) : 0 < baseCaseMStarStarErrorConst d

The corrected m <= m** error-tail constant is strictly positive.

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

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

theorem Algsuperdiff.Section3.Provider.Base.exists_baseCaseMStarStarErrorConst (d : ℕ) : ∃ (C2 : ℝ), 0 < C2 ∧ ∀ (M : ABKModel d), ∀ m ≤ mStarStar M, ∀ (s : { s : ℝ // s ∈ Set.Ioo 0 1 }), Probability.IsOneSidedOrlicz (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (Observable.cutoffHomogenizationError M m ⟨↑s, ⋯⟩) (C2 * (√(Disorder.cstarPlus M))⁻¹ * √M.gamma * √(baseLoss d s))

There is one positive dimension-only constant, chosen before the model and all scale parameters, that proves the corrected residual clause.