Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section3.Provider.CoarseEllipticity.UpperGoodBaseConsumption

UpperGoodBaseConsumption #

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

Exact root and strict-depth consumption of the framed good-base lane #

The good-cell base term is deterministic and independent of the root, descendant, cutoff sample, and observation frame. This file consumes that literal named summand through its Whitney-layer sum, finite coordinate trace, finite descendant maximum, separate depth-zero weight, and positive-depth grid series. The full root-plus-depth contribution is bounded by an explicit dimension-only constant.

No wave term, collar term, complete envelope, cutoff observable, or source-facing theorem is treated here.

source
noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedGoodBaseCoordinateENNRealLane (d : ℕ) (j : Fin d) :
ENNReal

The literal named good-base Whitney sum for one basis coordinate.

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

    The finite-coordinate trace of the literal named good-base lane.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedGoodBaseTerm_basisVec_eq (d n : ℕ) (j : Fin d) :
      Multiscale.probeSharpFramedGoodBaseTerm d n (HCPolySupport.basisVec j) = Multiscale.probeSharpGoodBaseLayer d n j

      The named framed good-base term is exactly the verified good-base layer.

      source
      theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedGoodBaseCoordinateENNRealLane_eq {d : ℕ} (hd : 2 ≤ d) (j : Fin d) :
      probeSharpFramedGoodBaseCoordinateENNRealLane d j = ENNReal.ofReal (Multiscale.probeSharpGoodBaseCoordinateConst d)

      The literal coordinate sum equals the verified explicit real coordinate constant.

      source
      theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedGoodBaseTraceENNRealLane_eq {d : ℕ} (hd : 2 ≤ d) :
      probeSharpFramedGoodBaseTraceENNRealLane d = ENNReal.ofReal (Multiscale.probeSharpGoodBaseConst d)

      The literal finite-coordinate trace equals the verified explicit dimension-only trace constant.