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 SectionVI.1 of Lang: Introduction to Complex Hyperbolic
Spaces or Section1.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 #
- 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 #
Shorthand notation for the restriction of a function with locally finite support within Set.univ
to the closed unit ball of radius r
.
Equations
Instances For
The Logarithmic Counting Function of a Function with Locally Finite Support #
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 a real 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 theorms of
Value Distribution Theory. We refer the reader to page 164 of Lang: Introduction to Complex
Hyperbolic Spaces for more details.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Evaluation of the logarithmic counting function at zero yields zero.
The Logarithmic Counting Function of a Meromorphic Function #
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.
Instances For
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โ
.
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โ
.
The logarithmic counting function logCounting f 0
is the counting function associated with the
zero-divisor of f
.
The logarithmic counting function logCounting f โค
is the counting function associated with
the pole-divisor of f
.
Evaluation of the logarithmic counting function at zero yields zero.
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 #
Relation between the logarithmic counting function of f
and of fโปยน
.
Adding an analytic function does not change the counting function counting poles.
Special case of logCounting_add_analyticOn
: Adding a constant does not change the counting
function counting poles.
Special case of logCounting_add_analyticOn
: Subtracting a constant does not change the counting
function counting poles.