Summation of the exponential lattice kernel in the sum-of-absolute-coordinates norm. The product decomposition supplies normal convergence bounds for Fourier series.

@[reducible, inline]

abbrev KamProject.Arnold1963.fourierIndexSuccEquiv (n : ℕ) : FourierIndex (n + 1) ≃ ℤ × FourierIndex n

Splitting an integer Fourier index into its first coordinate and its tail.

Equations

• KamProject.Arnold1963.fourierIndexSuccEquiv n = (Fin.consEquiv fun (x : Fin (n + 1)) => ℤ).symm

theorem KamProject.Arnold1963.hasSum_exp_int_abs {δ : ℝ} (hδ : 0 < δ) : HasSum (fun (k : ℤ) => Real.exp (-δ * |↑k|)) ((1 + Real.exp (-δ)) / (1 - Real.exp (-δ)))

theorem KamProject.Arnold1963.hasSum_exp_indexLength (n : ℕ) {δ : ℝ} (hδ : 0 < δ) : HasSum (fun (k : FourierIndex n) => Real.exp (-δ * indexLength k)) (((1 + Real.exp (-δ)) / (1 - Real.exp (-δ))) ^ n)

theorem KamProject.Arnold1963.summable_exp_indexLength (n : ℕ) {δ : ℝ} (hδ : 0 < δ) : Summable fun (k : FourierIndex n) => Real.exp (-δ * indexLength k)

theorem KamProject.Arnold1963.tsum_exp_indexLength_le (n : ℕ) {δ : ℝ} (hδ : 0 < δ) (hδ1 : δ ≤ 1) : ∑' (k : FourierIndex n), Real.exp (-δ * indexLength k) ≤ (4 / δ) ^ n