Construct the corrected analytic chart from the original chart and a small frequency shift, including local two-sided inverse identities.

theorem KamProject.Arnold1963.correctedFrequency_chart {n : ℕ} {A g Δ : ComplexSpace n → ComplexSpace n} {G Ω H V U : Set (ComplexSpace n)} {β κ : NNReal} (c : AnalyticFrequencyChart A g G Ω) (d : FrequencyShiftData (Δ ∘ g) V β κ) (hV : V ⊆ Ω) (hgV : Set.MapsTo g V H) (hHG : H ⊆ G) (hΔ : AnalyticOnNhd ℂ Δ H) (hVc : ConjInvariant V) (hΔc : ∀ p ∈ H, Δ (conjVec p) = conjVec (Δ p)) (hU : IsCompact U) (hUc : ConjInvariant U) (hUt : U ⊆ frequencyInverseTarget V β) : AnalyticFrequencyChart (fun (p : ComplexSpace n) => A p + Δ p) (correctedFrequencyInverse g Δ V β) (correctedFrequencyInverse g Δ V β '' U) U