Analytic frequency charts on compact domains. Local inverse identities imply the required coverage and inverse derivative estimates.

structure KamProject.Arnold1963.AnalyticFrequencyChart {n : ℕ} (A g : ComplexSpace n → ComplexSpace n) (G Ω : Set (ComplexSpace n)) : Prop

An analytic frequency chart with an analytic inverse and specified source and target sets.

• compact : IsCompact G
• analytic : AnalyticOnNhd ℂ A G
• inverse_analytic : AnalyticOnNhd ℂ g Ω
• maps : Set.MapsTo A G Ω
• inverse_maps : Set.MapsTo g Ω G
• left_local (p : ComplexSpace n) : p ∈ G → ∀ᶠ (x : ComplexSpace n) in nhds p, g (A x) = x
• right_local (y : ComplexSpace n) : y ∈ Ω → ∀ᶠ (x : ComplexSpace n) in nhds y, A (g x) = x
• domain_conj : ConjInvariant G
• map_conj (p : ComplexSpace n) : p ∈ G → A (conjVec p) = conjVec (A p)

theorem KamProject.Arnold1963.AnalyticFrequencyChart.left {n : ℕ} {A g : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} (c : AnalyticFrequencyChart A g G Ω) {p : ComplexSpace n} (hp : p ∈ G) : g (A p) = p

theorem KamProject.Arnold1963.AnalyticFrequencyChart.right {n : ℕ} {A g : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} (c : AnalyticFrequencyChart A g G Ω) {y : ComplexSpace n} (hy : y ∈ Ω) : A (g y) = y

theorem KamProject.Arnold1963.AnalyticFrequencyChart.image_eq {n : ℕ} {A g : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} (c : AnalyticFrequencyChart A g G Ω) : A '' G = Ω

theorem KamProject.Arnold1963.AnalyticFrequencyChart.inverse_image_eq {n : ℕ} {A g : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} (c : AnalyticFrequencyChart A g G Ω) : g '' Ω = G

theorem KamProject.Arnold1963.AnalyticFrequencyChart.image_compact {n : ℕ} {A g : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} (c : AnalyticFrequencyChart A g G Ω) : IsCompact Ω

theorem KamProject.Arnold1963.AnalyticFrequencyChart.injOn {n : ℕ} {A g : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} (c : AnalyticFrequencyChart A g G Ω) : Set.InjOn A G

theorem KamProject.Arnold1963.AnalyticFrequencyChart.image_conj {n : ℕ} {A g : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} (c : AnalyticFrequencyChart A g G Ω) : ConjInvariant Ω

theorem KamProject.Arnold1963.AnalyticFrequencyChart.inverse_conj {n : ℕ} {A g : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} (c : AnalyticFrequencyChart A g G Ω) {y : ComplexSpace n} (hy : y ∈ Ω) : g (conjVec y) = conjVec (g y)

theorem KamProject.Arnold1963.AnalyticFrequencyChart.symm {n : ℕ} {A g : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} (c : AnalyticFrequencyChart A g G Ω) : AnalyticFrequencyChart g A Ω G

theorem KamProject.Arnold1963.AnalyticFrequencyChart.interior_back {n : ℕ} {A g : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} (c : AnalyticFrequencyChart A g G Ω) {p : ComplexSpace n} (hp : p ∈ G) (hy : A p ∈ interior Ω) : p ∈ interior G

theorem KamProject.Arnold1963.AnalyticFrequencyChart.inverse_maps_erosion {n : ℕ} {A g : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} (c : AnalyticFrequencyChart A g G Ω) {Θ β : NNReal} (hΘ : 0 < Θ) (hd : ∀ p ∈ G, ‖fderiv ℂ A p‖ ≤ ↑Θ) : Set.MapsTo g (erosion Ω (Θ * β)) (erosion G β)

theorem KamProject.Arnold1963.AnalyticFrequencyChart.erosion_subset_image {n : ℕ} {A g : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} (c : AnalyticFrequencyChart A g G Ω) {Θ β : NNReal} (hΘ : 0 < Θ) (hd : ∀ p ∈ G, ‖fderiv ℂ A p‖ ≤ ↑Θ) : erosion Ω (Θ * β) ⊆ A '' erosion G β

theorem KamProject.Arnold1963.AnalyticFrequencyChart.inverse_derivative_le {n : ℕ} {A g : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} (c : AnalyticFrequencyChart A g G Ω) {θ : ℝ} (hθ : 0 < θ) (hlo : ∀ p ∈ G, ∀ (v : ComplexSpace n), θ * ‖v‖ ≤ ‖(fderiv ℂ A p) v‖) {y : ComplexSpace n} (hy : y ∈ Ω) : ‖fderiv ℂ g y‖ ≤ θ⁻¹

theorem KamProject.Arnold1963.AnalyticFrequencyChart.restrict {n : ℕ} {A g : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} (c : AnalyticFrequencyChart A g G Ω) {S : Set (ComplexSpace n)} (hS : S ⊆ Ω) (hSc : IsCompact S) (hSj : ConjInvariant S) : AnalyticFrequencyChart A g (g '' S) S