Planar normal form (Forster Thm 2.1, planar half)

• RS.AnalyticAt.exists_openPartialHomeomorph: packaged planar analytic inverse function theorem — an analytic f with deriv f z₀ ≠ 0 agrees near z₀ with an OpenPartialHomeomorph that is analytic with analytic inverse.
• RS.AnalyticAt.exists_normal_form: if the recentered vanishing order of f at z₀ is k ≠ 0, then f = f z₀ + φ ^ k near z₀ for an analytic local coordinate φ (φ z₀ = 0, deriv φ z₀ ≠ 0); also a packaged OpenPartialHomeomorph version.
• RS.analyticOrderAt_left_comp_sub: the recentered order is invariant under postcomposition with a bi-analytic germ (left twin of mathlib's analyticOrderAt_comp_of_deriv_ne_zero).
• RS.image_pow_ball: (· ^ k) maps ball 0 ρ onto ball 0 (ρ ^ k).

theorem RS.AnalyticAt.exists_openPartialHomeomorph {f : ℂ → ℂ} {z₀ : ℂ} (hf : AnalyticAt ℂ f z₀) (hf' : deriv f z₀ ≠ 0) : ∃ (φ : OpenPartialHomeomorph ℂ ℂ), z₀ ∈ φ.source ∧ (∀ z ∈ φ.source, ↑φ z = f z) ∧ AnalyticOnNhd ℂ (↑φ) φ.source ∧ AnalyticOnNhd ℂ (↑φ.symm) φ.target

Packaged planar analytic IFT: analytic + deriv ≠ 0 gives an OpenPartialHomeomorph agreeing with f near z₀, analytic with analytic inverse.

theorem RS.AnalyticAt.exists_normal_form {f : ℂ → ℂ} {z₀ : ℂ} {k : ℕ} (hf : AnalyticAt ℂ f z₀) (hk : analyticOrderAt (fun (x : ℂ) => f x - f z₀) z₀ = ↑k) (hk₀ : k ≠ 0) : ∃ (φ : ℂ → ℂ), AnalyticAt ℂ φ z₀ ∧ φ z₀ = 0 ∧ deriv φ z₀ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds z₀, f z = f z₀ + φ z ^ k

Local normal form (Forster 2.1, planar half): finite recentered order k ≥ 1 means f = f z₀ + φ ^ k with φ an analytic local coordinate at z₀.

theorem RS.AnalyticAt.exists_normal_form_openPartialHomeomorph {f : ℂ → ℂ} {z₀ : ℂ} {k : ℕ} (hf : AnalyticAt ℂ f z₀) (hk : analyticOrderAt (fun (x : ℂ) => f x - f z₀) z₀ = ↑k) (hk₀ : k ≠ 0) : ∃ (φ : OpenPartialHomeomorph ℂ ℂ), z₀ ∈ φ.source ∧ ↑φ z₀ = 0 ∧ AnalyticOnNhd ℂ (↑φ) φ.source ∧ AnalyticOnNhd ℂ (↑φ.symm) φ.target ∧ ∀ z ∈ φ.source, f z = f z₀ + ↑φ z ^ k

Normal form, packaged as an analytic-with-analytic-inverse partial homeomorphism.

theorem RS.analyticOrderAt_left_comp_sub {h f : ℂ → ℂ} {z₀ : ℂ} (hh : AnalyticAt ℂ h (f z₀)) (hh' : deriv h (f z₀) ≠ 0) (hf : AnalyticAt ℂ f z₀) : analyticOrderAt (fun (z : ℂ) => h (f z) - h (f z₀)) z₀ = analyticOrderAt (fun (x : ℂ) => f x - f z₀) z₀

Recentered order is invariant under postcomposition with a bi-analytic germ. (Left twin of mathlib's analyticOrderAt_comp_of_deriv_ne_zero; upstreamable.)

theorem RS.image_pow_ball {k : ℕ} (hk : k ≠ 0) {ρ : ℝ} (hρ : 0 ≤ ρ) : (fun (x : ℂ) => x ^ k) '' Metric.ball 0 ρ = Metric.ball 0 (ρ ^ k)

z ↦ z ^ k maps balls onto balls (fibre-counting geometry for mapping-degree).