UpperDeepBandTailRareProfile

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

Rare centered deep-band-tail Whitney-layer profile

This file prices and sums the explicit rare witness of the framed centered deep-band-tail good-mass lane. It retains the literal exceptional exponent Gamma_((1 - sigma) / 3), bounds the complete hsep product scale, and applies the countable Orlicz triangle inequality over Whitney layers.

The output still precedes multiplication by probeMeanGoodWaveConst M * vecNormSq p, coordinate tracing, grid/depth aggregation, and the cutoff observable. The root row, every other good lane, and every collar lane are absent.

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpDeepBandTailRareLayerConst (d : ℕ) : ℝ

A dimension-only coefficient for one rare centered-tail layer. The leading 1 makes strict positivity unconditional.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpDeepBandTailRareSumConst (d : ℕ) : ℝ

The dimension-only coefficient after summing the rare centered-tail layer majorant.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpDeepBandTailRareGoodMassLayerBound {d : ℕ} (M : ABKModel d) (E : ℝ) (n : ℕ) : ℝ

A summable deterministic majorant for one exact rare centered-tail scale.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpDeepBandTailRareLayerConst_pos (d : ℕ) : 0 < probeSharpDeepBandTailRareLayerConst d

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpDeepBandTailRareSumConst_pos (d : ℕ) : 0 < probeSharpDeepBandTailRareSumConst d

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpDeepBandTailRareGoodMassLayerBound_pos {d : ℕ} (M : ABKModel d) (E : ℝ) (n : ℕ) : 0 < probeSharpDeepBandTailRareGoodMassLayerBound M E n

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.tsum_probeSharpDeepBandTailRareGoodMassLayerBound_eq {d : ℕ} (M : ABKModel d) (E : ℝ) : ∑' (n : ℕ), probeSharpDeepBandTailRareGoodMassLayerBound M E n = probeSharpDeepBandTailRareSumConst d * M.gamma * Real.exp (-(upperHsepResidualRate * (E⁻¹ ^ 2 * M.gamma⁻¹)))

Exact evaluation of the summed deterministic rare-layer majorant.