Bounds for the omitted Fourier modes, retaining the exponential cutoff factor.
theorem
KamProject.Arnold1963.norm_fourierSeries_tail_le_of_decay
{n : ℕ}
{a : FourierIndex n → ℂ}
{M ρ δ γ N : ℝ}
{σ : NNReal}
(hM : 0 ≤ M)
(hδ : 0 < δ)
(hδ1 : δ ≤ 1)
(hγ : 0 ≤ γ)
(hσ : ↑σ ≤ ρ - (δ + γ))
(ha : ∀ (k : FourierIndex n), ‖a k‖ ≤ M * Real.exp (-(indexLength k * ρ)))
:
‖∑' (k : FourierIndex n), fourierTermOnStrip a σ k - ∑ k ∈ fourierModes n N, fourierTermOnStrip a σ k‖ ≤ M * Real.exp (-N * γ) * (4 / δ) ^ n