Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section3.Provider.CoarseEllipticity.UpperCollarBandMeanTunedProfile

UpperCollarBandMeanTunedProfile #

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

Collar band-mean profile at the source-compatible tuned depth #

This file repeats only the collar band-mean layer estimate whose earlier specialization used coefficient 1. Its integer depth is now the internal choice collarBandMeanDepth, with no new caller premise. The exact collar carrier and all generic cap/mass interpolation lemmas are reused unchanged.

These declarations are internal Provider results and make no source-node or development-status claim.

source
noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpCollarBandMeanTunedOuter {d : ℕ} (M : ABKModel d) (E : ℝ) (j : Fin d) :
ℝ

The exact outer band coefficient at the internally selected depth.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpCollarBandMeanTunedLayerScale {d : ℕ} (M : ABKModel d) (E : ℝ) (n : ℕ) :
    ℝ

    The deterministic Whitney scale at the internally selected depth.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpCollarBandMeanTunedOuter_nonneg {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) (E : ℝ) (j : Fin d) :
      0 ≤ probeSharpCollarBandMeanTunedOuter M E j
      source
      theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpCollarBandMeanTunedLayerScale_nonneg {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) (E : ℝ) (n : ℕ) :
      0 ≤ probeSharpCollarBandMeanTunedLayerScale M E n
      source
      theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpCollarBandMeanTunedOuter_le_const {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) {E : ℝ} (hE : 1 ≤ E) (hcstarE : (Disorder.cstar M)⁻¹ ≤ E) (hEgamma : E ≤ M.gamma ^ (-(1 / 5))) (j : Fin d) :
      probeSharpCollarBandMeanTunedOuter M E j ≤ probeSharpCollarBandMeanOuterConst d

      The deterministic band mean remains dimension-bounded for the smaller source-compatible coefficient.

      source
      theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpCollarBandMeanLayerCore_le_retainFrame {d : ℕ} (M : ABKModel d) {m : ℤ} {k : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k)) (E : ℝ) (k₀ n : ℕ) (omega : Cutoff.CutoffSample d) :
      probeSharpCollarBandMeanLayerCore M R.scale E k₀ n (m - 1) (Affine.superposedGradConst d) omega ≤ 4 * Affine.superposedGradConst d ^ 2 * probeSharpCollarBandMeanCapQuarter M E k₀ * probeSharpCollarBandMeanMassQuarterConst d * 3 ^ (2 * bfaProfileB * ↑k₀) * 3 ^ (1 / 16) * whitneyDecayRatio ^ n * Multiscale.slstarPowerTerm M R.scale E bfaProfileB M.gamma omega * 3 ^ (M.gamma * -(↑k + ↑n + ↑(Multiscale.bfaAfterBandLayerCeil n) + ↑k₀))

      The collar estimate with its full nonnegative frame decay retained.

      source
      theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpCollarBandMeanLayerCore_le_atDepth {d : ℕ} (M : ABKModel d) {m : ℤ} {k : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k)) (E : ℝ) (k₀ n : ℕ) (omega : Cutoff.CutoffSample d) :
      probeSharpCollarBandMeanLayerCore M R.scale E k₀ n (m - 1) (Affine.superposedGradConst d) omega ≤ 4 * Affine.superposedGradConst d ^ 2 * probeSharpCollarBandMeanCapQuarter M E k₀ * probeSharpCollarBandMeanMassQuarterConst d * 3 ^ (2 * bfaProfileB * ↑k₀) * 3 ^ (1 / 16) * Multiscale.slstarPowerTerm M R.scale E bfaProfileB M.gamma omega * whitneyDecayRatio ^ n

      The collar/frame core bound at an arbitrary deterministic integer depth. The proof is the same source algebra as the coefficient-one specialization; no size property of k₀ is used here.

      source
      theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedCollarWavePart_bandMeanTuned_le {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) {m : ℤ} {k : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k)) {E : ℝ} (hE : 1 ≤ E) (hcstarE : (Disorder.cstar M)⁻¹ ≤ E) (hEgamma : E ≤ M.gamma ^ (-(1 / 5))) (n : ℕ) (j : Fin d) (omega : Cutoff.CutoffSample d) :
      Multiscale.probeSharpFramedCollarWavePart M R.scale E bfaProfileB (collarBandMeanDepth M E) n (m - 1) (HCPolySupport.basisVec j) (Affine.superposedGradConst d) (fun (_eta : Cutoff.CutoffSample d) => waveBandMean (probeDeepBandMeanAmplitude d) M.gamma (collarBandMeanDepth M E) ^ 2) omega ≤ probeSharpCollarBandMeanTunedLayerScale M E n * Multiscale.slstarPowerTerm M R.scale E bfaProfileB M.gamma omega

      The literal ninth named summand at the source-compatible depth.

      source
      theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.summable_probeSharpCollarBandMeanTunedLayerScale {d : ℕ} (M : ABKModel d) (E : ℝ) :
      Summable fun (n : ℕ) => probeSharpCollarBandMeanTunedLayerScale M E n