UpperAfterBandRareProfile

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

Rare after-band Whitney-layer profile

This module prices and sums the explicit rare witness from SharpFramedAfterBandOrlicz at one strict descendant. It keeps the literal exceptional exponent Gamma_((1 - sigma) / 3), first bounds the complete gammaProductConst * residualScale * baseScale amplitude, and then applies the countable Orlicz triangle inequality over the Whitney-layer index.

The output still precedes multiplication by probeMeanGoodWaveConst M * vecNormSq p, the triadic grid/depth maximum, and the coarse-scale weights. The separate root row and every other wave/base/collar lane are absent.

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

A dimension-only coefficient for the exponentially small rare after-band layer. The leading 1 makes positivity unconditional.

Equations

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

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

The dimension-only coefficient after the Whitney-layer sum.

Equations

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

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

A summable deterministic majorant for one exact rare-lane scale.

Equations

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

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

The additional product of the hsep residual with a Gamma_1 factor has a universal product constant on the full terminal sigma window.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpAfterBandRareLayerConst_pos (d : ℕ) : 0 < probeSharpAfterBandRareLayerConst d

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpAfterBandRareSumConst_pos (d : ℕ) : 0 < probeSharpAfterBandRareSumConst d

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpAfterBandRareGoodMassScale_le_layerBound {d : ℕ} (M : ABKModel d) {m : ℤ} {k : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k)) {E sigma : ℝ} (hE : 1 ≤ E) (hgamma20 : M.gamma ≤ 1 / 20) (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (n : ℕ) : Multiscale.probeSharpAfterBandRareGoodMassScale M R.scale m E sigma k n ≤ probeSharpAfterBandRareGoodMassLayerBound M E k n

The complete exact rare scale of one strict-descendant Whitney layer is bounded by the fixed geometric layer profile times the verified exponential residual.

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.tsum_probeSharpAfterBandRareGoodMassLayerBound_eq {d : ℕ} (M : ABKModel d) (E : ℝ) (k : ℕ) : ∑' (n : ℕ), probeSharpAfterBandRareGoodMassLayerBound M E k n = probeSharpAfterBandRareSumConst d * (min 1 (M.gamma * ↑(k + 1)) * 3 ^ (M.gamma * ↑(k + 1))) * Real.exp (-(upperHsepResidualRate * (E⁻¹ ^ 2 * M.gamma⁻¹)))

Exact evaluation of the summed deterministic rare-layer majorant.