meromorphicOrderAt_eq — Mathlib

English

The order of the factorized rational function F = ∏ᶠ u (· − u)^{d(u)} at z equals d(z) when the support of d is finite.

Русский

Порядок нуля функции F = ∏ᶠ u (z − u)^{d(u)} в точке z равен d(z) при конечной опоре d.

LaTeX

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

Lean4

/-- The order of the factorized rational function `(∏ᶠ u, fun z ↦ (z - u) ^ d u)` at `z` equals `d z`.
-/
theorem meromorphicOrderAt_eq {z : 𝕜} (d : 𝕜 → ℤ) (h₁d : d.support.Finite) :
    meromorphicOrderAt (∏ᶠ u, (· - u) ^ d u) z = d z := by
  classical
  rw [meromorphicOrderAt_eq_int_iff ((meromorphicNFOn_univ d).meromorphicOn _ (mem_univ _))]
  use ∏ᶠ u, (· - u) ^ update d z 0 u
  simp only [update_self, le_refl, analyticAt, ne_eq, ne_zero, not_false_eq_true, smul_eq_mul, true_and]
  filter_upwards
  simp [extractFactor z h₁d]

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