English
A variant showing that if the point x is outside the support of d, the trailing coefficient equals the product with update at x.
Русский
Вариант: если x не принадлежит опоре d, то завершающий коэффициент равен произведению с обновлением в x.
LaTeX
$$$\text{meromorphicTrailingCoeffAt}\left(\prod^{\mathrm{fin}}_{u} (\cdot - u)^{d(u)}\right) x = \prod^{\mathrm{fin}}_{u} (x - u)^{d(u)\;\text{with}\; d\,\text{updated at } x\;0\;u}$$$
Lean4
/-- In the setting of `MeromorphicOn.extract_zeros_poles`, compute the trailing
coefficient of `f` in terms of `divisor f U` and `g x`.
-/
theorem meromorphicTrailingCoeffAt_extract_zeros_poles {x : 𝕜} {f g : 𝕜 → E} {D : 𝕜 → ℤ} (hD : D.support.Finite)
(h₁x : x ∈ U) (h₂x : AccPt x (𝓟 U)) (hf : MeromorphicAt f x) (h₁g : AnalyticAt 𝕜 g x) (h₂g : g x ≠ 0)
(h : f =ᶠ[codiscreteWithin U] (∏ᶠ u, (· - u) ^ D u) • g) :
meromorphicTrailingCoeffAt f x = (∏ᶠ u, (x - u) ^ Function.update D x 0 u) • g x :=
by
have t₀ : MeromorphicAt (∏ᶠ u, (· - u) ^ D u) x := (FactorizedRational.meromorphicNFOn D U).meromorphicOn x h₁x
rw [meromorphicTrailingCoeffAt_congr_nhdsNE
(hf.eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin (by fun_prop) h₁x h₂x h),
t₀.meromorphicTrailingCoeffAt_smul h₁g.meromorphicAt, h₁g.meromorphicTrailingCoeffAt_of_ne_zero h₂g]
simp [meromorphicTrailingCoeffAt_factorizedRational hD]
