English
If the ratio tends to zero while coefficients are eventually nonzero, the radius is top.
Русский
Если коэффициенты не нулевые после некоторого момента и отношение стремится к нулю, радиус бесконечен.
LaTeX
$$$\text{radius}(\operatorname{ofScalars} E c) = \top$$$
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 analyticOrderNatAt_eq_iff (hf : AnalyticAt 𝕜 f z₀) (hf' : analyticOrderAt f z₀ ≠ ⊤) {n : ℕ} :
analyticOrderNatAt f z₀ = n ↔
∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ z in 𝓝 z₀, f z = (z - z₀) ^ n • g z :=
by simp [← Nat.cast_inj (R := ℕ∞), Nat.cast_analyticOrderNatAt hf', hf.analyticOrderAt_eq_natCast]
