English
At zero, the difference between the characteristic functions equals log ‖f 0‖.
Русский
В нуле разность характеристических функций равна log ‖f(0)‖.
LaTeX
$$$\text{characteristic}(f)\top 0 - \text{characteristic}(f^{-1})\top 0 = \log\|f(0)\|$$$
Lean4
/-- Helper lemma for the first part of the First Main Theorem: Away from zero, the difference between
the characteristic functions of `f` and `f⁻¹` equals `log ‖meromorphicTrailingCoeffAt f 0‖`.
-/
theorem characteristic_sub_characteristic_inv_of_ne_zero (hf : MeromorphicOn f Set.univ) (hR : R ≠ 0) :
characteristic f ⊤ R - characteristic f⁻¹ ⊤ R = log ‖meromorphicTrailingCoeffAt f 0‖ := by
calc
characteristic f ⊤ R - characteristic f⁻¹ ⊤ R
_ = (characteristic f ⊤ - characteristic f⁻¹ ⊤) R := by simp
_ = circleAverage (log ‖f ·‖) 0 R - (divisor f Set.univ).logCounting R :=
by
rw [characteristic_sub_characteristic_inv hf]
rfl
_ = log ‖meromorphicTrailingCoeffAt f 0‖ :=
by
rw [MeromorphicOn.circleAverage_log_norm hR (hf.mono_set (by tauto))]
unfold Function.locallyFinsuppWithin.logCounting
have : (divisor f (closedBall 0 |R|)) = (divisor f Set.univ).toClosedBall R :=
(divisor_restrict hf (by tauto)).symm
simp [this, toClosedBall, restrictMonoidHom, restrict_apply]
