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][MR886677] or Section~1.1 of [Noguchi-Winkelmann, Nevanlinna Theory in Several Complex Variables and Diophantine Approximation][MR3156076] 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

• For 𝕜 = ℂ, add the integral presentation of the logarithmic counting function
• Discuss the counting function for rational functions, add a forward reference to the upcoming converse, formulated in terms of the Nevanlinna height.
• Counting function of powers.

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.

The Logarithmic Counting Function of a Function with Locally Finite Support

noncomputable def Function.locallyFinsuppWithin.logCounting {E : Type u_1} [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 for a formal statement.

theorem Function.locallyFinsuppWithin.countingFunction_finsum_eq_finsum_add {R : ℝ} {D : ℂ → ℤ} (hR : R ≠ 0) (hD : (Function.support D).Finite) : ∑ᶠ (u : ℂ), ↑(D u) * (Real.log R - Real.log ‖u‖) = ∑ᶠ (u : ℂ), ↑(D u) * Real.log (R * ‖u‖⁻¹) + ↑(D 0) * Real.log R

Alternate presentation of the finsum that appears in the definition of the counting function.

@[simp]

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

Evaluation of the logarithmic counting function at zero yields zero.

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.

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.