English
A concrete extraction of a factor from a finite product: the product equals the pulled-out factor times the product with updated exponent at u0.
Русский
Непосредственное извлечение фактора из конечного произведения: произведение равно вынесенному фактору, умноженному на произведение с обновленным показателем в u0.
LaTeX
$$$\prod^{\mathrm{fin}}_{u} (\cdot - u)^{d(u)} = (\cdot - u_0)^{d(u_0)} \cdot \prod^{\mathrm{fin}}_{u} (\cdot - u)^{(\mathrm{update}\, d\, u_0\, 0\, u)}$$$
Lean4
/-- In the setting of `MeromorphicOn.extract_zeros_poles`, the function `log ‖f‖` is equivalent, modulo
equality on codiscrete subsets, to `∑ᶠ u, (divisor f U u * log ‖· - u‖) + log ‖g ·‖`.
-/
theorem extract_zeros_poles_log {f g : 𝕜 → E} {D : Function.locallyFinsuppWithin U ℤ} (hg : ∀ u : U, g u ≠ 0)
(h : f =ᶠ[codiscreteWithin U] (∏ᶠ u, (· - u) ^ D u) • g) :
(log ‖f ·‖) =ᶠ[codiscreteWithin U] ∑ᶠ u, (D u * log ‖· - u‖) + (log ‖g ·‖) := by
-- Identify support of the sum in the goal
have t₁ : (fun u ↦ (D u * log ‖· - u‖)).support = D.support :=
by
ext u
rw [← not_iff_not]
simp only [ne_eq, not_not, Function.mem_support]
constructor <;> intro hx
· obtain ⟨y, hy⟩ := NormedField.exists_one_lt_norm 𝕜
have := congrFun hx (y + u)
simp only [add_sub_cancel_right, Pi.zero_apply, mul_eq_zero, Int.cast_eq_zero, log_eq_zero, norm_eq_zero] at this
rcases this with h | h | h | h
· assumption
· simp only [h, norm_zero] at hy
linarith
· simp only [h, lt_self_iff_false] at hy
· simp only [h, lt_neg_self_iff] at hy
linarith
·
simp_all [Pi.zero_def]
-- Trivial case: the support of D is infinite
by_cases h₃f : D.support.Finite
case neg =>
rw [finsum_of_infinite_support (by simpa [t₁] using h₃f)]
rw [finprod_of_infinite_mulSupport (by simpa [FactorizedRational.mulSupport] using h₃f)] at h
filter_upwards [h] with x hx
simp [hx]
-- General case
filter_upwards [h, D.eq_zero_codiscreteWithin, self_mem_codiscreteWithin U] with z hz h₂z h₃z
rw [Pi.zero_apply] at h₂z
rw [hz, finprod_eq_prod_of_mulSupport_subset (s := h₃f.toFinset) _ (by simp_all [FactorizedRational.mulSupport]),
finsum_eq_sum_of_support_subset (s := h₃f.toFinset) _ (by simp_all)]
have : ∀ x ∈ h₃f.toFinset, ‖z - x‖ ^ D x ≠ 0 := by
intro x hx
rw [Finite.mem_toFinset, Function.mem_support] at hx
rw [ne_eq, zpow_eq_zero_iff hx, norm_eq_zero, sub_eq_zero, eq_comm]
apply ne_of_apply_ne D
rwa [h₂z]
simp only [Pi.smul_apply', Finset.prod_apply, Pi.pow_apply, norm_smul, norm_prod, norm_zpow]
rw [log_mul (Finset.prod_ne_zero_iff.2 this) (by simp [hg ⟨z, h₃z⟩]), log_prod _ _ this]
simp [log_zpow]
