meromorphicOrderAt_ne_top — Mathlib

English

The order at z of the factorized rational function is never top (i.e., not +∞) for any z when the support is finite.

Русский

Порядок в точке z для факторизованной рациональной функции никогда не достигает бесконечности при конечной опоре.

LaTeX

$$$\meromorphicOrderAt\left(\prod^{\mathrm{fin}}_{u} (\cdot - u)^{d(u)}\right) z \neq \top$$$

Lean4

/-- Factorized rational functions are nowhere locally constant zero.
-/
theorem meromorphicOrderAt_ne_top {z : 𝕜} (d : 𝕜 → ℤ) : meromorphicOrderAt (∏ᶠ u, (· - u) ^ d u) z ≠ ⊤ :=
  by
  by_cases hd : d.support.Finite
  · simp [meromorphicOrderAt_eq d hd]
  · rw [← mulSupport] at hd
    have : AnalyticAt 𝕜 (1 : 𝕜 → 𝕜) z := analyticAt_const
    simp [finprod_of_infinite_mulSupport hd, this.meromorphicOrderAt_eq, this.analyticOrderAt_eq_zero.2 (by simp)]

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