English
The natural-order version of analytic order is defined as the natural part of the analytic order.
Русский
Естественный порядок аналитичности определяется как натуральная часть порядка аналитичности.
LaTeX
$$$\text{analyticOrderNatAt } f z_0 := (analyticOrderAt f z_0).toNat$$$
Lean4
/-- The order of vanishing of `f` at `z₀`, as an element of `ℕ`.
The order is defined to be `0` if `f` is identically zero on a neighbourhood of `z₀`,
and is 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 `analyticOrderNatAt f z₀` returns a junk value of `0`. -/
noncomputable def analyticOrderNatAt (f : 𝕜 → E) (z₀ : 𝕜) : ℕ :=
(analyticOrderAt f z₀).toNat
