The Fourier tail estimate with the explicit constant used in the analytic KAM iteration.

theorem KamProject.Arnold1963.kernel_constant_le_arnold {n : ℕ} (hn : 0 < n) {δ : ℝ} (hδ : 0 < δ) (hsmall : δ ≤ 1 / 12) : (4 / δ) ^ n ≤ (2 * ↑n / Real.exp 1) ^ n / δ ^ (n + 1)

theorem KamProject.Arnold1963.norm_fourierSeries_tail_le_arnoldConstant {n : ℕ} {a : FourierIndex n → ℂ} {M ρ δ γ N : ℝ} {σ : NNReal} (hn : 0 < n) (hM : 0 ≤ M) (hδ : 0 < δ) (hsmall : δ ≤ 1 / 12) (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‖ ≤ (2 * ↑n / Real.exp 1) ^ n * M / δ ^ (n + 1) * Real.exp (-N * γ)