Local analytic k-th root

RS.AnalyticAt.exists_pow_eq: a non-vanishing analytic germ u at z₀ : ℂ has an analytic k-th root r near z₀ (r ^ k = u eventually, r z₀ ≠ 0), for any k ≠ 0.

Route (design §5.1): with a := u z₀ ≠ 0, set r z := exp (log a / k) * exp (log (u z / a) / k). Only log (u z / a) (value near 1, inside slitPlane) needs analyticity of log; exp (log a) = a holds for every nonzero constant, so no case split on arg (u z₀) is needed.

theorem RS.AnalyticAt.exists_pow_eq {u : ℂ → ℂ} {z₀ : ℂ} (hu : AnalyticAt ℂ u z₀) (hu₀ : u z₀ ≠ 0) {k : ℕ} (hk : k ≠ 0) : ∃ (r : ℂ → ℂ), AnalyticAt ℂ r z₀ ∧ r z₀ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds z₀, r z ^ k = u z

Local analytic k-th root of a non-vanishing analytic function.