Frequency functions agreeing near every domain point give the same analytic chart.

theorem KamProject.Arnold1963.AnalyticFrequencyChart.congr {n : ℕ} {A A' g : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} (c : AnalyticFrequencyChart A g G Ω) (he : ∀ p ∈ G, A' =ᶠ[nhds p] A) : AnalyticFrequencyChart A' g G Ω