StreamDerivativeSum

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

The corrected full-range stream derivative sum

This module exposes the literal shell-derivative sum in corrected e.W.1.inf.bound. It is a source-facing provider over the already proved large-cube derivative gauge estimate; the internal gauge is unfolded in the conclusion.

Source: ABK26 l.km.kn.Lp.estimates, with inputs.

theorem Algsuperdiff.Section3.Provider.Stream.stream_derivative_sum_bound_provider (d : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : ABKModel d) (l m n : ℤ), n ≤ min m l → HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : Cutoff.ShellSeq d) => ∑ k ∈ Finset.Ioc n m, (3 ^ k * localCubeDerivNorm l (omega k) + 3 ^ (2 * k) * localCubeSecondDerivNorm l (omega k))) (C * √(max 1 (↑l - ↑n)) * min M.gamma⁻¹ (↑m - ↑n) * 3 ^ (M.gamma * ↑m))

The corrected full-range Gamma_2 bound for the weighted first- and second-derivative shell sum. The positive constant is chosen from the dimension before the model and all scales.