The Characteristic Function of Value Distribution Theory

This file defines the "characteristic function" attached to a meromorphic function defined on the complex plane. Also known as "Nevanlinna Height", this is one of the three main functions used in Value Distribution Theory.

The characteristic function plays a role analogous to the height function in number theory: both measure the "complexity" of objects. For rational functions, the characteristic function grows like the degree times the logarithm, much like the logarithmic height in number theory reflects the degree of an algebraic number.

See SectionVI.2 of [Lang, Introduction to Complex Hyperbolic Spaces][MR886677] or Section1.1 of [Noguchi-Winkelmann, Nevanlinna Theory in Several Complex Variables and Diophantine Approximation][MR3156076] for a detailed discussion.

TODO

• Characterize rational functions in terms of the growth rate of their characteristic function, as discussed in Theorem 2.6 on p. 170 of [Lang, Introduction to Complex Hyperbolic Spaces][MR886677].

noncomputable def ValueDistribution.characteristic {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (a : WithTop E) : ℝ → ℝ

The Characteristic Function of Value Distribution Theory

If f : ℂ → E is meromorphic and a : WithTop E is any value, the characteristic function of f is defined as the sum of two terms: the proximity function, which quantifies how close f gets to a on the circle ∣z∣ = r, and the counting function, which counts the number times that f attains the value a inside the disk ∣z∣ ≤ r, weighted by multiplicity.

Equations

• ValueDistribution.characteristic f a = ValueDistribution.proximity f a + ValueDistribution.logCounting f a

Elementary Properties

@[simp]

theorem ValueDistribution.characteristic_sub_characteristic_eq_proximity_sub_proximity {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} (h : MeromorphicOn f ⊤) (a₀ : E) : characteristic f ⊤ - characteristic (fun (x : ℂ) => f x - a₀) ⊤ = proximity f ⊤ - proximity (fun (x : ℂ) => f x - a₀) ⊤

The difference between the characteristic functions of f and f - const simplifies to the difference between the proximity functions.