English
For finite a0, logCounting f a0 equals the logCounting associated to the divisor of (f − a0).
Русский
Для конечного a0 логарифмическая счетная функция f a0 эквивалентна logCounting, связанной с делителем (f − a0).
LaTeX
$$$\logCounting f a_0 = (\text{divisor }(f- a_0)\, univ)^{+}.\logCounting$$$
Lean4
/-- The logarithmic counting function of a meromorphic function.
If `f : 𝕜 → E` is meromorphic and `a : WithTop E` is any value, this is a logarithmically weighted
measure of the number of times the function `f` takes a given value `a` within the disk `∣z∣ ≤ r`,
counting multiplicities. In the special case where `a = ⊤`, it counts the poles of `f`.
-/
noncomputable def logCounting : ℝ → ℝ := by
by_cases h : a = ⊤
· exact (divisor f univ)⁻.logCounting
· exact (divisor (fun z ↦ f z - a.untop₀) univ)⁺.logCounting
