Supporting results for the analytic Hamiltonian KAM construction.

noncomputable def KamProject.Arnold1963.actionFrequency {n : ℕ} (h : ComplexSpace n → ℂ) (p : ComplexSpace n) : ComplexSpace n

The coordinate gradient of an action-dependent Hamiltonian, giving its frequency map.

Equations

• KamProject.Arnold1963.actionFrequency h p j = (fderiv ℂ h p) (Pi.single j 1)

noncomputable def KamProject.Arnold1963.actionFrequencyCLM (n : ℕ) : (ComplexSpace n →L[ℂ] ℂ) →L[ℂ] ComplexSpace n

Evaluation of an action covector on the coordinate basis as a continuous linear map.

Equations

• KamProject.Arnold1963.actionFrequencyCLM n = ContinuousLinearMap.pi fun (j : Fin n) => (ContinuousLinearMap.apply ℂ ℂ) (Pi.single j 1)

theorem KamProject.Arnold1963.fderiv_actionFrequency_apply {n : ℕ} {h : ComplexSpace n → ℂ} {p : ComplexSpace n} (ha : AnalyticAt ℂ h p) (v : ComplexSpace n) (j : Fin n) : (fderiv ℂ (actionFrequency h) p) v j = ((fderiv ℂ (fderiv ℂ h) p) v) (Pi.single j 1)

theorem KamProject.Arnold1963.fderiv_eq_actionFrequency {n : ℕ} (h : ComplexSpace n → ℂ) (p v : ComplexSpace n) : (fderiv ℂ h p) v = ∑ j : Fin n, actionFrequency h p j * v j

theorem KamProject.Arnold1963.analyticOnNhd_actionFrequency {n : ℕ} {G : Set (ComplexSpace n)} {h : ComplexSpace n → ℂ} (hh : AnalyticOnNhd ℂ h G) : AnalyticOnNhd ℂ (actionFrequency h) G

theorem KamProject.Arnold1963.actionFrequency_conj_of_mem_nhds {n : ℕ} {h : ComplexSpace n → ℂ} {V : Set (ComplexSpace n)} {p : ComplexSpace n} (ha : AnalyticAt ℂ h p) (hc : ∀ x ∈ V, h (conjVec x) = star (h x)) (hp : V ∈ nhds (conjVec p)) : actionFrequency h (conjVec p) = conjVec (actionFrequency h p)

structure KamProject.Arnold1963.IntegrableData {n : ℕ} (h : ComplexSpace n → ℂ) (G : Set (ComplexSpace n)) (Θ : ℝ) : Prop

Analyticity, real compatibility and frequency bounds for an integrable Hamiltonian.

• analytic : AnalyticOnNhd ℂ h G
• conj_compatible (p : ComplexSpace n) : p ∈ G → h (conjVec p) = star (h p)
• frequency_conj (p : ComplexSpace n) : p ∈ G → actionFrequency h (conjVec p) = conjVec (actionFrequency h p)
• hessian_bound (p : ComplexSpace n) : p ∈ G → ∀ (i j : Fin n), ‖((fderiv ℂ (fderiv ℂ h) p) (Pi.single i 1)) (Pi.single j 1)‖ ≤ Θ