Supporting results for the analytic Hamiltonian KAM construction.

noncomputable def KamProject.Arnold1963.indexPairingCLM {n : ℕ} (k : FourierIndex n) : ComplexSpace n →L[ℂ] ℂ

Pairing with an integer Fourier index as a continuous complex linear functional.

Equations

• KamProject.Arnold1963.indexPairingCLM k = ∑ j : Fin n, ↑(k j) • ContinuousLinearMap.proj j

@[simp]

theorem KamProject.Arnold1963.indexPairingCLM_apply {n : ℕ} (k : FourierIndex n) (q : ComplexSpace n) : (indexPairingCLM k) q = indexPairing k q

theorem KamProject.Arnold1963.fderiv_fourierMonomial {n : ℕ} (k : FourierIndex n) (q v : ComplexSpace n) : (fderiv ℂ (fourierMonomial k) q) v = Complex.I * indexPairing k v * fourierMonomial k q

theorem KamProject.Arnold1963.fourierMonomial_periodic {n : ℕ} (k m : FourierIndex n) (q : ComplexSpace n) : fourierMonomial k (q + angleShift m) = fourierMonomial k q

theorem KamProject.Arnold1963.fourierMonomial_conj_neg {n : ℕ} (k : FourierIndex n) (q : ComplexSpace n) : fourierMonomial (-k) (conjVec q) = star (fourierMonomial k q)

theorem KamProject.Arnold1963.sum_lowModes_neg {n : ℕ} {A : Type u_1} [AddCommMonoid A] (N : ℝ) (f : FourierIndex n → A) : ∑ k ∈ lowModes n N, f (-k) = ∑ k ∈ lowModes n N, f k

theorem KamProject.Arnold1963.angle_fderiv_eq_sum_qGradient {n : ℕ} {S : ComplexPhaseSpace n → ℂ} {p q : ComplexSpace n} (ha : AnalyticAt ℂ S (p, q)) (v : ComplexSpace n) : (fderiv ℂ (fun (t : ComplexSpace n) => S (p, t)) q) v = ∑ j : Fin n, v j * qGradient S (p, q) j