English
The ENNReal formulation handles zero and infinite cases uniformly via ENNReal arithmetic.
Русский
Формулировка ENNReal обрабатывает случаи нуля и бесконечности однородно через арифметику ENNReal.
LaTeX
$$$\text{(ENNReal formulation of radius)}$$$
Lean4
/-- The order of vanishing of `f` at `z₀`, as an element of `ℕ∞`.
The order is defined to be `∞` if `f` is identically 0 on a neighbourhood of `z₀`, and otherwise the
unique `n` such that `f` can locally be written as `f z = (z - z₀) ^ n • g z`, where `g` is analytic
and does not vanish at `z₀`. See `AnalyticAt.analyticOrderAt_eq_top` and
`AnalyticAt.analyticOrderAt_eq_natCast` for these equivalences.
If `f` isn't analytic at `z₀`, then `analyticOrderAt f z₀` returns a junk value of `0`. -/
noncomputable def analyticOrderAt (f : 𝕜 → E) (z₀ : 𝕜) : ℕ∞ :=
if hf : AnalyticAt 𝕜 f z₀ then
if h : ∀ᶠ z in 𝓝 z₀, f z = 0 then ⊤ else ↑(hf.exists_eventuallyEq_pow_smul_nonzero_iff.mpr h).choose
else 0
