English
The difference between the characteristic functions of f and f⁻¹ is related to a circle-average of log norms and to the divisor’s logCounting, as formalized in the first main theorem.
Русский
Разность характеристических функций f и f⁻¹ связана с окружной средней по нормам и логарифмическим счётом делителя, как формулируется в первую главную теорему.
LaTeX
$$$\text{characteristic}(f) - \text{characteristic}(f^{-1}) = \text{circleAverage}(\log\|f\|) - (\text{divisor } f)\logCounting$$$
Lean4
/-- Helper lemma for the first part of the First Main Theorem: Given a meromorphic function `f`, compute
difference between the characteristic functions of `f` and of its inverse.
-/
theorem characteristic_sub_characteristic_inv (h : MeromorphicOn f ⊤) :
characteristic f ⊤ - characteristic f⁻¹ ⊤ = circleAverage (log ‖f ·‖) 0 - (divisor f Set.univ).logCounting := by
calc
characteristic f ⊤ - characteristic f⁻¹ ⊤
_ = proximity f ⊤ - proximity f⁻¹ ⊤ - (logCounting f⁻¹ ⊤ - logCounting f ⊤) :=
by
unfold characteristic
ring
_ = circleAverage (log ‖f ·‖) 0 - (logCounting f⁻¹ ⊤ - logCounting f ⊤) := by
rw [proximity_sub_proximity_inv_eq_circleAverage h]
_ = circleAverage (log ‖f ·‖) 0 - (logCounting f 0 - logCounting f ⊤) := by rw [logCounting_inv]
_ = circleAverage (log ‖f ·‖) 0 - (divisor f Set.univ).logCounting := by
rw [← ValueDistribution.log_counting_zero_sub_logCounting_top]
