WaveTailProfile

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

A fixed-profile wave-tail estimate

This internal analytic provider collapses the explicit geometric series in waveTailGainScale at the manuscript's fixed b = 2⁻²⁰ and sigma₂ = 2 / sigma. It proves a dimension-only C(d) sigma⁻¹ 3^{-(d/8)k₀} scale used by a proposed wave endpoint.

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.waveTailProfileConst (d : ℕ) : ℝ

A fully explicit dimensional constant for the fixed b = 2⁻²⁰ wave tail.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Multiscale.waveTailGainScale_profile_le {d : ℕ} (M : ABKModel d) {sigma : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) {lout ell : ℤ} {k₀ k : ℕ} (hgap : lout - ell = ↑(Whitney.whitneyScaleSeq CoarseEllipticity.bfaProfileB 0 k₀ k)) : waveTailGainScale d CoarseEllipticity.bfaProfileB sigma (2 / sigma) lout ell ≤ waveTailProfileConst d * sigma⁻¹ * 3 ^ (-(↑d / 8) * ↑k₀)

At the exact deterministic Whitney gap, the explicit wave-tail series is bounded by the manuscript's C(d) sigma⁻¹ 3^{-(d/8)k₀} scale.