Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section3.Provider.Multiscale.WaveSharpUpper

WaveSharpUpper #

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

A macroscopic cube-averaged wave term #

This internal analytic provider keeps the cube-averaged L⁴ carrier for the macroscopic increment. It obtains the sqrt gamma * sqrt (L-ell) * 3^(gamma*(L-ell)) Gamma₂ scale directly from the proved increment estimate, with no translated-cube maximum and therefore no grid penalty.

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

A dimension-only constant for the macroscopic L⁴ term.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def Algsuperdiff.Section3.Provider.Multiscale.waveSharpUpperTerm {d : ℕ} (M : ABKModel d) (lout ell L : ℤ) (omega : Cutoff.CutoffSample d) :
    ℝ

    The macroscopic L⁴ wave term, without a translated-cube maximum.

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