English
Characterizes when a natural n is ≤ the analytic order; equivalently, there exists a local representation with (z - z0)^n times an analytic, nonvanishing factor.
Русский
Характеризует, когда натуральное число n ≤_ORDER, существование локального представления с (z - z0)^n и некотирующим нулей фактором.
LaTeX
$$$n \le\ analyticOrderAt f z_0 \iff \exists g,\ AnalyticAt 𝕜 g z_0 \land \forall^ᶠ z \ in\nhds z_0, f z = (z - z_0)^n \cdot g z$$$
Lean4
/-- The order of an analytic function `f` at `z₀` is finite iff `f` can locally be written as `f z =
(z - z₀) ^ analyticOrderNatAt f z₀ • g z`, where `g` is analytic and does not vanish at `z₀`.
See `MeromorphicNFAt.order_eq_zero_iff` for an analogous statement about meromorphic functions in
normal form.
-/
theorem analyticOrderAt_ne_top (hf : AnalyticAt 𝕜 f z₀) :
analyticOrderAt f z₀ ≠ ⊤ ↔
∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ f =ᶠ[𝓝 z₀] fun z ↦ (z - z₀) ^ analyticOrderNatAt f z₀ • g z :=
by simp only [← ENat.coe_toNat_eq_self, Eq.comm, EventuallyEq, ← hf.analyticOrderAt_eq_natCast, analyticOrderNatAt]
