meromorphicOrderAt_nonneg_iff_analyticAt

English

For a meromorphic function in normal form, order is nonnegative iff the function is analytic at that point.

Русский

Для мероморфной функции в нормальной форме порядок неотрицателен тогда и только тогда, когда функция аналитична в этой точке.

LaTeX

$$$0 \le \operatorname{meromorphicOrderAt} f x \,\Leftrightarrow\, \AnalyticAt f x$$$

Lean4

/-- If a function is meromorphic in normal form at `x`, then it has non-negative order iff it is
analytic. -/
theorem meromorphicOrderAt_nonneg_iff_analyticAt (hf : MeromorphicNFAt f x) :
    0 ≤ meromorphicOrderAt f x ↔ AnalyticAt 𝕜 f x :=
  by
  constructor <;> intro h₂f
  · rw [meromorphicNFAt_iff_analyticAt_or] at hf
    rcases hf with h | ⟨_, h₃f, _⟩
    · exact h
    · by_contra h'
      exact lt_irrefl 0 (lt_of_le_of_lt h₂f h₃f)
  · rw [h₂f.meromorphicOrderAt_eq]
    simp

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