Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section3.Provider.Multiscale.SharpFramedDeepBandTailProfile

SharpFramedDeepBandTailProfile #

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

Ordinary profile of the centered tuned deep-band tail #

This file computes the exact deterministic scale of the squared centered deep-band tail after removing the framed hsep factor at a strict descendant. The corresponding deterministic 2 branch is summed over Whitney layers and shown to be bounded by a dimension-only constant times gamma.

The actual random hsep split is not performed here, and no random variable is identified with this numerical carrier. The outer probeMeanGoodWaveConst M * vecNormSq p, the complementary residual branch, all other good/collar terms, depth/grid aggregation, and the cutoff observable are absent.

source
noncomputable def Algsuperdiff.Section3.Provider.Multiscale.probeSharpDeepBandTailAmplitude (d : ℕ) :
ℝ

The dimension-only coefficient in the closed form of the wave-gauged centered deep-band scale.

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

    Dimension-only coefficient for the pointwise geometric layer profile.

    Equations
    Instances For
      source
      theorem Algsuperdiff.Section3.Provider.Multiscale.probeDeepBandGaugedFluct_eq_closed {d : ℕ} (M : ABKModel d) (ell : ℤ) (k₀ g₀ : ℕ) :
      CoarseEllipticity.probeDeepBandGaugedFluct M ell k₀ g₀ = probeSharpDeepBandTailAmplitude d * √M.gamma * CoarseEllipticity.probeBandUnitGain d ^ g₀ * 3 ^ (M.gamma * ↑k₀)

      Exact cancellation of the layer anchor in the wave-gauged centered-tail scale.

      source
      theorem Algsuperdiff.Section3.Provider.Multiscale.probeDeepBandGaugedFluct_sq_eq_closed {d : ℕ} (M : ABKModel d) (ell : ℤ) (k₀ g₀ : ℕ) :
      CoarseEllipticity.probeDeepBandGaugedFluct M ell k₀ g₀ ^ 2 = probeSharpDeepBandTailAmplitude d ^ 2 * M.gamma * (CoarseEllipticity.probeBandUnitGain d ^ g₀) ^ 2 * 3 ^ (2 * (M.gamma * ↑k₀))

      Squared closed form of the centered deep-band scale.

      source
      theorem Algsuperdiff.Section3.Provider.Multiscale.probeSharpDeepBandTailOrdinaryLayerConst_nonneg (d : ℕ) :
      0 ≤ probeSharpDeepBandTailOrdinaryLayerConst d