6.37. MappingDegree.LocalKFoldMultiplicityUnconditional🔗

Jacobians.MappingDegree.LocalKFoldMultiplicityUnconditional — source

kthRootSubstitution_of_localFactorization

Bundle construction from a local factorization.

theorem kthRootSubstitution_of_localFactorization
    {g u : ℂ → ℂ} {x₀ w₀ : ℂ} {R : ℝ} {k : ℕ}
    (hR : 0 < R) (hk : 1 ≤ k)
    (hu_an : AnalyticOnNhd ℂ u (Metric.closedBall x₀ R))
    (hu_x₀ : u x₀ ≠ 0)
    (hfact : ∀ z ∈ Metric.closedBall x₀ R,
        g z - w₀ = (z - x₀) ^ k * u z) :
    KthRootSubstitution g x₀ w₀ k

localMultiplicityOne_preimage_card_with_radius

localMultiplicityOne_preimage_card with an extra radius bound ε ≤ R.

theorem localMultiplicityOne_preimage_card_with_radius
    {g : ℂ → ℂ} {x₀ : ℂ}
    (h_an : AnalyticAt ℂ g x₀) (hd : deriv g x₀ ≠ 0)
    {R : ℝ} (hR : 0 < R) :
    ∃ ε > (0 : ℝ), ε ≤ R ∧ ∃ δ > (0 : ℝ),
      ∀ w ∈ Metric.ball (g x₀) δ, w ≠ g x₀ →
        ({z ∈ Metric.ball x₀ ε | g z = w} : Set ℂ).ncard = 1

kthRootsFinset

The k-th roots of a nonzero complex number, viewed as a Finset.

noncomputable def kthRootsFinset (k : ℕ) (a : ℂ) : Finset ℂ

kth_roots_eq_finset

The set of k-th roots of a equals (kthRootsFinset k a : Set ℂ), when a ≠ 0 and k ≥ 1.

lemma kth_roots_eq_finset {k : ℕ} (hk : 1 ≤ k) {a : ℂ} (_ha : a ≠ 0) :
    {ξ : ℂ | ξ ^ k = a} = (kthRootsFinset k a : Set ℂ)

kth_roots_finset_card

The Finset of k-th roots has cardinality k.

lemma kth_roots_finset_card {k : ℕ} (hk : 1 ≤ k) {a : ℂ} (ha : a ≠ 0) :
    (kthRootsFinset k a).card = k