The 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 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, counting multiplicities.

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 counting function for arbitrary normed fields.

TODO

• Discuss the 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 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 counting function respects the ≤ relation.

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₂

The 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, counting multiplicities. 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 counting function associated with the zero-divisor of the meromorphic function 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 value zero of the shifted function 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 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 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 counting function associated with the divisor of f is the difference between logCounting f 0 and logCounting f ⊤.

Elementary Properties of the Counting Function

@[simp]

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

Relation between the logarithmic counting function 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 counting function counting 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 counting function counting 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 counting function counting poles.

Behaviour under Arithmetic Operations

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

For 1 ≤ r, the counting function counting zeros of f * g is less than or equal to the sum of the counting functions counting 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_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

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

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

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

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₂ ⊤

Asymptotically, the counting function counting zeros of f * g is less than or equal to the sum of the counting functions counting 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 counting function counting zeros of f ^ n equals n times the counting function counting 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 counting function counting poles of f ^ n equals n times the counting function counting 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.