UpperWaveTailRareProfile

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

Rare good-mass wave-tail profile

This file prices the rare witness in the exact split of the framed random-depth wave-tail term at one strict descendant. It retains the target exceptional exponent, the complete hsep-product constant, the squared sigma pole, and the tuned exponential factor. The two exponential factors in the product scale are weakened internally to one factor.

The outer mean/vector coefficient, translation to the descendant sample, grid/depth aggregation, root row, other named lanes, and cutoff observable are not treated here. These declarations are conditional internal Provider A for the normalized rare wave-tail lane only.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.gammaProductConst_upperProfileHsepTau_tailSigma_le_sixty_four {sigma : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) : HCPolySupport.Book.Ch04.gammaProductConst (upperProfileHsepTau sigma) (upperProfileTailSigma sigma) ≤ 64

The product constant for the hsep residual and profile-tail exponents is uniformly bounded by 64 on the terminal profile window.

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

A dimension-only coefficient for one rare wave-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.probeSharpWaveTailRareSumConst (d : ℕ) : ℝ

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

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpWaveTailRareSumConst d = Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpWaveTailRareLayerConst d * (1 - 3 ^ (-(1 / 2)))⁻¹

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpWaveTailRareLayerConst_pos (d : ℕ) : 0 < probeSharpWaveTailRareLayerConst d

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpWaveTailRareSumConst_pos (d : ℕ) : 0 < probeSharpWaveTailRareSumConst d