Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section3.Provider.CoarseEllipticity.UpperHsepResidualScale

UpperHsepResidualScale #

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

Uniform upper-profile hsep residual scale #

This file isolates the numerical comparison for the exact scale returned by HsepReduction at the Section 3.3 upper-profile parameters. The constants below are universal (hence, in particular, safe wherever a dimension-only constant is allowed), and the comparison is uniform in the terminal exponent sigma.

This is an internal scale-arithmetic helper.

source
noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.upperHsepResidualScale (sigma gamma : ℝ) :
ℝ

The exact amplitude returned by HsepReduction after specializing its internal exponents to the Section 3.3 upper profile.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.upperHsepResidualRate :
    ℝ

    Fixed exponential rate retained from the truncation depth floor((81 gamma)^{-1}).

    Equations
    Instances For
      source
      noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.upperHsepResidualConst :
      ℝ

      A universal amplitude for the exact upper-profile hsep residual scale.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.upperHsepResidualRate_pos :
        0 < upperHsepResidualRate
        source
        theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.upperHsepResidualConst_pos :
        0 < upperHsepResidualConst
        source
        theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.upperHsepResidualScale_pos (sigma gamma : ℝ) :
        0 < upperHsepResidualScale sigma gamma
        source
        theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.upperHsepResidualScale_le_exp {sigma E gamma : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hE : 1 ≤ E) (hgamma : 0 < gamma) :
        upperHsepResidualScale sigma gamma ≤ upperHsepResidualConst * Real.exp (-(upperHsepResidualRate * (E⁻¹ ^ 2 * gamma⁻¹)))

        The exact upper-profile hsep residual scale is bounded by one universal amplitude times a fixed-rate exponential. The constants are selected before sigma, E, and gamma, so the estimate is uniform in all three runtime parameters on the displayed window.