English
If the ratio converges in ENNReal sense to a finite r, the radius is r^{-1} in ENNReal terms.
Русский
Если отношение сходится в ENNReal к конечному r, то радиус равен r^{-1} в ENNReal смысле.
LaTeX
$$$\operatorname{radius}(\operatorname{ofScalars} E c) = r^{-1}$ in ENNReal sense$$
Lean4
/-- The order of an analytic function `f` at `z₀` equals a natural number `n` iff `f` can locally
be written as `f z = (z - z₀) ^ n • g z`, where `g` is analytic and does not vanish at `z₀`. -/
theorem analyticOrderAt_eq_natCast (hf : AnalyticAt 𝕜 f z₀) :
analyticOrderAt f z₀ = n ↔ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ z in 𝓝 z₀, f z = (z - z₀) ^ n • g z :=
by
unfold analyticOrderAt
split_ifs with h
· simp only [ENat.top_ne_coe, false_iff]
contrapose! h
rw [← hf.exists_eventuallyEq_pow_smul_nonzero_iff]
exact ⟨n, h⟩
· rw [← hf.exists_eventuallyEq_pow_smul_nonzero_iff] at h
refine ⟨fun hn ↦ (WithTop.coe_inj.mp hn : h.choose = n) ▸ h.choose_spec, fun h' ↦ ?_⟩
rw [AnalyticAt.unique_eventuallyEq_pow_smul_nonzero h.choose_spec h']
