English
The trailing coefficient of the factorized rational function at x equals ∏ᶠ u (x − u)^{update(d, x, 0, u)}.
Русский
Здесь постоянный коэффициент (Trailing coefficient) факторизованной рациональной функции в точке x равен ∏ᶠ u (x − u)^{update(d, x, 0, u)}.
LaTeX
$$$\operatorname{meromorphicTrailingCoeffAt}\left(\prod^{\mathrm{fin}}_{u} (\cdot - u)^{d(u)}\right) x = \prod^{\mathrm{fin}}_{u} (x - u)^{\operatorname{update}(d, x, 0, u)}$$
Lean4
/-- Variant of `meromorphicTrailingCoeffAt_factorizedRational`: Compute the trailing coefficient of the
factorized rational function associated with `d : 𝕜 → ℤ` at points outside the support of `d`.
-/
theorem meromorphicTrailingCoeffAt_factorizedRational_off_support {d : 𝕜 → ℤ} {x : 𝕜} (h₁ : d.support.Finite)
(h₂ : x ∉ d.support) : meromorphicTrailingCoeffAt (∏ᶠ u, (· - u) ^ d u) x = ∏ᶠ u, (x - u) ^ d u := by
classical
rw [meromorphicTrailingCoeffAt_factorizedRational h₁, finprod_eq_prod_of_mulSupport_subset _ (mulSupport_update h₁)]
have : (fun u ↦ (x - u) ^ d u).mulSupport ⊆ h₁.toFinset :=
by
intro u
contrapose
simp_all
rw [finprod_eq_prod_of_mulSupport_subset _ this, Finset.prod_congr rfl]
intro y hy
congr
apply Function.update_of_ne
by_contra hCon
simp_all
