6.6. MappingDegree.AnalyticKthRoot🔗

Jacobians.MappingDegree.AnalyticKthRoot — source

slitPlane_of_mem_ball_one

Points in Metric.ball (1 : ℂ) (1/2) lie in Complex.slitPlane.

lemma slitPlane_of_mem_ball_one {z : ℂ} (hz : z ∈ Metric.ball (1 : ℂ) (1/2)) :
    z ∈ Complex.slitPlane

analytic_kth_root_of_nonvanishing

Analytic k-th root branch on a disc.

theorem analytic_kth_root_of_nonvanishing
    {u : ℂ → ℂ} {x₀ : ℂ} {ρ : ℝ} {k : ℕ}
    (hρ : 0 < ρ)
    (hu : AnalyticOnNhd ℂ u (Metric.closedBall x₀ ρ))
    (hux₀ : u x₀ ≠ 0) (hk : 1 ≤ k) :
    ∃ (r : ℂ → ℂ) (ρ' : ℝ), 0 < ρ' ∧ ρ' ≤ ρ ∧
      AnalyticOnNhd ℂ r (Metric.closedBall x₀ ρ') ∧
      ∀ z ∈ Metric.closedBall x₀ ρ', (r z) ^ k = u z