Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section3.Provider.Multiscale.SharpFramedLayerNamedDecomposition

SharpFramedLayerNamedDecomposition #

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

Literal named-lane decomposition of one framed sharp layer #

This file expands probeSharpFramedMeanLayerEnvelope into twelve literal nonnegative summands: the good-cell base term, five good-cell wave terms, the collar base term, and five collar wave terms. It is an algebraic inventory of the already-defined envelope. No estimate, probabilistic price, aggregation, or cutoff-observable conclusion is asserted.

The equality prevents a later consumer from silently dropping a lane.

source
noncomputable def Algsuperdiff.Section3.Provider.Multiscale.probeSharpFramedGoodBaseTerm (d n : ℕ) (p : HCPolySupport.Vec d) :
ℝ

The literal deterministic good-cell base term.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def Algsuperdiff.Section3.Provider.Multiscale.probeSharpFramedGoodWavePart {d : ℕ} (M : ABKModel d) (root : ℤ) (E b : ℝ) (k₀ n : ℕ) (i : ℤ) (p : HCPolySupport.Vec d) (Z : Cutoff.CutoffSample d → ℝ) (omega : Cutoff.CutoffSample d) :
    ℝ

    One named good-cell wave-square term, with the common frame, hsep power, mean coefficient, and layer mass retained.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def Algsuperdiff.Section3.Provider.Multiscale.probeSharpFramedCollarFactor {d : ℕ} (M : ABKModel d) (root : ℤ) (E b : ℝ) (k₀ n : ℕ) (Cgrad : ℝ) (omega : Cutoff.CutoffSample d) :
      ℝ

      The literal nonnegative collar prefactor.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def Algsuperdiff.Section3.Provider.Multiscale.probeSharpFramedCollarBaseTerm {d : ℕ} (M : ABKModel d) (root : ℤ) (E b : ℝ) (k₀ n : ℕ) (p : HCPolySupport.Vec d) (Cgrad : ℝ) (omega : Cutoff.CutoffSample d) :
        ℝ

        The literal collar base term.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def Algsuperdiff.Section3.Provider.Multiscale.probeSharpFramedCollarWavePart {d : ℕ} (M : ABKModel d) (root : ℤ) (E b : ℝ) (k₀ n : ℕ) (i : ℤ) (p : HCPolySupport.Vec d) (Cgrad : ℝ) (Z : Cutoff.CutoffSample d → ℝ) (omega : Cutoff.CutoffSample d) :
          ℝ

          One named collar wave-square term, with the literal collar mass and common framed multiplier retained.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def Algsuperdiff.Section3.Provider.Multiscale.probeSharpFramedLayerNamedSum {d : ℕ} (M : ABKModel d) (root : ℤ) (E b : ℝ) (k₀ n : ℕ) (i L : ℤ) (omega : Cutoff.CutoffSample d) (p : HCPolySupport.Vec d) (Cgrad : ℝ) :
            ℝ

            The complete twelve-lane named sum for one framed layer.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem Algsuperdiff.Section3.Provider.Multiscale.probeSharpFramedGoodWavePart_nonneg {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) (root : ℤ) (E b : ℝ) (k₀ n : ℕ) (i : ℤ) (p : HCPolySupport.Vec d) {Z : Cutoff.CutoffSample d → ℝ} (hZ : ∀ (omega : Cutoff.CutoffSample d), 0 ≤ Z omega) (omega : Cutoff.CutoffSample d) :
              0 ≤ probeSharpFramedGoodWavePart M root E b k₀ n i p Z omega
              source
              theorem Algsuperdiff.Section3.Provider.Multiscale.probeSharpFramedCollarFactor_nonneg {d : ℕ} (M : ABKModel d) (root : ℤ) (E b : ℝ) (k₀ n : ℕ) (Cgrad : ℝ) (omega : Cutoff.CutoffSample d) :
              0 ≤ probeSharpFramedCollarFactor M root E b k₀ n Cgrad omega
              source
              theorem Algsuperdiff.Section3.Provider.Multiscale.probeSharpFramedCollarBaseTerm_nonneg {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) (root : ℤ) (E b : ℝ) (k₀ n : ℕ) (p : HCPolySupport.Vec d) (Cgrad : ℝ) (omega : Cutoff.CutoffSample d) :
              0 ≤ probeSharpFramedCollarBaseTerm M root E b k₀ n p Cgrad omega
              source
              theorem Algsuperdiff.Section3.Provider.Multiscale.probeSharpFramedCollarWavePart_nonneg {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) (root : ℤ) (E b : ℝ) (k₀ n : ℕ) (i : ℤ) (p : HCPolySupport.Vec d) (Cgrad : ℝ) {Z : Cutoff.CutoffSample d → ℝ} (hZ : ∀ (omega : Cutoff.CutoffSample d), 0 ≤ Z omega) (omega : Cutoff.CutoffSample d) :
              0 ≤ probeSharpFramedCollarWavePart M root E b k₀ n i p Cgrad Z omega
              source
              theorem Algsuperdiff.Section3.Provider.Multiscale.probeSharpFramedMeanLayerEnvelope_eq_namedSum {d : ℕ} (M : ABKModel d) (root : ℤ) (E b : ℝ) (k₀ n : ℕ) (i L : ℤ) (omega : Cutoff.CutoffSample d) (p : HCPolySupport.Vec d) (Cgrad : ℝ) :
              probeSharpFramedMeanLayerEnvelope M root E b k₀ n i L omega p Cgrad = probeSharpFramedLayerNamedSum M root E b k₀ n i L omega p Cgrad

              Exact expansion of the framed sharp mean-layer envelope into the twelve named lanes. This is an equality of existing algebraic expressions, not an estimate of any lane.