Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section3.Provider.CoarseEllipticity.UpperWaveTailBoundedProfile

UpperWaveTailBoundedProfile #

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

Bounded good-mass wave-tail profile #

This file prices the literal bounded witness from the framed random-depth wave-tail split at one strict descendant. It compares the actual Whitney layer anchor with the tuned band gap, retains the squared wave-tail scale, and sums the resulting geometric layer profile.

The outer mean/vector coefficient, the rare witness, root row, collar lanes, grid/depth aggregation, other named lanes, and cutoff observable are not treated here. The declarations below are conditional internal A for this single normalized lane.

source
noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpWaveTailBaseLayerConst (d : ℕ) :
ℝ

Dimension-only coefficient for the unframed bounded wave-tail layer.

Equations
Instances For
    source
    noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpWaveTailBoundedLayerConst (d : ℕ) :
    ℝ

    Dimension-only coefficient after inserting the exact bounded witness factor 2.

    Equations
    Instances For
      source
      noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpWaveTailBoundedSumConst (d : ℕ) :
      ℝ

      Dimension-only coefficient after the Whitney-layer sum.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpWaveTailBaseLayerConst_pos {d : ℕ} (hd : 2 ≤ d) :
        0 < probeSharpWaveTailBaseLayerConst d
        source
        theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpWaveTailBoundedLayerConst_pos {d : ℕ} (hd : 2 ≤ d) :
        0 < probeSharpWaveTailBoundedLayerConst d
        source
        theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpWaveTailBoundedSumConst_pos {d : ℕ} (hd : 2 ≤ d) :
        0 < probeSharpWaveTailBoundedSumConst d

        The actual anchor and tuned-depth decay #

        Layer pricing and summation #