Compose the old frequency inverse with the inverse of the small shift. Domain buffers and measure bounds are assembled in FrequencyDomain to keep the dependencies acyclic.

theorem KamProject.Arnold1963.frequencyChange_derivative_bounds {n : ℕ} {A Δ : ComplexSpace n → ComplexSpace n} {p : ComplexSpace n} {θ Θ : ℝ} {κ : NNReal} (hA : DifferentiableAt ℂ A p) (hΔ : DifferentiableAt ℂ Δ p) (hθΘ : θ ≤ Θ) (hlo : ∀ (v : ComplexSpace n), θ * ‖v‖ ≤ ‖(fderiv ℂ A p) v‖) (hhi : ∀ (v : ComplexSpace n), ‖(fderiv ℂ A p) v‖ ≤ Θ * ‖v‖) (hdΔ : ‖fderiv ℂ Δ p‖ ≤ ↑κ * θ) (v : ComplexSpace n) : θ * (1 - ↑κ) * ‖v‖ ≤ ‖(fderiv ℂ (fun (x : ComplexSpace n) => A x + Δ x) p) v‖ ∧ ‖(fderiv ℂ (fun (x : ComplexSpace n) => A x + Δ x) p) v‖ ≤ Θ * (1 + ↑κ) * ‖v‖

theorem KamProject.Arnold1963.frequencyShiftData_of_old_inverse {n : ℕ} {g Δ : ComplexSpace n → ComplexSpace n} {G V : Set (ComplexSpace n)} {β κ : NNReal} {θ : ℝ} (hβ : 0 < β) (hκ : κ < 1) (hθ : 0 < θ) (hg : AnalyticOnNhd ℂ g V) (hmap : Set.MapsTo g V G) (hΔ : AnalyticOnNhd ℂ Δ G) (hb : NormBoundOn Δ G ↑β) (hdg : ∀ x ∈ V, ‖fderiv ℂ g x‖ ≤ θ⁻¹) (hdΔ : ∀ p ∈ G, ‖fderiv ℂ Δ p‖ ≤ ↑κ * θ) : FrequencyShiftData (Δ ∘ g) V β κ

noncomputable def KamProject.Arnold1963.correctedFrequencyInverse {n : ℕ} (g Δ : ComplexSpace n → ComplexSpace n) (V : Set (ComplexSpace n)) (β : NNReal) : ComplexSpace n → ComplexSpace n

The inverse of a corrected frequency chart, composed with the original inverse chart.

Equations

• KamProject.Arnold1963.correctedFrequencyInverse g Δ V β = g ∘ KamProject.Arnold1963.frequencyInverse (Δ ∘ g) V β

theorem KamProject.Arnold1963.correctedFrequencyInverse_analytic {n : ℕ} {g Δ : ComplexSpace n → ComplexSpace n} {V : Set (ComplexSpace n)} {β κ : NNReal} (d : FrequencyShiftData (Δ ∘ g) V β κ) (hg : AnalyticOnNhd ℂ g V) : AnalyticOnNhd ℂ (correctedFrequencyInverse g Δ V β) (frequencyInverseTarget V β)

theorem KamProject.Arnold1963.correctedFrequencyInverse_right {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {V : Set (ComplexSpace n)} {β κ : NNReal} (d : FrequencyShiftData (Δ ∘ g) V β κ) (hA : ∀ x ∈ V, A (g x) = x) {y : ComplexSpace n} (hy : y ∈ frequencyInverseTarget V β) : A (correctedFrequencyInverse g Δ V β y) + Δ (correctedFrequencyInverse g Δ V β y) = y

theorem KamProject.Arnold1963.correctedFrequencyInverse_injOn {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {V : Set (ComplexSpace n)} {β κ : NNReal} (d : FrequencyShiftData (Δ ∘ g) V β κ) (hA : ∀ x ∈ V, A (g x) = x) : Set.InjOn (correctedFrequencyInverse g Δ V β) (frequencyInverseTarget V β)

theorem KamProject.Arnold1963.correctedFrequency_image_domain {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {V Ω₁ : Set (ComplexSpace n)} {β κ : NNReal} (d : FrequencyShiftData (Δ ∘ g) V β κ) (hA : ∀ x ∈ V, A (g x) = x) (hΩ₁ : Ω₁ ⊆ frequencyInverseTarget V β) : (fun (p : ComplexSpace n) => A p + Δ p) '' correctedFrequencyInverse g Δ V β '' Ω₁ = Ω₁