Supporting results for the analytic Hamiltonian KAM construction.

noncomputable def KamProject.Arnold1963.homologicalFunction {n : ℕ} {G E : Set (ComplexSpace n)} {ρ δ : NNReal} (f : AnalyticPhaseFunction n G ρ) (ω : ComplexSpace n → ComplexSpace n) {K N M : ℝ} (hE : E ⊆ G) (hc : ConjInvariant E) (hω : AnalyticOnNhd ℂ ω E) (hωc : ∀ p ∈ E, ω (conjVec p) = conjVec (ω p)) (hnr : ∀ p ∈ E, FiniteNonresonant (ω p) K N) (hK : 0 < K) (hM : f.uniformNorm ≤ M) (hδ : 0 < δ) (hδ1 : δ ≤ 1) (hδρ : δ + δ ≤ ρ) : AnalyticPhaseFunction n E (ρ - (δ + δ))

The finite homological generator packaged with analytic phase-function structure and bounds.

Equations

• One or more equations did not get rendered due to their size.

theorem KamProject.Arnold1963.norm_homologicalFunction_le {n : ℕ} {G E : Set (ComplexSpace n)} {ρ δ : NNReal} (f : AnalyticPhaseFunction n G ρ) (ω : ComplexSpace n → ComplexSpace n) {K N M : ℝ} (hE : E ⊆ G) (hc : ConjInvariant E) (hω : AnalyticOnNhd ℂ ω E) (hωc : ∀ p ∈ E, ω (conjVec p) = conjVec (ω p)) (hnr : ∀ p ∈ E, FiniteNonresonant (ω p) K N) (hK : 0 < K) (hM : f.uniformNorm ≤ M) (hδ : 0 < δ) (hδ1 : δ ≤ 1) (hδρ : δ + δ ≤ ρ) : (homologicalFunction f ω hE hc hω hωc hnr hK hM hδ hδ1 hδρ).uniformNorm ≤ homologicalBound n M K ↑δ