UpperAfterBandRareAbsorption

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

Frozen-scale absorption for the rare after-band lane

This module proves the terminal numerical absorption for foldedBlockPole at the exact rare after-band coordinate base scale. The output threshold is explicit and depends only on the dimension.

The theorem here does not perform the actual weighted depth sum or root fold, nor does it connect the resulting numerical envelope to the complete random variable. It also does not assemble the other upper lanes, the complete observable, the all-exponent result, or the frozen theorem, and it carries no source-node or closure status.

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.upperAfterBandRareTriangleConst : ℝ

A uniform triangle constant for the frozen upper exponent (1 - sigma) / 3, whose inverse is at most six.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.upperAfterBandRareTriangleConst = 4 * 117649 ^ 12

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

A uniform grid-net constant for the frozen upper exponent.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.upperAfterBandRareGridNetConst d = (3 * ↑d * Real.log 3) ^ 6

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

The dimension-only part of probeMeanGoodWaveConst.

Equations

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.upperProfileTargetSigma_one_six_le {sigma : ℝ} (hsigma : sigma ≤ 1 / 2) : 1 / 6 ≤ upperProfileTargetSigma sigma

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.gammaTriangleConst_upperProfileTarget_le {sigma : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) : HCPolySupport.IndependentSums.gammaTriangleConst (upperProfileTargetSigma sigma) ≤ upperAfterBandRareTriangleConst

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.gridNetConst_upperProfileTarget_le {d : ℕ} (hd : 2 ≤ d) {sigma : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) : gridNetConst d (upperProfileTargetSigma sigma) ≤ upperAfterBandRareGridNetConst d

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeMeanGoodWaveConst_eq_dimension_mul_cstarInv {d : ℕ} (M : ABKModel d) : Multiscale.probeMeanGoodWaveConst M = probeMeanGoodWaveDimensionConst d * (Disorder.cstar M)⁻¹