Construct a local frequency chart from nondegeneracy at a real point, before choosing a perturbation. The frequency domain is a real-centered closed polydisc; the action domain is its analytic inverse image and need not be convex.

theorem KamProject.Arnold1963.realCenteredPolydisc_const_eq_closedBall {n : ℕ} (c : RealSpace n) {r : ℝ} (hr : 0 ≤ r) : (realCenteredPolydisc c fun (x : Fin n) => r) = Metric.closedBall (complexify c) r

theorem KamProject.Arnold1963.exists_polydisc_frequency_chart {n : ℕ} {A : ComplexSpace n → ComplexSpace n} {V : Set (ComplexSpace n)} (x : RealSpace n) (hV : V ∈ nhds (complexify x)) (ha : AnalyticAt ℂ A (complexify x)) (hu : IsUnit (fderiv ℂ A (complexify x))) (hc : ∀ p ∈ V, A (conjVec p) = conjVec (A p)) : ∃ (g : ComplexSpace n → ComplexSpace n) (G : Set (ComplexSpace n)) (r : ℝ), 0 < r ∧ G ⊆ V ∧ complexify x ∈ interior G ∧ AnalyticFrequencyChart A g G (realCenteredPolydisc (realPart (A (complexify x))) fun (x : Fin n) => r)

theorem KamProject.Arnold1963.AnalyticFrequencyChart.exists_derivative_bounds {n : ℕ} {A g : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} (c : AnalyticFrequencyChart A g G Ω) : ∃ (θ : NNReal) (Θ : NNReal), 0 < θ ∧ θ < 1 ∧ 1 < Θ ∧ (∀ p ∈ G, ∀ (v : ComplexSpace n), ↑θ * ‖v‖ ≤ ‖(fderiv ℂ A p) v‖) ∧ ∀ p ∈ G, ‖fderiv ℂ A p‖ ≤ ↑Θ