6.50. MappingDegree.RoucheBridge🔗

Jacobians.MappingDegree.RoucheBridge — source

kFold_count_radiusBounded

Radius-bounded fully-unconditional planar k-fold count.

Same conclusion as localKFoldMultiplicity_preimage_card, but with the additional guarantee ε ≤ R for a prescribed R > 0.

theorem kFold_count_radiusBounded
    {g : ℂ → ℂ} {x₀ w₀ : ℂ} {k : ℕ} {R : ℝ}
    (hR : 0 < R) (hk : 1 ≤ k)
    (hg : AnalyticAt ℂ g x₀)
    (h_w₀ : g x₀ = w₀)
    (hord : analyticOrderAt (fun z => g z - w₀) x₀ = (k : ℕ∞)) :
    ∃ ε > (0 : ℝ), ε ≤ R ∧ ∃ δ > (0 : ℝ),
      ∀ w ∈ Metric.ball (g x₀) δ, w ≠ g x₀ →
        ({z ∈ Metric.ball x₀ ε | g z = w} : Set ℂ).ncard = k