meromorphicNFOn_univ — Mathlib

English

For any divisor d, the factorized rational function F = ∏ᶠ u (· − u)^{d(u)} is meromorphic on the whole field (Set.univ).

Русский

Для любого делителя d функция F = ∏ᶠ u (· − u)^{d(u)} мероморфна на всей области (универсуме поля).

LaTeX

$$$\text{MeromorphicNFOn}\left(\prod^{\mathrm{fin}}_{u} (\cdot - u)^{d(u)}\right) \;\text{Set.univ}$$$

Lean4

/-- Factorized rational functions are meromorphic in normal form on `univ`.
-/
theorem meromorphicNFOn_univ (d : 𝕜 → ℤ) : MeromorphicNFOn (∏ᶠ u, (· - u) ^ d u) univ := by
  classical
  by_cases hd : d.support.Finite
  · intro z hz
    rw [extractFactor z hd]
    right
    use d z, (∏ᶠ u, (· - u) ^ update d z 0 u)
    simp [analyticAt, ne_zero]
  · rw [← mulSupport d] at hd
    rw [finprod_of_infinite_mulSupport hd]
    exact AnalyticOnNhd.meromorphicNFOn analyticOnNhd_const

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