Supporting results for the analytic Hamiltonian KAM construction.

noncomputable def KamProject.Arnold1963.homologicalCoeff {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) (ω : ComplexSpace n → ComplexSpace n) (p : ComplexSpace n) (k : FourierIndex n) : ℂ

The coefficient solving the homological equation for one nonzero Fourier mode.

Equations

• KamProject.Arnold1963.homologicalCoeff f ω p k = Complex.I * f.fourierCoeff p k / KamProject.Arnold1963.indexPairing k (ω p)

noncomputable def KamProject.Arnold1963.homologicalGenerator {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) (ω : ComplexSpace n → ComplexSpace n) (N : ℝ) (z : ComplexPhaseSpace n) : ℂ

The finite Fourier generating function solving the truncated homological equation.

Equations

• KamProject.Arnold1963.homologicalGenerator f ω N z = ∑ k ∈ KamProject.Arnold1963.lowModes n N, KamProject.Arnold1963.homologicalCoeff f ω z.1 k * KamProject.Arnold1963.fourierMonomial k z.2

theorem KamProject.Arnold1963.analyticAt_homologicalCoeff {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {ω : ComplexSpace n → ComplexSpace n} {K N : ℝ} {p : ComplexSpace n} (hp : p ∈ G) (hω : AnalyticAt ℂ ω p) (hK : 0 < K) (hnr : FiniteNonresonant (ω p) K N) {k : FourierIndex n} (hk : k ∈ lowModes n N) : AnalyticAt ℂ (fun (P : ComplexSpace n) => homologicalCoeff f ω P k) p

theorem KamProject.Arnold1963.analyticAt_homologicalGenerator {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {ω : ComplexSpace n → ComplexSpace n} {K N : ℝ} {z : ComplexPhaseSpace n} (hz : z.1 ∈ G) (hω : AnalyticAt ℂ ω z.1) (hK : 0 < K) (hnr : FiniteNonresonant (ω z.1) K N) : AnalyticAt ℂ (homologicalGenerator f ω N) z

theorem KamProject.Arnold1963.homologicalGenerator_periodic {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {ω : ComplexSpace n → ComplexSpace n} {N : ℝ} (p q : ComplexSpace n) (m : FourierIndex n) : homologicalGenerator f ω N (p, q + angleShift m) = homologicalGenerator f ω N (p, q)

theorem KamProject.Arnold1963.homologicalCoeff_conj {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {ω : ComplexSpace n → ComplexSpace n} {p : ComplexSpace n} (hp : p ∈ G) (hω : ω (conjVec p) = conjVec (ω p)) (k : FourierIndex n) : homologicalCoeff f ω (conjVec p) (-k) = star (homologicalCoeff f ω p k)

theorem KamProject.Arnold1963.homologicalGenerator_conj {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {ω : ComplexSpace n → ComplexSpace n} {N : ℝ} {z : ComplexPhaseSpace n} (hz : z.1 ∈ G) (hω : ω (conjVec z.1) = conjVec (ω z.1)) : homologicalGenerator f ω N (conjPhase z) = star (homologicalGenerator f ω N z)

theorem KamProject.Arnold1963.angle_fderiv_homologicalGenerator {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {ω : ComplexSpace n → ComplexSpace n} {N : ℝ} (p q v : ComplexSpace n) : (fderiv ℂ (fun (t : ComplexSpace n) => homologicalGenerator f ω N (p, t)) q) v = ∑ k ∈ lowModes n N, homologicalCoeff f ω p k * (Complex.I * indexPairing k v * fourierMonomial k q)

theorem KamProject.Arnold1963.homological_equation {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {ω : ComplexSpace n → ComplexSpace n} {K N : ℝ} {z : ComplexPhaseSpace n} (hz : z.1 ∈ G) (hω : AnalyticAt ℂ ω z.1) (hK : 0 < K) (hnr : FiniteNonresonant (ω z.1) K N) (hN : 0 < N) (hmean : f.angleAverage z.1 = 0) : ∑ j : Fin n, ω z.1 j * qGradient (homologicalGenerator f ω N) z j + fourierTruncation (f.fourierCoeff z.1) N z.2 = 0