Finite Fourier polynomials and their bounds on complex angle strips.

noncomputable def KamProject.Arnold1963.fourierMonomial {n : ℕ} (k : FourierIndex n) (q : ComplexSpace n) : ℂ

The complex Fourier character with integer frequency and angles of period 2π.

Equations

• KamProject.Arnold1963.fourierMonomial k q = Complex.exp (Complex.I * KamProject.Arnold1963.indexPairing k q)

noncomputable def KamProject.Arnold1963.fourierTruncation {n : ℕ} (a : FourierIndex n → ℂ) (N : ℝ) (q : ComplexSpace n) : ℂ

The finite Fourier sum over modes below the specified strict cutoff.

Equations

• KamProject.Arnold1963.fourierTruncation a N q = ∑ k ∈ KamProject.Arnold1963.fourierModes n N, a k * KamProject.Arnold1963.fourierMonomial k q

@[simp]

theorem KamProject.Arnold1963.fourierMonomial_zero {n : ℕ} (q : ComplexSpace n) : fourierMonomial 0 q = 1

theorem KamProject.Arnold1963.fourierTruncation_eq_zero_add {n : ℕ} (a : FourierIndex n → ℂ) {N : ℝ} (hN : 0 < N) (q : ComplexSpace n) : fourierTruncation a N q = a 0 + ∑ k ∈ lowModes n N, a k * fourierMonomial k q

theorem KamProject.Arnold1963.norm_fourierMonomial_le {n : ℕ} (k : FourierIndex n) (q : ComplexSpace n) : ‖fourierMonomial k q‖ ≤ Real.exp (indexLength k * ‖imagPart q‖)

theorem KamProject.Arnold1963.norm_fourierTerm_le {n : ℕ} {a : FourierIndex n → ℂ} {M ρ δ : ℝ} (hM : 0 ≤ M) (ha : ∀ (k : FourierIndex n), ‖a k‖ ≤ M * Real.exp (-(indexLength k * ρ))) {q : ComplexSpace n} (hq : ‖imagPart q‖ ≤ ρ - δ) (k : FourierIndex n) : ‖a k * fourierMonomial k q‖ ≤ M * Real.exp (-(indexLength k * δ))

theorem KamProject.Arnold1963.norm_fourierTruncation_le {n : ℕ} {a : FourierIndex n → ℂ} {M ρ δ : ℝ} (hM : 0 ≤ M) (ha : ∀ (k : FourierIndex n), ‖a k‖ ≤ M * Real.exp (-(indexLength k * ρ))) {q : ComplexSpace n} (hq : ‖imagPart q‖ ≤ ρ - δ) (N : ℝ) : ‖fourierTruncation a N q‖ ≤ M * ∑ k ∈ fourierModes n N, Real.exp (-(indexLength k * δ))