English
For any U and locally finite divisor D with finite support, the divisor of the finite product equals D.
Русский
Для данного U и локально ограниченного делителя D с конечной опорой дивизор конечного произведения равен D.
LaTeX
$$$\text{MeromorphicOn.divisor}\left(\finprod_{u} (\cdot - u)^{D(u)}\, U\right) = D$$$
Lean4
/-- Compute the trailing coefficient of the factorized rational function associated with `d : 𝕜 → ℤ`.
-/
/-
Low-priority TODO: Using that non-trivially normed fields contain infinitely many elements that are
no roots of unity, it might be possible to drop assumption `h` here and in some of the theorems
below.
-/
theorem meromorphicTrailingCoeffAt_factorizedRational {d : 𝕜 → ℤ} {x : 𝕜} (h : d.support.Finite) :
meromorphicTrailingCoeffAt (∏ᶠ u, (· - u) ^ d u) x = ∏ᶠ u, (x - u) ^ update d x 0 u :=
by
have : (fun u ↦ (· - u) ^ d u).mulSupport ⊆ h.toFinset := by simp [Function.FactorizedRational.mulSupport]
rw [finprod_eq_prod_of_mulSupport_subset _ this, meromorphicTrailingCoeffAt_prod (fun _ ↦ by fun_prop),
finprod_eq_prod_of_mulSupport_subset _ (mulSupport_update h)]
apply Finset.prod_congr rfl
intro y hy
rw [MeromorphicAt.meromorphicTrailingCoeffAt_zpow (by fun_prop)]
by_cases hxy : x = y
· rw [hxy, meromorphicTrailingCoeffAt_id_sub_const]
simp_all
· grind [Function.update_of_ne, meromorphicTrailingCoeffAt_id_sub_const]
