The Logarithmic Counting Function of Value Distribution Theory

For nontrivially normed fields 𝕜, this file defines the logarithmic counting function of a meromorphic function defined on 𝕜. Also known as the Nevanlinna counting function, this is one of the three main functions used in Value Distribution Theory.

The logarithmic counting function of a meromorphic function f is a logarithmically weighted measure of the number of times the function f takes a given value a within the disk ∣z∣ ≤ r, taking multiplicities into account.

See Section VI.1 of Lang, Introduction to Complex Hyperbolic Spaces or Section 1.1 of Noguchi-Winkelmann, Nevanlinna Theory in Several Complex Variables and Diophantine Approximation for a detailed discussion.

Implementation Notes

• This file defines the logarithmic counting function first for functions with locally finite support on 𝕜 and then specializes to the setting where the function with locally finite support is the pole or zero-divisor of a meromorphic function.

• Even though value distribution theory is best developed for meromorphic functions on the complex plane (and therefore placed in the complex analysis section of Mathlib), we introduce the logarithmic counting function for arbitrary normed fields.

TODO

• Discuss the logarithmic counting function for rational functions, add a forward reference to the upcoming converse, formulated in terms of the Nevanlinna height.

Supporting Notation

noncomputable def Function.locallyFinsuppWithin.toClosedBall {E : Type u_1} [NormedAddCommGroup E] (r : ℝ) : locallyFinsuppWithin Set.univ ℤ →+ locallyFinsuppWithin (Metric.closedBall 0 |r|) ℤ

Shorthand notation for the restriction of a function with locally finite support within Set.univ to the closed unit ball of radius r.

Equations

• Function.locallyFinsuppWithin.toClosedBall r = Function.locallyFinsuppWithin.restrictMonoidHom ⋯

@[simp]

theorem Function.locallyFinsuppWithin.toClosedBall_eval_within {E : Type u_1} [NormedAddCommGroup E] {r : ℝ} {z : E} (f : locallyFinsuppWithin Set.univ ℤ) (ha : z ∈ Metric.closedBall 0 |r|) : ((toClosedBall r) f) z = f z

@[simp]

theorem Function.locallyFinsuppWithin.toClosedBall_divisor {r : ℝ} {f : ℂ → ℂ} (h : MeromorphicOn f Set.univ) : MeromorphicOn.divisor f (Metric.closedBall 0 |r|) = (toClosedBall r) (MeromorphicOn.divisor f Set.univ)

The Logarithmic Counting Function of a Function with Locally Finite Support

noncomputable def Function.locallyFinsuppWithin.logCounting {E : Type u_2} [NormedAddCommGroup E] [ProperSpace E] : locallyFinsuppWithin Set.univ ℤ →+ ℝ → ℝ

Definition of the logarithmic counting function, as a group morphism mapping functions D with locally finite support to maps ℝ → ℝ. Given D, the result map logCounting D takes r : ℝ to a logarithmically weighted measure of values that D takes within the disk ∣z∣ ≤ r.

Implementation Note: In case where z = 0, the term log (r * ‖z‖⁻¹) evaluates to zero, which is typically different from log r - log ‖z‖ = log r. The summand (D 0) * log r compensates this, producing cleaner formulas when the logarithmic counting function is used in the main theorems of Value Distribution Theory. We refer the reader to page 164 of Lang: Introduction to Complex Hyperbolic Spaces for more details, and to the lemma countingFunction_finsum_eq_finsum_add in Mathlib/Analysis/Complex/JensenFormula.lean for a formal statement.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Function.locallyFinsuppWithin.logCounting_eval_zero {E : Type u_2} [NormedAddCommGroup E] [ProperSpace E] (D : locallyFinsuppWithin Set.univ ℤ) : logCounting D 0 = 0

Evaluation of the logarithmic counting function at zero yields zero.

theorem Function.locallyFinsuppWithin.logCounting_nonneg {E : Type u_2} [NormedAddCommGroup E] [ProperSpace E] {f : locallyFinsuppWithin Set.univ ℤ} {r : ℝ} (h : 0 ≤ f) (hr : 1 ≤ r) : 0 ≤ logCounting f r

For 1 ≤ r, the logarithmic counting function is non-negative.

theorem Function.locallyFinsuppWithin.logCounting_le {E : Type u_2} [NormedAddCommGroup E] [ProperSpace E] {f₁ f₂ : locallyFinsuppWithin Set.univ ℤ} {r : ℝ} (h : f₁ ≤ f₂) (hr : 1 ≤ r) : logCounting f₁ r ≤ logCounting f₂ r

For 1 ≤ r, the logarithmic counting function respects the ≤ relation.

theorem Function.locallyFinsuppWithin.logCounting_eventuallyLE {E : Type u_2} [NormedAddCommGroup E] [ProperSpace E] {f₁ f₂ : locallyFinsuppWithin Set.univ ℤ} (h : f₁ ≤ f₂) : logCounting f₁ ≤ᶠ[Filter.atTop] logCounting f₂

The logarithmic counting function respects the ≤ relation asymptotically.

@[deprecated Function.locallyFinsuppWithin.logCounting_eventuallyLE (since := "2025-12-11")]

theorem Function.locallyFinsuppWithin.logCounting_eventually_le {E : Type u_2} [NormedAddCommGroup E] [ProperSpace E] {f₁ f₂ : locallyFinsuppWithin Set.univ ℤ} (h : f₁ ≤ f₂) : logCounting f₁ ≤ᶠ[Filter.atTop] logCounting f₂

Alias of Function.locallyFinsuppWithin.logCounting_eventuallyLE.

---

The logarithmic counting function respects the ≤ relation asymptotically.

The Logarithmic Counting Function of a Meromorphic Function

noncomputable def ValueDistribution.logCounting {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : 𝕜 → E) (a : WithTop E) : ℝ → ℝ

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, taking multiplicities into account. In the special case where a = ⊤, it counts the poles of f.

Equations

• One or more equations did not get rendered due to their size.

theorem locallyFinsuppWithin.logCounting_divisor {f : ℂ → ℂ} : Function.locallyFinsuppWithin.logCounting (MeromorphicOn.divisor f ⊤) = ValueDistribution.logCounting f 0 - ValueDistribution.logCounting f ⊤

Relation between ValueDistribution.logCounting and locallyFinsuppWithin.logCounting.

theorem ValueDistribution.logCounting_coe {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {a₀ : E} : logCounting f ↑a₀ = Function.locallyFinsuppWithin.logCounting (MeromorphicOn.divisor (fun (z : 𝕜) => f z - a₀) Set.univ)⁺

For finite values a₀, the logarithmic counting function logCounting f a₀ is the logarithmic counting function for the zeros of f - a₀.

theorem ValueDistribution.logCounting_coe_eq_logCounting_sub_const_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {a₀ : E} : logCounting f ↑a₀ = logCounting (f - fun (x : 𝕜) => a₀) 0

For finite values a₀, the logarithmic counting function logCounting f a₀ equals the logarithmic counting function for the zeros of f - a₀.

theorem ValueDistribution.logCounting_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} : logCounting f 0 = Function.locallyFinsuppWithin.logCounting (MeromorphicOn.divisor f Set.univ)⁺

The logarithmic counting function logCounting f 0 is the logarithmic counting function associated with the zero-divisor of f.

theorem ValueDistribution.logCounting_top {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} : logCounting f ⊤ = Function.locallyFinsuppWithin.logCounting (MeromorphicOn.divisor f Set.univ)⁻

The logarithmic counting function logCounting f ⊤ is the logarithmic counting function associated with the pole-divisor of f.

@[simp]

theorem ValueDistribution.logCounting_eval_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {a : WithTop E} : logCounting f a 0 = 0

Evaluation of the logarithmic counting function at zero yields zero.

theorem ValueDistribution.log_counting_zero_sub_logCounting_top {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} : Function.locallyFinsuppWithin.logCounting (MeromorphicOn.divisor f Set.univ) = logCounting f 0 - logCounting f ⊤

The logarithmic counting function associated with the divisor of f is the difference between logCounting f 0 and logCounting f ⊤.

@[simp]

theorem ValueDistribution.logCounting_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : E} {e : WithTop E} : logCounting (fun (x : 𝕜) => c) e = 0

The logarithmic counting function of a constant function is zero.

@[simp]

theorem ValueDistribution.logCounting_const_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {e : WithTop E} : logCounting 0 e = 0

The logarithmic counting function of the constant function zero is zero.

Elementary Properties of the Logarithmic Counting Function

@[simp]

theorem ValueDistribution.logCounting_inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {f : 𝕜 → 𝕜} : logCounting f⁻¹ ⊤ = logCounting f 0

Relation between the logarithmic counting functions of f and of f⁻¹.

theorem ValueDistribution.logCounting_add_analyticOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f g : 𝕜 → E} (hf : MeromorphicOn f Set.univ) (hg : AnalyticOn 𝕜 g Set.univ) : logCounting (f + g) ⊤ = logCounting f ⊤

Adding an analytic function does not change the logarithmic counting function for the poles.

@[simp]

theorem ValueDistribution.logCounting_add_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {a₀ : E} (hf : MeromorphicOn f Set.univ) : logCounting (f + fun (x : 𝕜) => a₀) ⊤ = logCounting f ⊤

Special case of logCounting_add_analyticOn: Adding a constant does not change the logarithmic counting function for the poles.

@[simp]

theorem ValueDistribution.logCounting_sub_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {a₀ : E} (hf : MeromorphicOn f Set.univ) : logCounting (f - fun (x : 𝕜) => a₀) ⊤ = logCounting f ⊤

Special case of logCounting_add_analyticOn: Subtracting a constant does not change the logarithmic counting function for the poles.

Behaviour under Arithmetic Operations

theorem ValueDistribution.logCounting_add_top_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f₁ f₂ : 𝕜 → E} {r : ℝ} (h₁f₁ : MeromorphicOn f₁ Set.univ) (h₁f₂ : MeromorphicOn f₂ Set.univ) (hr : 1 ≤ r) : logCounting (f₁ + f₂) ⊤ r ≤ (logCounting f₁ ⊤ + logCounting f₂ ⊤) r

For 1 ≤ r, the logarithmic counting function for the poles of f + g is less than or equal to the sum of the logarithmic counting functions for the poles of f and g, respectively.

theorem ValueDistribution.logCounting_add_top_eventuallyLE {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f₁ f₂ : 𝕜 → E} (h₁f₁ : MeromorphicOn f₁ Set.univ) (h₁f₂ : MeromorphicOn f₂ Set.univ) : logCounting (f₁ + f₂) ⊤ ≤ᶠ[Filter.atTop] logCounting f₁ ⊤ + logCounting f₂ ⊤

Asymptotically, the logarithmic counting function for the poles of f + g is less than or equal to the sum of the logarithmic counting functions for the poles of f and g, respectively.

theorem ValueDistribution.logCounting_sum_top_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {α : Type u_3} (s : Finset α) (f : α → 𝕜 → E) {r : ℝ} (h₁f : ∀ (a : α), MeromorphicOn (f a) Set.univ) (hr : 1 ≤ r) : logCounting (∑ a ∈ s, f a) ⊤ r ≤ (∑ a ∈ s, logCounting (f a) ⊤) r

For 1 ≤ r, the logarithmic counting function for the poles of a sum ∑ a ∈ s, f a is less than or equal to the sum of the logarithmic counting functions for the poles of the f ·.

theorem ValueDistribution.logCounting_sum_top_eventuallyLE {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {α : Type u_3} (s : Finset α) (f : α → 𝕜 → E) (h₁f : ∀ (a : α), MeromorphicOn (f a) Set.univ) : logCounting (∑ a ∈ s, f a) ⊤ ≤ᶠ[Filter.atTop] ∑ a ∈ s, logCounting (f a) ⊤

Asymptotically, the logarithmic counting function for the poles of a sum ∑ a ∈ s, f a is less than or equal to the sum of the logarithmic counting functions for the poles of the f ·.

theorem ValueDistribution.logCounting_mul_zero_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {f₁ f₂ : 𝕜 → 𝕜} {r : ℝ} (hr : 1 ≤ r) (h₁f₁ : MeromorphicOn f₁ Set.univ) (h₂f₁ : ∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤) (h₁f₂ : MeromorphicOn f₂ Set.univ) (h₂f₂ : ∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤) : logCounting (f₁ * f₂) 0 r ≤ (logCounting f₁ 0 + logCounting f₂ 0) r

For 1 ≤ r, the logarithmis counting function for the zeros of f * g is less than or equal to the sum of the logarithmic counting functions for the zeros of f and g, respectively.

Note: The statement proven here is found at the top of page 169 of Lang: Introduction to Complex Hyperbolic Spaces where it is written as an inequality between functions. This could be interpreted as claiming that the inequality holds for ALL values of r, which is not true. For a counterexample, take f₁ : z → z and f₂ : z → z⁻¹. Then,

• logCounting f₁ 0 = log
• logCounting f₂ 0 = 0
• logCounting (f₁ * f₂) 0 = 0

But log r is negative for small r.

@[deprecated ValueDistribution.logCounting_mul_zero_le (since := "2025-12-11")]

theorem ValueDistribution.logCounting_zero_mul_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {f₁ f₂ : 𝕜 → 𝕜} {r : ℝ} (hr : 1 ≤ r) (h₁f₁ : MeromorphicOn f₁ Set.univ) (h₂f₁ : ∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤) (h₁f₂ : MeromorphicOn f₂ Set.univ) (h₂f₂ : ∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤) : logCounting (f₁ * f₂) 0 r ≤ (logCounting f₁ 0 + logCounting f₂ 0) r

Alias of ValueDistribution.logCounting_mul_zero_le.

---

For 1 ≤ r, the logarithmis counting function for the zeros of f * g is less than or equal to the sum of the logarithmic counting functions for the zeros of f and g, respectively.

Note: The statement proven here is found at the top of page 169 of Lang: Introduction to Complex Hyperbolic Spaces where it is written as an inequality between functions. This could be interpreted as claiming that the inequality holds for ALL values of r, which is not true. For a counterexample, take f₁ : z → z and f₂ : z → z⁻¹. Then,

• logCounting f₁ 0 = log
• logCounting f₂ 0 = 0
• logCounting (f₁ * f₂) 0 = 0

But log r is negative for small r.

theorem ValueDistribution.logCounting_mul_zero_eventuallyLE {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {f₁ f₂ : 𝕜 → 𝕜} (h₁f₁ : MeromorphicOn f₁ Set.univ) (h₂f₁ : ∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤) (h₁f₂ : MeromorphicOn f₂ Set.univ) (h₂f₂ : ∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤) : logCounting (f₁ * f₂) 0 ≤ᶠ[Filter.atTop] logCounting f₁ 0 + logCounting f₂ 0

Asymptotically, the logarithmic counting function for the zeros of f * g is less than or equal to the sum of the logarithmic counting functions for the zeros of f and g, respectively.

@[deprecated ValueDistribution.logCounting_mul_zero_eventuallyLE (since := "2025-12-11")]

theorem ValueDistribution.logCounting_zero_mul_eventually_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {f₁ f₂ : 𝕜 → 𝕜} (h₁f₁ : MeromorphicOn f₁ Set.univ) (h₂f₁ : ∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤) (h₁f₂ : MeromorphicOn f₂ Set.univ) (h₂f₂ : ∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤) : logCounting (f₁ * f₂) 0 ≤ᶠ[Filter.atTop] logCounting f₁ 0 + logCounting f₂ 0

Alias of ValueDistribution.logCounting_mul_zero_eventuallyLE.

---

Asymptotically, the logarithmic counting function for the zeros of f * g is less than or equal to the sum of the logarithmic counting functions for the zeros of f and g, respectively.

theorem ValueDistribution.logCounting_mul_top_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {f₁ f₂ : 𝕜 → 𝕜} {r : ℝ} (hr : 1 ≤ r) (h₁f₁ : MeromorphicOn f₁ Set.univ) (h₂f₁ : ∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤) (h₁f₂ : MeromorphicOn f₂ Set.univ) (h₂f₂ : ∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤) : logCounting (f₁ * f₂) ⊤ r ≤ (logCounting f₁ ⊤ + logCounting f₂ ⊤) r

For 1 ≤ r, the logarithmic counting function for the poles of f * g is less than or equal to the sum of the logarithmic counting functions for the poles of f and g, respectively.

@[deprecated ValueDistribution.logCounting_mul_top_le (since := "2025-12-11")]

theorem ValueDistribution.logCounting_top_mul_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {f₁ f₂ : 𝕜 → 𝕜} {r : ℝ} (hr : 1 ≤ r) (h₁f₁ : MeromorphicOn f₁ Set.univ) (h₂f₁ : ∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤) (h₁f₂ : MeromorphicOn f₂ Set.univ) (h₂f₂ : ∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤) : logCounting (f₁ * f₂) ⊤ r ≤ (logCounting f₁ ⊤ + logCounting f₂ ⊤) r

Alias of ValueDistribution.logCounting_mul_top_le.

---

For 1 ≤ r, the logarithmic counting function for the poles of f * g is less than or equal to the sum of the logarithmic counting functions for the poles of f and g, respectively.

theorem ValueDistribution.logCounting_mul_top_eventuallyLE {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {f₁ f₂ : 𝕜 → 𝕜} (h₁f₁ : MeromorphicOn f₁ Set.univ) (h₂f₁ : ∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤) (h₁f₂ : MeromorphicOn f₂ Set.univ) (h₂f₂ : ∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤) : logCounting (f₁ * f₂) ⊤ ≤ᶠ[Filter.atTop] logCounting f₁ ⊤ + logCounting f₂ ⊤

Asymptotically, the logarithmic counting function for the zeros of f * g is less than or equal to the sum of the logarithmic counting functions for the zeros of f and g, respectively.

@[deprecated ValueDistribution.logCounting_mul_top_eventuallyLE (since := "2025-12-11")]

theorem ValueDistribution.logCounting_top_mul_eventually_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {f₁ f₂ : 𝕜 → 𝕜} (h₁f₁ : MeromorphicOn f₁ Set.univ) (h₂f₁ : ∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤) (h₁f₂ : MeromorphicOn f₂ Set.univ) (h₂f₂ : ∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤) : logCounting (f₁ * f₂) ⊤ ≤ᶠ[Filter.atTop] logCounting f₁ ⊤ + logCounting f₂ ⊤

Alias of ValueDistribution.logCounting_mul_top_eventuallyLE.

---

Asymptotically, the logarithmic counting function for the zeros of f * g is less than or equal to the sum of the logarithmic counting functions for the zeros of f and g, respectively.

@[simp]

theorem ValueDistribution.logCounting_pow_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {f : 𝕜 → 𝕜} {n : ℕ} (hf : MeromorphicOn f Set.univ) : logCounting (f ^ n) 0 = n • logCounting f 0

For natural numbers n, the logarithmic counting function for the zeros of f ^ n equals n times the logarithmic counting function for the zeros of f.

@[simp]

theorem ValueDistribution.logCounting_pow_top {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {f : 𝕜 → 𝕜} {n : ℕ} (hf : MeromorphicOn f Set.univ) : logCounting (f ^ n) ⊤ = n • logCounting f ⊤

For natural numbers n, the logarithmic counting function for the poles of f ^ n equals n times the logarithmic counting function for the poles of f.

Representation by Integrals

For 𝕜 = ℂ, the theorems below describe the logarithmic counting function in terms of circle averages.

theorem Function.locallyFinsuppWithin.logCounting_divisor_eq_circleAverage_sub_const {R : ℝ} {f : ℂ → ℂ} (h : MeromorphicOn f ⊤) (hR : R ≠ 0) : logCounting (MeromorphicOn.divisor f ⊤) R = Real.circleAverage (fun (x : ℂ) => Real.log ‖f x‖) 0 R - Real.log ‖meromorphicTrailingCoeffAt f 0‖

Over the complex numbers, present the logarithmic counting function attached to the divisor of a meromorphic function f as a circle average over log ‖f ·‖.

This is a reformulation of Jensen's formula of complex analysis. See MeromorphicOn.circleAverage_log_norm for Jensen's formula in the original context.

theorem ValueDistribution.logCounting_zero_sub_logCounting_top_eq_circleAverage_sub_const {R : ℝ} {f : ℂ → ℂ} (h : MeromorphicOn f ⊤) (hR : R ≠ 0) : (logCounting f 0 - logCounting f ⊤) R = Real.circleAverage (fun (x : ℂ) => Real.log ‖f x‖) 0 R - Real.log ‖meromorphicTrailingCoeffAt f 0‖

Variant of locallyFinsuppWithin.logCounting_divisor_eq_circleAverage_sub_const, using ValueDistribution.logCounting instead of locallyFinsuppWithin.logCounting.