Documentation

TauCeti.Analysis.Complex.LocalNormalForm

Local power coordinates for a holomorphic germ #

A holomorphic function whose difference from its value at a point has finite positive order m is, after subtracting that value, the mth power of a biholomorphic coordinate centered at the point. The coordinate and its inverse are analytic on their domains, and the power identity holds throughout the coordinate domain, which can be chosen inside any prescribed neighbourhood. This is the planar local model for ramification of holomorphic maps between Riemann surfaces.

References #

theorem AnalyticAt.exists_openPartialHomeomorph_sub_eq_pow {f : ℂ → ℂ} {z₀ : ℂ} {m : ℕ} (hf : AnalyticAt ℂ f z₀) (hm : 0 < m) (horder : analyticOrderAt (fun (z : ℂ) => f z - f z₀) z₀ = ↑m) {W : Set ℂ} (hW : W ∈ nhds z₀) :
∃ (e : OpenPartialHomeomorph ℂ ℂ), z₀ ∈ e.source ∧ ↑e z₀ = 0 ∧ e.source ⊆ W ∧ AnalyticOnNhd ℂ (↑e) e.source ∧ AnalyticOnNhd ℂ (↑e.symm) e.target ∧ ∀ z ∈ e.source, f z - f z₀ = ↑e z ^ m

A holomorphic germ of finite positive order after subtracting its value admits a centered biholomorphic coordinate in which that difference is exactly a power. Both directions of the coordinate are analytic, and its source lies inside any prescribed neighbourhood of the point.