Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section3.Provider.Multiscale.SharpFramedAfterBandLayerProfile

SharpFramedAfterBandLayerProfile #

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

Whitney-layer profile for the saturated after-band term #

This file prices the deterministic 2 summand supplied by the pointwise hsep reduction for the after-band square. The carrier below includes the actual sharp five-term coefficient, the good-layer mass envelope, the exact short-gap saturation, and the tuned band depth. The complementary random Orlicz summand is deliberately not included here. This is the normalized inner good-mass branch before multiplication by probeMeanGoodWaveConst M * vecNormSq p; consequently it is not the complete Whitney-layer mean contribution. It omits every other lane.

Scalar layer arithmetic #

source
noncomputable def Algsuperdiff.Section3.Provider.Multiscale.bfaAfterBandLayerCeil (n : ℕ) :
ℕ

The ceiling appearing in the fixed-slope Whitney layer.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Algsuperdiff.Section3.Provider.Multiscale.bfaAfterBandLayerCeil_le (n : ℕ) :
    bfaAfterBandLayerCeil n ≤ n

    At the fixed profile slope, the additional ceiling is at most the layer index itself.

    source
    theorem Algsuperdiff.Section3.Provider.Multiscale.min_one_mul_le_mul_min_one {a x : ℝ} (ha : 1 ≤ a) :
    min 1 (a * x) ≤ a * min 1 x

    Scaling the argument of min 1 by a factor at least one costs at most that factor outside the minimum.

    source
    theorem Algsuperdiff.Section3.Provider.Multiscale.bfaAfterBandSaturation_le {gamma : ℝ} (hgamma : 0 ≤ gamma) (k n : ℕ) :
    min 1 (gamma * (1 + ↑k + ↑n + ↑(bfaAfterBandLayerCeil n))) ≤ 2 * ↑(n + 1) * min 1 (gamma * ↑(k + 1))

    The saturated gap at layer n costs only a linear (n+1) factor relative to the target depth profile.

    source
    theorem Algsuperdiff.Section3.Provider.Multiscale.gamma_mul_waveBandDepth_one_le {E gamma : ℝ} (hE : 1 ≤ E) (hgamma : 0 < gamma) (hgamma20 : gamma ≤ 1 / 20) :
    gamma * ↑(CoarseEllipticity.waveBandDepth 1 E gamma) ≤ 21 / 20

    The tuned band depth costs at most 21/20 in its gamma-weighted exponent when E ≥ 1 and gamma ≤ 1/20.

    source
    theorem Algsuperdiff.Section3.Provider.Multiscale.sqrt_probeSharpLayerMassEnvelope_eq (d n : ℕ) :
    √(probeSharpLayerMassEnvelope d n) = √(6 * ↑d) * 3 ^ (-↑n / 2)

    Exact square-root form of the good Whitney-layer mass envelope.

    source
    theorem Algsuperdiff.Section3.Provider.Multiscale.sqrt_mass_mul_afterBandGrowth_le {E gamma : ℝ} (hE : 1 ≤ E) (hgamma : 0 < gamma) (hgamma20 : gamma ≤ 1 / 20) (d n : ℕ) :
    √(probeSharpLayerMassEnvelope d n) * 3 ^ (gamma * (1 + ↑n + ↑(bfaAfterBandLayerCeil n) + ↑(CoarseEllipticity.waveBandDepth 1 E gamma))) ≤ √(6 * ↑d) * 3 ^ (11 / 10) * CoarseEllipticity.whitneyDecayRatio ^ n

    The good-mass square root absorbs all layer growth and the tuned band depth, leaving the fixed geometric ratio.

    The concrete deterministic branch #

    source
    noncomputable def Algsuperdiff.Section3.Provider.Multiscale.probeSharpAfterBandOrdinaryGoodMassLayer {d : ℕ} (M : ABKModel d) (E : ℝ) (k n : ℕ) :
    ℝ

    The literal deterministic 2 branch of the framed after-band square after multiplication by the sharp five-term coefficient and the good-layer mass square root. It is the normalized inner branch before multiplication by probeMeanGoodWaveConst M * vecNormSq p, not the complete layer.

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

      Dimension-only coefficient in the pointwise Whitney-layer profile.

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

        Dimension-only coefficient after summing the normalized inner branch over all Whitney layers.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Algsuperdiff.Section3.Provider.Multiscale.probeSharpAfterBandOrdinaryGoodMassLayer_nonneg {d : ℕ} (M : ABKModel d) (E : ℝ) (k n : ℕ) :
          0 ≤ probeSharpAfterBandOrdinaryGoodMassLayer M E k n
          source
          theorem Algsuperdiff.Section3.Provider.Multiscale.probeSharpAfterBandOrdinaryLayerConst_nonneg (d : ℕ) :
          0 ≤ probeSharpAfterBandOrdinaryLayerConst d
          source
          theorem Algsuperdiff.Section3.Provider.Multiscale.probeSharpAfterBandOrdinaryGoodMassLayer_le {d : ℕ} (M : ABKModel d) {E : ℝ} (hE : 1 ≤ E) (hgamma20 : M.gamma ≤ 1 / 20) (k n : ℕ) :
          probeSharpAfterBandOrdinaryGoodMassLayer M E k n ≤ probeSharpAfterBandOrdinaryLayerConst d * (↑(n + 1) * CoarseEllipticity.whitneyDecayRatio ^ n) * (min 1 (M.gamma * ↑(k + 1)) * 3 ^ (M.gamma * ↑(k + 1)))

          One deterministic after-band layer has the target saturated depth profile times the fixed summable Whitney weight.

          source
          theorem Algsuperdiff.Section3.Provider.Multiscale.tsum_probeSharpAfterBandOrdinaryGoodMassLayer_le {d : ℕ} (M : ABKModel d) {E : ℝ} (hE : 1 ≤ E) (hgamma20 : M.gamma ≤ 1 / 20) (k : ℕ) :
          ∑' (n : ℕ), probeSharpAfterBandOrdinaryGoodMassLayer M E k n ≤ probeSharpAfterBandOrdinarySumConst d * (min 1 (M.gamma * ↑(k + 1)) * 3 ^ (M.gamma * ↑(k + 1)))

          The sum of the normalized deterministic inner branches retains the exact saturated depth profile. The outer mean coefficient and vector norm are not part of either side.