English
Variant expression for log of the trailing coefficient similar to the non-variant form.
Русский
Вариант выражения логарифма нормы завершающего коэффициента аналогичен основному формату.
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
/-- In the setting of `MeromorphicOn.extract_zeros_poles`, compute the log of the
norm of the trailing coefficient of `f` in terms of `divisor f U` and `g x`.
-/
theorem log_norm_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) :
log ‖meromorphicTrailingCoeffAt f x‖ = ∑ᶠ u, (D u) * log ‖x - u‖ + log ‖g x‖ :=
by
rw [meromorphicTrailingCoeffAt_congr_nhdsNE
(hf.eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin
(((FactorizedRational.meromorphicNFOn D U).meromorphicOn x h₁x).smul h₁g.meromorphicAt) h₁x h₂x h),
((FactorizedRational.meromorphicNFOn D U).meromorphicOn x h₁x).meromorphicTrailingCoeffAt_smul h₁g.meromorphicAt,
h₁g.meromorphicTrailingCoeffAt_of_ne_zero h₂g, norm_smul, log_mul, log_norm_meromorphicTrailingCoeffAt hD]
· simp only [ne_eq, norm_eq_zero]
apply
MeromorphicAt.meromorphicTrailingCoeffAt_ne_zero ((FactorizedRational.meromorphicNFOn D U).meromorphicOn x h₁x)
apply FactorizedRational.meromorphicOrderAt_ne_top
· simp_all
