Supporting results for the analytic Hamiltonian KAM construction.

theorem KamProject.Arnold1963.actionFrequency_add {n : ℕ} {a b : ComplexSpace n → ℂ} {p : ComplexSpace n} (ha : DifferentiableAt ℂ a p) (hb : DifferentiableAt ℂ b p) : actionFrequency (fun (x : ComplexSpace n) => a x + b x) p = actionFrequency a p + actionFrequency b p

theorem KamProject.Arnold1963.actionFrequency_add_eventually {n : ℕ} {a b : ComplexSpace n → ℂ} {p : ComplexSpace n} (ha : AnalyticAt ℂ a p) (hb : AnalyticAt ℂ b p) : (actionFrequency fun (x : ComplexSpace n) => a x + b x) =ᶠ[nhds p] fun (x : ComplexSpace n) => actionFrequency a x + actionFrequency b x

noncomputable def KamProject.Arnold1963.AnalyticPhaseFunction.averagedHamiltonian {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) (a : ComplexSpace n → ℂ) : ComplexSpace n → ℂ

The integrable Hamiltonian updated by adding the perturbation's angle average.

Equations

• f.averagedHamiltonian a p = a p + f.angleAverage p

noncomputable def KamProject.Arnold1963.AnalyticPhaseFunction.frequencyShift {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) : ComplexSpace n → ComplexSpace n

The frequency correction produced by the perturbation's angle average.

Equations

• f.frequencyShift = KamProject.Arnold1963.actionFrequency f.angleAverage

theorem KamProject.Arnold1963.AnalyticPhaseFunction.frequencyShift_analytic {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) : AnalyticOnNhd ℂ f.frequencyShift G

theorem KamProject.Arnold1963.AnalyticPhaseFunction.frequencyShift_bound {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {β : NNReal} (hβ : 0 < β) {M : ℝ} (hf : f.uniformNorm ≤ M) : NormBoundOn f.frequencyShift (erosion G β) (M / ↑β)

theorem KamProject.Arnold1963.AnalyticPhaseFunction.frequencyShift_derivative_bound {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {β : NNReal} (hβ : 0 < β) {M : ℝ} (hf : f.uniformNorm ≤ M) {p : ComplexSpace n} (hp : p ∈ erosion G β) : ‖fderiv ℂ f.frequencyShift p‖ ≤ 2 * ↑n * M / ↑β ^ 2

theorem KamProject.Arnold1963.AnalyticPhaseFunction.frequencyShift_conj {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {β : NNReal} (hβ : 0 < β) {p : ComplexSpace n} (hp : p ∈ erosion G β) : f.frequencyShift (conjVec p) = conjVec (f.frequencyShift p)

theorem KamProject.Arnold1963.AnalyticPhaseFunction.averagedHamiltonian_frequency {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {a : ComplexSpace n → ℂ} (ha : AnalyticOnNhd ℂ a G) {p : ComplexSpace n} (hp : p ∈ G) : actionFrequency (f.averagedHamiltonian a) p = actionFrequency a p + f.frequencyShift p