Supporting results for the analytic Hamiltonian KAM construction.

noncomputable def KamProject.Arnold1963.homologicalBound (n : ℕ) (M K δ : ℝ) : ℝ

The uniform norm bound for the finite homological generating function.

Equations

• KamProject.Arnold1963.homologicalBound n M K δ = M * KamProject.Arnold1963.constantL5 n / (K * δ ^ KamProject.Arnold1963.homologicalExponent n)

theorem KamProject.Arnold1963.constantL0_pos (n : ℕ) : 0 < constantL0 n

theorem KamProject.Arnold1963.constantL5_pos (n : ℕ) : 0 < constantL5 n

theorem KamProject.Arnold1963.nat_pow_exp_bound {x δ : ℝ} (hx : 0 < x) (hδ : 0 < δ) (n : ℕ) : x ^ (n + 1) * Real.exp (-(x * δ)) ≤ constantL0 n / δ ^ (n + 1)

theorem KamProject.Arnold1963.norm_homologicalCoeff_le {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {ω : ComplexSpace n → ComplexSpace n} {M K N : ℝ} {p : ComplexSpace n} (hp : p ∈ G) (hM : f.uniformNorm ≤ M) (hK : 0 < K) (hnr : FiniteNonresonant (ω p) K N) {k : FourierIndex n} (hk : k ∈ lowModes n N) : ‖homologicalCoeff f ω p k‖ ≤ M / K * indexLength k ^ (n + 1) * Real.exp (-(indexLength k * ↑ρ))

theorem KamProject.Arnold1963.norm_homologicalTerm_le {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {ω : ComplexSpace n → ComplexSpace n} {M K N δ : ℝ} {p q : ComplexSpace n} (hp : p ∈ G) (hM : f.uniformNorm ≤ M) (hK : 0 < K) (hδ : 0 < δ) (hnr : FiniteNonresonant (ω p) K N) (hq : ‖imagPart q‖ ≤ ↑ρ - (δ + δ)) {k : FourierIndex n} (hk : k ∈ lowModes n N) : ‖homologicalCoeff f ω p k * fourierMonomial k q‖ ≤ M / K * (constantL0 n / δ ^ (n + 1)) * Real.exp (-δ * indexLength k)

theorem KamProject.Arnold1963.norm_homologicalGenerator_le {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {ω : ComplexSpace n → ComplexSpace n} {M K N δ : ℝ} {p q : ComplexSpace n} (hp : p ∈ G) (hM : f.uniformNorm ≤ M) (hK : 0 < K) (hδ : 0 < δ) (hδ1 : δ ≤ 1) (hnr : FiniteNonresonant (ω p) K N) (hq : ‖imagPart q‖ ≤ ↑ρ - (δ + δ)) : ‖homologicalGenerator f ω N (p, q)‖ ≤ homologicalBound n M K δ