meromorphicTrailingCoeffAt — Mathlib

English

If analytic at x and the value at x is nonzero, the trailing coefficient equals f(x).

Русский

Если аналитично в x и f(x) ≠ 0, то trailing coefficient равен f(x).

LaTeX

$$$\\text{meromorphicTrailingCoeffAt} f x = f x$ при $f x \\neq 0$ и $\\text{AnalyticAt} f x$$$

Lean4

/-- If `f` is meromorphic of finite order at a point `x`, the trailing coefficient is defined as the
(unique!) value `g x` for a presentation of `f` in the form `(z - x) ^ order • g z` with `g`
analytic at `x`. In all other cases, the trailing coefficient is defined to be zero.
-/
noncomputable def meromorphicTrailingCoeffAt : E :=
  by
  by_cases h₁ : MeromorphicAt f x
  · by_cases h₂ : meromorphicOrderAt f x = ⊤
    · exact 0
    · exact ((meromorphicOrderAt_ne_top_iff h₁).1 h₂).choose x
  · exact 0

Похожие утверждения