Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section3.Provider.Multiscale.SharpFramedGoodBaseProfile

SharpFramedGoodBaseProfile #

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

Deterministic good-mass base profile in the framed layer envelope #

The good-cell part of probeSharpFramedMeanLayerEnvelope contains the deterministic summand probeMeanGoodBaseConst d * vecNormSq p * probeSharpLayerMassEnvelope d n. This file sums that literal term over the Whitney-layer index and over the coordinate basis. The resulting bound is dimension-only.

No collar mass, wave term, random factor, depth aggregation, or cutoff block carrier is treated here.

source
noncomputable def Algsuperdiff.Section3.Provider.Multiscale.probeSharpGoodBaseLayer (d n : ℕ) (j : Fin d) :
ℝ

The literal deterministic good-mass base summand for one layer and one coordinate.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def Algsuperdiff.Section3.Provider.Multiscale.probeSharpGoodBaseCoordinateConst (d : ℕ) :
    ℝ

    The dimension-only sum of one coordinate's deterministic good-mass base layers.

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

      The dimension-only sum after the finite coordinate trace.

      Equations
      Instances For
        source
        theorem Algsuperdiff.Section3.Provider.Multiscale.probeSharpGoodBaseLayer_nonneg {d : ℕ} (hd : 2 ≤ d) (n : ℕ) (j : Fin d) :
        0 ≤ probeSharpGoodBaseLayer d n j
        source
        theorem Algsuperdiff.Section3.Provider.Multiscale.probeSharpGoodBaseCoordinateConst_nonneg {d : ℕ} (hd : 2 ≤ d) :
        0 ≤ probeSharpGoodBaseCoordinateConst d
        source
        theorem Algsuperdiff.Section3.Provider.Multiscale.probeSharpGoodBaseConst_nonneg {d : ℕ} (hd : 2 ≤ d) :
        0 ≤ probeSharpGoodBaseConst d
        source
        theorem Algsuperdiff.Section3.Provider.Multiscale.tsum_probeSharpGoodBaseLayer_eq (d : ℕ) (j : Fin d) :
        ∑' (n : ℕ), probeSharpGoodBaseLayer d n j = probeSharpGoodBaseCoordinateConst d

        One coordinate's deterministic good-mass base layers sum to the explicit dimension-only constant.