4.3. LocalMultiplicity.AnalyticDerivOrder🔗

Jacobians.LocalMultiplicity.AnalyticDerivOrder — source

deriv_not_eventually_zero_of_analyticAt_not_eventually_const

Non-locally-constant ⇒ derivative not eventually zero. If F : ℂ → ℂ is analytic at z₀ and F is not eventually equal to F z₀ on any neighbourhood of z₀, then deriv F is not eventually zero on any neighbourhood of z₀.

Reads off AnalyticAt.analyticOrderAt_deriv_add_one: analyticOrderAt (deriv F) z₀ + 1 = analyticOrderAt (F · - F z₀) z₀. The hypothesis forces the right-hand side ≠ ⊤ (else F = F z₀ on a neighbourhood), hence the left-hand side ≠ ⊤, i.e. deriv F is not eventually 0.

lemma deriv_not_eventually_zero_of_analyticAt_not_eventually_const
    {F : ℂ → ℂ} {z₀ : ℂ}
    (hF : AnalyticAt ℂ F z₀)
    (hne : ¬ ∀ᶠ z in 𝓝 z₀, F z = F z₀) :
    ¬ ∀ᶠ z in 𝓝 z₀, deriv F z = 0