Supporting results for the analytic Hamiltonian KAM construction.
theorem
KamProject.Arnold1963.IntegrableData.of_frequency_bound
{n : ℕ}
{G : Set (ComplexSpace n)}
{h : ComplexSpace n → ℂ}
{Θ : ℝ}
(ha : AnalyticOnNhd ℂ h G)
(hc : ∀ p ∈ G, h (conjVec p) = star (h p))
(hωc : ∀ p ∈ G, actionFrequency h (conjVec p) = conjVec (actionFrequency h p))
(hbound : ∀ p ∈ G, ‖fderiv ℂ (actionFrequency h) p‖ ≤ Θ)
:
IntegrableData h G Θ