MultiscaleAbsorptionArith

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

Provider: the scalar absorption arithmetic of p.multiscale.estimate

Why this file exists

It is a statement-preserving motion and nothing else: sections 4, 5 and 6 of that module -- the three scale bridges of the non-lane terms, the bad lane's two amplitudes, and the deterministic remainder -- were moved here with their section headers, their docstrings, their statements and their proof text unchanged. The original section numbers 4, 5, 6 are kept precisely so that every cross-reference in either module's header still points where it did.

Exactly two mechanical changes were forced by the motion, at no mathematical cost:

1. each moved declaration is protected theorem here where it was private theorem there (12 declarations); and
2. the ten call sites inside this file that consume a sibling of this file carry the MultiscaleAbsorptionArith. qualifier, because a protected name is not in scope under its own short form.

No statement was altered, no lemma was dropped, no lemma was added, and no proof was re-golfed.

What is here

Twelve real-scalar inequalities, all model-free: they mention no ABKModel, no measure and no random variable, only real parameters (eps, Cms, E, cgamma, s, cstar^{-1}, and the amplitude constants).

• Section 4 -- polyTerm_le_ordinaryScale, expTerm_le_ordinaryScale, expTerm_le_rareScale: the three scale bridges carrying a display term into the ordinary scale s^{-2} eps^2 E^2 cgamma or the rare scale s^{-4} eps^2 exp(-2 E^{-3} cgamma^{-1}), on top of the Core module's absorb_window_poly, absorb_window_exp and absorb_window_exp_rare.
• Section 5 -- badProfile_le, badRemainder_le, badOrdinarySum_le, badOrdinaryAmplitude_le, badRareAmplitude_le: the bad lane's Gamma_1 and Gamma_{2/7} amplitudes, absorbed.
• Section 6 -- remainderGap_le, remainderScale_le, remainderLog_le, remainderTerm_le: the three summands of the deterministic remainder and their sum, absorbed into the ordinary normal form.

Four of the twelve are consumed by the parent module (inside the proof of exists_absorbed_envelope): polyTerm_le_ordinaryScale, badOrdinaryAmplitude_le, badRareAmplitude_le and remainderTerm_le. The other eight are consumed only here.

Scope

protected implementation support for one sibling module, NOT source-facing. Every declaration is a proved local helper over real scalars.

4. The three scale bridges of the non-lane terms

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.MultiscaleAbsorptionArith.polyTerm_le_ordinaryScale {cstarInv eps Cms E gam s Q p K : ℝ} (hQ : 0 ≤ Q) (hcs : 0 ≤ cstarInv) (heps0 : 0 < eps) (heps1 : eps ≤ 1) (hCms : 2 + p ≤ Cms) (hQE : Q ≤ K * E) (hwin : cstarInv * eps ^ (-Cms) ≤ E) (hgam : 0 ≤ gam) (hs : 0 < s) : Q * cstarInv * eps ^ (-p) * gam * s⁻¹ ^ 2 ≤ K * (s⁻¹ ^ 2 * (eps ^ 2 * E ^ 2 * gam))

A polynomial term of the display, in the ordinary normal form.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.MultiscaleAbsorptionArith.expTerm_le_ordinaryScale {eps Cms E gam s a Q K : ℝ} (hQ : 0 ≤ Q) (ha : 0 < a) (hE : 0 < E) (hgam : 0 < gam) (heps0 : 0 < eps) (heps1 : eps ≤ 1) (hgammaE : gam ≤ E⁻¹ ^ 10) (hCms : 2 ≤ 8 * Cms) (hfloor : 2 / 3 * eps ^ (-Cms) ≤ E) (hK : 2 * Q * a⁻¹ ^ 2 * (3 / 2) ^ 8 ≤ K) (hs : 0 < s) : Q * Real.exp (-(a * E⁻¹ ^ 2 * gam⁻¹)) * s⁻¹ ^ 2 ≤ K * (s⁻¹ ^ 2 * (eps ^ 2 * E ^ 2 * gam))

An exponentially small term of the display, in the ordinary normal form.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.MultiscaleAbsorptionArith.expTerm_le_rareScale {eps Cms E gam s a Q K X : ℝ} (hQ : 0 ≤ Q) (ha : 0 < a) (hE : 0 < E) (hgam : 0 < gam) (heps0 : 0 < eps) (heps1 : eps ≤ 1) (hgammaE : gam ≤ E⁻¹ ^ 10) (hEa : 4 / a ≤ E) (hCms : 2 ≤ 16 * Cms) (hfloor : 2 / 3 * eps ^ (-Cms) ≤ E) (hK : 8 * Q * a⁻¹ ^ 2 * (3 / 2) ^ 16 ≤ K) (hs : 0 < s) (hs1 : s ≤ 1) (hX : X = 2 * E⁻¹ ^ 3 * gam⁻¹) (hK0 : 0 ≤ K) : Q * Real.exp (-(a * E⁻¹ ^ 2 * gam⁻¹)) ≤ K * (s⁻¹ ^ 4 * (eps ^ 2 * Real.exp (-X)))

An exponentially small term of the display, in the rare normal form.

5. The bad lane's two amplitudes

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.MultiscaleAbsorptionArith.badProfile_le {Ccg0 gam s : ℝ} (hCcg0 : 0 < Ccg0) (hgam0 : 0 < gam) (hgam1 : gam ≤ 1) (hs8 : 8 * gam ≤ s) : 0 ≤ 8 * Ccg0 + 8 * 3 ^ gam * lowerEllipticityProfile Ccg0 gam (s / 4) Tail.exponentTwo ∧ 8 * Ccg0 + 8 * 3 ^ gam * lowerEllipticityProfile Ccg0 gam (s / 4) Tail.exponentTwo ≤ 24 * Ccg0

The printed lower-ellipticity profile is 2/3 . Ccg on the window 8 cgamma <= s, so the crude bound's deterministic shift is <= 24 Ccg.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.MultiscaleAbsorptionArith.badRemainder_le {Ccg0 cstarInv gam s : ℝ} (hCcg0 : 0 < Ccg0) (hcs : 0 ≤ cstarInv) (hgam0 : 0 < gam) (hs8 : 8 * gam ≤ s) : 8 * (Ccg0 * cstarInv * (s / 4) * gam * (2 * (s / 4) - gam)⁻¹ ^ 3) ≤ 38 * Ccg0 * cstarInv * gam * s⁻¹ ^ 2

The remainder summand of the crude bound's ordinary amplitude, at the window's own cube bound (8/(3s))^3.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.MultiscaleAbsorptionArith.badOrdinarySum_le {cstarInv gam s Ccg0 cc T dR E Q4a Q4b Q4c : ℝ} (hCcg0 : 0 < Ccg0) (hcc : 0 < cc) (hcs : 0 ≤ cstarInv) (hdR : 0 ≤ dR) (hgam0 : 0 < gam) (hgam1 : gam ≤ 1) (hs8 : 8 * gam ≤ s) (hT0 : 0 ≤ T) (hQ4a : Q4a = 122880 * Ccg0 * HCPolySupport.IndependentSums.gammaTriangleConst 1 * dR * cc⁻¹) (hQ4b : Q4b = 122880 * Ccg0 * HCPolySupport.IndependentSums.gammaTriangleConst 1 * dR) (hQ4c : Q4c = 608 * Ccg0) : 8 * ((1 + Real.log 2) ^ 1⁻¹ * ((8 * Ccg0 + 8 * 3 ^ gam * lowerEllipticityProfile Ccg0 gam (s / 4) Tail.exponentTwo) * (HCPolySupport.IndependentSums.gammaTriangleConst 1 * (20 * s⁻¹ * (16 * dR * s⁻¹ * (cc⁻¹ * cstarInv * T * gam + Real.exp (-(cc * E⁻¹ ^ 2 * gam⁻¹)))))) + 8 * (Ccg0 * cstarInv * (s / 4) * gam * (2 * (s / 4) - gam)⁻¹ ^ 3))) ≤ Q4a * cstarInv * T * gam * s⁻¹ ^ 2 + Q4b * Real.exp (-(cc * E⁻¹ ^ 2 * gam⁻¹)) * s⁻¹ ^ 2 + Q4c * cstarInv * gam * s⁻¹ ^ 2

The crude bound's ordinary amplitude, reduced to its three absorbable summands. Only the [0,1] profile bound, the remainder's cube bound and the merge constant 1 + log 2 <= 2 are used.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.MultiscaleAbsorptionArith.badOrdinaryAmplitude_le {cstarInv eps Cms E gam s Ccg0 cc T p dR K Q4a Q4b Q4c : ℝ} (hCcg0 : 0 < Ccg0) (hcc : 0 < cc) (hcs : 0 ≤ cstarInv) (hdR : 0 ≤ dR) (hgam0 : 0 < gam) (hgam1 : gam ≤ 1) (hs8 : 8 * gam ≤ s) (hT0 : 0 ≤ T) (hT : T ≤ eps ^ (-p)) (hp0 : 0 ≤ p) (heps0 : 0 < eps) (heps1 : eps ≤ 1) (hE : 0 < E) (hgammaE : gam ≤ E⁻¹ ^ 10) (hwin : cstarInv * eps ^ (-Cms) ≤ E) (hfloor : 2 / 3 * eps ^ (-Cms) ≤ E) (hQ4a : Q4a = 122880 * Ccg0 * HCPolySupport.IndependentSums.gammaTriangleConst 1 * dR * cc⁻¹) (hQ4b : Q4b = 122880 * Ccg0 * HCPolySupport.IndependentSums.gammaTriangleConst 1 * dR) (hQ4c : Q4c = 608 * Ccg0) (hCmsp : 2 + p ≤ Cms) (hQ4aE : Q4a ≤ E) (hQ4cE : Q4c ≤ E) (hK : 2 * Q4b * cc⁻¹ ^ 2 * (3 / 2) ^ 8 + 2 ≤ K) : 8 * ((1 + Real.log 2) ^ 1⁻¹ * ((8 * Ccg0 + 8 * 3 ^ gam * lowerEllipticityProfile Ccg0 gam (s / 4) Tail.exponentTwo) * (HCPolySupport.IndependentSums.gammaTriangleConst 1 * (20 * s⁻¹ * (16 * dR * s⁻¹ * (cc⁻¹ * cstarInv * T * gam + Real.exp (-(cc * E⁻¹ ^ 2 * gam⁻¹)))))) + 8 * (Ccg0 * cstarInv * (s / 4) * gam * (2 * (s / 4) - gam)⁻¹ ^ 3))) ≤ K * (s⁻¹ ^ 2 * (eps ^ 2 * E ^ 2 * gam))

The bad lane's Gamma_1 amplitude, absorbed into the ordinary normal form: the 3^{5h} cgamma head (polynomial in eps^{-1}, absorbed by the window at 2 + p <= Cms), the exponentially small tail (absorbed by x^2 e^{-x} <= 2), and the profile remainder.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.MultiscaleAbsorptionArith.badRareAmplitude_le {eps Cms E gam s Ccg0 K : ℝ} (hCcg0 : 0 < Ccg0) (hgam0 : 0 < gam) (hgam1 : gam ≤ 1) (hs : 0 < s) (hs1 : s ≤ 1) (heps0 : 0 < eps) (heps1 : eps ≤ 1) (hE : 0 < E) (hgammaE : gam ≤ E⁻¹ ^ 10) (hEa : 8 * Ccg0 ≤ E) (hCms : 2 ≤ 16 * Cms) (hfloor : 2 / 3 * eps ^ (-Cms) ≤ E) (hK : 8 * 4096 * Ccg0 ^ 2 * (3 / 2) ^ 16 ≤ K) (hK0 : 0 ≤ K) : 8 * ((1 + Real.log 2) ^ (2 / 7)⁻¹ * (8 * Real.exp (-(Ccg0⁻¹ * E⁻¹ ^ 2 * gam⁻¹)) + 8 * 3 ^ gam * Real.exp (-(Ccg0⁻¹ * E⁻¹ ^ 2 * gam⁻¹)))) ≤ K * (s⁻¹ ^ 4 * (eps ^ 2 * Real.exp (-(2 * E⁻¹ ^ 3 * gam⁻¹))))

The bad lane's Gamma_{2/7} amplitude, absorbed into the rare normal form. The printed rate exp(-(Ccg^{-1} E^{-2} cgamma^{-1})) clears the frozen root's own exp(-(2 E^{-3} cgamma^{-1})) on the window 8 Ccg <= E.

6. The deterministic remainder

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.MultiscaleAbsorptionArith.remainderGap_le {eps Cms E gam s hgapR Q5 : ℝ} (hQ5 : 0 ≤ Q5) (hgam0 : 0 < gam) (hs : 0 < s) (hs1 : s ≤ 1) (heps0 : 0 < eps) (heps1 : eps ≤ 1) (hE1 : 1 ≤ E) (hgammaE : gam ≤ E⁻¹ ^ 10) (hhgap0 : 0 ≤ hgapR) (hhgap : hgapR ≤ 2 * E) (hCms10 : 2 ≤ 10 * Cms) (hfloor : 2 / 3 * eps ^ (-Cms) ≤ E) : Q5 * gam ^ 2 * hgapR ^ 2 ≤ 4 * Q5 * (3 / 2) ^ 10 * (s⁻¹ ^ 2 * (eps ^ 2 * E ^ 2 * gam))

The cgamma^2 h^2 summand of the deterministic remainder.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.MultiscaleAbsorptionArith.remainderScale_le {eps Cms E gam s Q5 : ℝ} (hQ5 : 0 ≤ Q5) (hgam0 : 0 < gam) (hs : 0 < s) (heps0 : 0 < eps) (heps1 : eps ≤ 1) (hE1 : 1 ≤ E) (hgammaE : gam ≤ E⁻¹ ^ 10) (hCms10 : 2 ≤ 10 * Cms) (hfloor : 2 / 3 * eps ^ (-Cms) ≤ E) : Q5 * gam ^ 2 * (s ^ 2)⁻¹ ≤ Q5 * (3 / 2) ^ 10 * (s⁻¹ ^ 2 * (eps ^ 2 * E ^ 2 * gam))

The cgamma^2 s^{-2} summand of the deterministic remainder.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.MultiscaleAbsorptionArith.remainderLog_le {eps Cms E gam s Q5 : ℝ} (hQ5 : 0 ≤ Q5) (hgam0 : 0 < gam) (hgam1 : gam ≤ 1) (hs : 0 < s) (hs1 : s ≤ 1) (heps0 : 0 < eps) (heps1 : eps ≤ 1) (hE1 : 1 ≤ E) (hgammaE : gam ≤ E⁻¹ ^ 10) (hCms3 : 2 ≤ 3 * Cms) (hfloor : 2 / 3 * eps ^ (-Cms) ≤ E) : Q5 * gam ^ 2 * (E ^ 4 * |Real.log gam| ^ 4) ≤ 384 * Q5 * (3 / 2) ^ 3 * (s⁻¹ ^ 2 * (eps ^ 2 * E ^ 2 * gam))

The cgamma^2 E^4 |log cgamma|^4 summand of the deterministic remainder.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.MultiscaleAbsorptionArith.remainderTerm_le {eps Cms E gam s hgapR Q5 K : ℝ} (hQ5 : 0 ≤ Q5) (hgam0 : 0 < gam) (hgam1 : gam ≤ 1) (hs : 0 < s) (hs1 : s ≤ 1) (heps0 : 0 < eps) (heps1 : eps ≤ 1) (hE1 : 1 ≤ E) (hgammaE : gam ≤ E⁻¹ ^ 10) (hhgap0 : 0 ≤ hgapR) (hhgap : hgapR ≤ 2 * E) (hCms3 : 2 ≤ 3 * Cms) (hCms10 : 2 ≤ 10 * Cms) (hfloor : 2 / 3 * eps ^ (-Cms) ≤ E) (hK : 4 * Q5 * (3 / 2) ^ 10 + Q5 * (3 / 2) ^ 10 + 384 * Q5 * (3 / 2) ^ 3 ≤ K) : Q5 * gam ^ 2 * (hgapR ^ 2 + (s ^ 2)⁻¹ + E ^ 4 * |Real.log gam| ^ 4) ≤ K * (s⁻¹ ^ 2 * (eps ^ 2 * E ^ 2 * gam))

The deterministic remainder, absorbed into the ordinary normal form.