SharpFramedDeepBandTailOrlicz

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

Orlicz split for the framed centered deep-band tail

This file applies the already-verified upper-profile separation split to the literal squared centered deep-band tail in one good-cell Whitney lane. The unframed square uses the exact Gamma_1 certificate supplied by the grouped deep-band estimate, and its deterministic 2 witness is identified with the separately computed ordinary layer profile.

Only the normalized inner good-mass centered-tail lane is treated. The outer probeMeanGoodWaveConst M * vecNormSq p, the root row, good base, band mean, after-band and wave-tail lanes, every collar lane, layer/grid/depth aggregation, and the cutoff observable are absent.

Literal carriers

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.probeSharpDeepBandTailGoodMassCoeff (d n : ℕ) : ℝ

The common sharp coefficient and good-layer mass square root for the centered deep-band square.

Equations

• Algsuperdiff.Section3.Provider.Multiscale.probeSharpDeepBandTailGoodMassCoeff d n = 5 * ↑d ^ 2 * √(Algsuperdiff.Section3.Provider.Multiscale.probeSharpLayerMassEnvelope d n)

theorem Algsuperdiff.Section3.Provider.Multiscale.probeSharpDeepBandTailGoodMassCoeff_nonneg (d n : ℕ) : 0 ≤ probeSharpDeepBandTailGoodMassCoeff d n

Exact descendant identity and unframed certificate

Explicit ordinary and rare lanes