English
Variant of trailing coefficient log: the same type of formula holds for the log of the trailing coefficient with the update operation.
Русский
Вариант формулы для логарифма завершающего коэффициента: та же форма обновления применяется к d.
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
/-- If `f` is meromorphic on an open set `U`, if `f` is nowhere locally constant zero, and if the
support of the divisor of `f` is finite, then there exists an analytic function `g` on `U` without
zeros such that `f` is equivalent, modulo equality on codiscrete sets, to the product of `g` and the
factorized rational function associated with the divisor of `f`.
-/
theorem extract_zeros_poles {f : 𝕜 → E} (h₁f : MeromorphicOn f U) (h₂f : ∀ u : U, meromorphicOrderAt f u ≠ ⊤)
(h₃f : (divisor f U).support.Finite) :
∃ g : 𝕜 → E,
AnalyticOnNhd 𝕜 g U ∧ (∀ u : U, g u ≠ 0) ∧ f =ᶠ[codiscreteWithin U] (∏ᶠ u, (· - u) ^ divisor f U u) • g :=
by
-- Take `g` as the inverse of the Laurent polynomial defined below, converted to a meromorphic
-- function in normal form. Then check all the properties.
let φ := ∏ᶠ u, (· - u) ^ (divisor f U u)
have hφ : MeromorphicOn φ U := (meromorphicNFOn (divisor f U) U).meromorphicOn
let g := toMeromorphicNFOn (φ⁻¹ • f) U
have hg : MeromorphicNFOn g U := by apply meromorphicNFOn_toMeromorphicNFOn
refine ⟨g, ?_, ?_, ?_⟩
· -- AnalyticOnNhd 𝕜 g U
rw [← hg.divisor_nonneg_iff_analyticOnNhd, divisor_of_toMeromorphicNFOn (hφ.inv.smul h₁f),
divisor_smul hφ.inv h₁f _ (fun z hz ↦ h₂f ⟨z, hz⟩), divisor_inv, Function.FactorizedRational.divisor h₃f,
neg_add_cancel]
intro z hz
simpa [meromorphicOrderAt_inv] using meromorphicOrderAt_ne_top (divisor f U)
· -- ∀ (u : ↑U), g ↑u ≠ 0
intro ⟨u, hu⟩
rw [← (hg hu).meromorphicOrderAt_eq_zero_iff, ←
meromorphicOrderAt_congr (toMeromorphicNFOn_eq_self_on_nhdsNE (hφ.inv.smul h₁f) hu).symm,
meromorphicOrderAt_smul (hφ u hu).inv (h₁f u hu), meromorphicOrderAt_inv, meromorphicOrderAt_eq _ h₃f]
simp only [h₁f, hu, divisor_apply]
lift meromorphicOrderAt f u to ℤ using (h₂f ⟨u, hu⟩) with n hn
rw [WithTop.untop₀_coe, ← WithTop.LinearOrderedAddCommGroup.coe_neg, ← WithTop.coe_add]
simp
· -- f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), fun z ↦ (z - u) ^ (divisor f U) u) * g
filter_upwards [(divisor f U).eq_zero_codiscreteWithin, (hφ.inv.smul h₁f).meromorphicNFAt_mem_codiscreteWithin,
self_mem_codiscreteWithin U] with a h₂a h₃a h₄a
unfold g
simp only [Pi.smul_apply', toMeromorphicNFOn_eq_toMeromorphicNFAt (hφ.inv.smul h₁f) h₄a,
toMeromorphicNFAt_eq_self.2 h₃a, Pi.inv_apply]
rw [← smul_assoc, smul_eq_mul, mul_inv_cancel₀ _, one_smul]
rwa [← ((meromorphicNFOn_univ (divisor f U)) trivial).meromorphicOrderAt_eq_zero_iff, meromorphicOrderAt_eq, h₂a,
Pi.zero_apply, WithTop.coe_zero]
