StreamDerivativeSumBound

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

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