English
The log of the norm of the trailing coefficient equals the sum over u of (d(u) · log ||x − u||).
Русский
Логарифм нормы завершающего коэффициента равен сумме по u: d(u) · log ||x − u||.
LaTeX
$$$\log \|\mathrm{meromorphicTrailingCoeffAt}\left(\prod^{\mathrm{fin}}_{u} (\cdot - u)^{d(u)}\right) x\| = \sum^{\mathrm{fin}}_{u} (d(u)) \cdot \log \|x - u\|$$
Lean4
/-- Variant of `meromorphicTrailingCoeffAt_factorizedRational`: Compute log of the norm of the trailing
coefficient. The convention that `log 0 = 0` gives a closed formula easier than the one in
`meromorphicTrailingCoeffAt_factorizedRational`.
-/
theorem log_norm_meromorphicTrailingCoeffAt {d : 𝕜 → ℤ} {x : 𝕜} (h : d.support.Finite) :
log ‖meromorphicTrailingCoeffAt (∏ᶠ u, (· - u) ^ d u) x‖ = ∑ᶠ u, (d u) * log ‖x - u‖ := by
classical
rw [meromorphicTrailingCoeffAt_factorizedRational h, finprod_eq_prod_of_mulSupport_subset _ (mulSupport_update h)]
have : ∀ y ∈ h.toFinset, ‖(x - y) ^ update d x 0 y‖ ≠ 0 :=
by
intro y _
by_cases h : x = y
· rw [h]
simp_all
· simp_all [zpow_ne_zero, sub_ne_zero]
rw [norm_prod, log_prod _ _ this]
have : (fun u ↦ (d u) * log ‖x - u‖).support ⊆ h.toFinset :=
by
intro u
contrapose
simp_all
rw [finsum_eq_sum_of_support_subset _ this]
apply Finset.sum_congr rfl
intro y hy
rw [norm_zpow, Real.log_zpow]
by_cases h : x = y
· simp [h]
· rw [Function.update_of_ne (by tauto)]
