StepFourBoundaryBudget #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
1. The window count #
|Icc n m| = (m-n)+1 as a real, for n ≤ m.
2. The boundary budget kit: legs #
theorem
Algsuperdiff.Section4.Provider.Regularity.sum_Icc_top_boundaryDelta_le_of_legs
{δ Ag Ah ε : ℤ → ℝ}
{r₁ r₂ Kg Kh Hinf Flat Se W ind : ℝ}
{n m : ℤ}
(hnm : n ≤ m)
(hr₁0 : 0 < r₁)
(hr₁1 : r₁ < 1)
(hr₂0 : 0 < r₂)
(hr₂1 : r₂ < 1)
(hAg0 : 0 ≤ Ag m)
(hAgd : ∀ j ≤ m, Ag j ≤ Kg * r₁ ^ (m - j))
(hAh0 : 0 ≤ Ah m)
(hAhd : ∀ j ≤ m, Ah j ≤ Kh * r₂ ^ (m - j))
(hSe : ∑ j ∈ Finset.Icc n m, ε j ≤ Se)
(hHinf : 0 ≤ Hinf)
(hind0 : 0 ≤ ind)
(hW : W = ↑m - ↑n + 1)
(hδ : ∀ (j : ℤ), δ j = Ag j + (Ah j + ε j * Hinf + Flat) * ind)
:
e.sum.delta.j.bound with the anchor's ε-free flat leg carried.
δ_j = A^g_j + (A^h_j + ε_j H + F) 𝟙 with A^g, A^h geometrically dominated
from the top scale and F a constant (flat) leg. Then
∑_{j=n}^{m} δ_j ≤ K_g/(1-r₁) + ( K_h/(1-r₂) + S_ε H + W F ) 𝟙 , W = (m-n)+1 .
The flat leg's contribution is W-linear: it is the only summand whose
coefficient is not bought by the ε-budget.
3. stepFourDeltaOut in the boundary four-leg shape #
noncomputable def
Algsuperdiff.Section4.Provider.Regularity.stepFourBoundaryDeltaConst
(Crem Vd Cst s : ℝ)
:
The single constant the Step-4 boundary output collapses to: C_rem V_d C (s^{-4} s^{-3/2} + 8 s^{-7} + s^{-6}).