Pull back real-slice measure through the original frequency chart, using real Jacobians.

theorem KamProject.Arnold1963.AnalyticFrequencyChart.inverse_real {n : ℕ} {A g : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} (c : AnalyticFrequencyChart A g G Ω) {x : RealSpace n} (hx : complexify x ∈ Ω) : complexify (realPart (g (complexify x))) = g (complexify x)

theorem KamProject.Arnold1963.AnalyticFrequencyChart.realSlice_inverse_image {n : ℕ} {A g : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} (c : AnalyticFrequencyChart A g G Ω) {S : Set (ComplexSpace n)} (hS : S ⊆ Ω) : realSlice (g '' S) = realRestriction g '' realSlice S

theorem KamProject.Arnold1963.AnalyticFrequencyChart.inverse_realVolume_le {n : ℕ} {A g : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} (c : AnalyticFrequencyChart A g G Ω) {S : Set (ComplexSpace n)} (hS : MeasurableSet S) (hSΩ : S ⊆ Ω) {θ : ℝ} (hθ : 0 < θ) (hlo : ∀ p ∈ G, ∀ (v : ComplexSpace n), θ * ‖v‖ ≤ ‖(fderiv ℂ A p) v‖) : realVolume (g '' S) ≤ ENNReal.ofReal (θ⁻¹ ^ n) * realVolume S

theorem KamProject.Arnold1963.AnalyticFrequencyChart.inverse_image_complement {n : ℕ} {A g : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} (c : AnalyticFrequencyChart A g G Ω) {G₁ : Set (ComplexSpace n)} (hG₁ : G₁ ⊆ G) : g '' (Ω \ A '' G₁) = G \ G₁

theorem KamProject.Arnold1963.AnalyticFrequencyChart.realVolume_loss_le {n : ℕ} {A g : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} (c : AnalyticFrequencyChart A g G Ω) {G₁ S : Set (ComplexSpace n)} (hG₁ : G₁ ⊆ G) (hS : MeasurableSet S) (hcover : S ⊆ A '' G₁) {θ : ℝ} (hθ : 0 < θ) (hlo : ∀ p ∈ G, ∀ (v : ComplexSpace n), θ * ‖v‖ ≤ ‖(fderiv ℂ A p) v‖) : realVolume (G \ G₁) ≤ ENNReal.ofReal (θ⁻¹ ^ n) * realVolume (Ω \ S)

theorem KamProject.Arnold1963.AnalyticFrequencyChart.realVolume_image_le {n : ℕ} {A g : ComplexSpace n → ComplexSpace n} {G Ω : Set (ComplexSpace n)} (c : AnalyticFrequencyChart A g G Ω) {Θ : ℝ} (hΘ : 0 ≤ Θ) (hhi : ∀ p ∈ G, ‖fderiv ℂ A p‖ ≤ Θ) : realVolume Ω ≤ ENNReal.ofReal (Θ ^ n) * realVolume G