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 Section VI.2 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.

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 logarithmic counting function, which counts the number times that f attains the value a inside the disk ∣z∣ ≤ r, weighted by multiplicity.

Elementary Properties

theorem ValueDistribution.characteristic_congr_codiscrete {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : ℂ → E} {a : WithTop E} {r : ℝ} (hfg : f =ᶠ[Filter.codiscrete ℂ] g) (hr : r ≠ 0) : characteristic f a r = characteristic g a r

If two functions differ only on a discrete set, then their characteristic functions agree, except perhaps at radius 0.

@[simp]

theorem ValueDistribution.characteristic_sub_characteristic_eq_proximity_sub_proximity {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} (h : Meromorphic 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 for the poles of f and f - const simplifies to the difference between the proximity functions.

theorem ValueDistribution.characteristic_even {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {a : WithTop E} : Function.Even (characteristic f a)

The characteristic function is even.

theorem ValueDistribution.characteristic_nonneg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {a : WithTop E} {r : ℝ} (hr : 1 ≤ r) : 0 ≤ characteristic f a r

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

theorem ValueDistribution.characteristic_eventually_nonneg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {a : WithTop E} : 0 ≤ᶠ[Filter.atTop] characteristic f a

The characteristic function is asymptotically non-negative.

Behaviour under Arithmetic Operations

theorem ValueDistribution.characteristic_add_top_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f₁ f₂ : ℂ → E} {r : ℝ} (h₁f₁ : Meromorphic f₁) (h₁f₂ : Meromorphic f₂) (hr : 1 ≤ r) : characteristic (f₁ + f₂) ⊤ r ≤ characteristic f₁ ⊤ r + characteristic f₂ ⊤ r + Real.log 2

For 1 ≤ r, the characteristic function of f + g at ⊤ is less than or equal to the sum of the characteristic functions of f and g, respectively, plus log 2 (where 2 is the number of summands).

theorem ValueDistribution.characteristic_add_top_eventuallyLE {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f₁ f₂ : ℂ → E} (h₁f₁ : Meromorphic f₁) (h₁f₂ : Meromorphic f₂) : characteristic (f₁ + f₂) ⊤ ≤ᶠ[Filter.atTop] characteristic f₁ ⊤ + characteristic f₂ ⊤ + fun (x : ℝ) => Real.log 2

Asymptotically, the characteristic function of f + g at ⊤ is less than or equal to the sum of the characteristic functions of f and g, respectively.

theorem ValueDistribution.characteristic_sum_top_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {α : Type u_2} (s : Finset α) (f : α → ℂ → E) {r : ℝ} (hf : ∀ (a : α), Meromorphic (f a)) (hr : 1 ≤ r) : characteristic (∑ a ∈ s, f a) ⊤ r ≤ (∑ a ∈ s, characteristic (f a) ⊤) r + Real.log ↑s.card

For 1 ≤ r, the characteristic function of a sum ∑ a, f a at ⊤ is less than or equal to the sum of the characteristic functions of f ·, plus log s.card.

theorem ValueDistribution.characteristic_sum_top_eventuallyLE {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {α : Type u_2} (s : Finset α) (f : α → ℂ → E) (hf : ∀ (a : α), Meromorphic (f a)) : characteristic (∑ a ∈ s, f a) ⊤ ≤ᶠ[Filter.atTop] ∑ a ∈ s, characteristic (f a) ⊤ + fun (x : ℝ) => Real.log ↑s.card

Asymptotically, the characteristic function of a sum ∑ a, f a at ⊤ is less than or equal to the sum of the characteristic functions of f ·.

theorem ValueDistribution.characteristic_mul_zero_le {f₁ f₂ : ℂ → ℂ} {r : ℝ} (hr : 1 ≤ r) (h₁f₁ : Meromorphic f₁) (h₂f₁ : ∀ (z : ℂ), meromorphicOrderAt f₁ z ≠ ⊤) (h₁f₂ : Meromorphic f₂) (h₂f₂ : ∀ (z : ℂ), meromorphicOrderAt f₂ z ≠ ⊤) : characteristic (f₁ * f₂) 0 r ≤ (characteristic f₁ 0 + characteristic f₂ 0) r

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

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

theorem ValueDistribution.characteristic_zero_mul_le {f₁ f₂ : ℂ → ℂ} {r : ℝ} (hr : 1 ≤ r) (h₁f₁ : Meromorphic f₁) (h₂f₁ : ∀ (z : ℂ), meromorphicOrderAt f₁ z ≠ ⊤) (h₁f₂ : Meromorphic f₂) (h₂f₂ : ∀ (z : ℂ), meromorphicOrderAt f₂ z ≠ ⊤) : characteristic (f₁ * f₂) 0 r ≤ (characteristic f₁ 0 + characteristic f₂ 0) r

Alias of ValueDistribution.characteristic_mul_zero_le.

---

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

theorem ValueDistribution.characteristic_mul_zero_eventuallyLE {f₁ f₂ : ℂ → ℂ} (h₁f₁ : Meromorphic f₁) (h₂f₁ : ∀ (z : ℂ), meromorphicOrderAt f₁ z ≠ ⊤) (h₁f₂ : Meromorphic f₂) (h₂f₂ : ∀ (z : ℂ), meromorphicOrderAt f₂ z ≠ ⊤) : characteristic (f₁ * f₂) 0 ≤ᶠ[Filter.atTop] characteristic f₁ 0 + characteristic f₂ 0

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

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

theorem ValueDistribution.characteristic_zero_mul_eventually_le {f₁ f₂ : ℂ → ℂ} (h₁f₁ : Meromorphic f₁) (h₂f₁ : ∀ (z : ℂ), meromorphicOrderAt f₁ z ≠ ⊤) (h₁f₂ : Meromorphic f₂) (h₂f₂ : ∀ (z : ℂ), meromorphicOrderAt f₂ z ≠ ⊤) : characteristic (f₁ * f₂) 0 ≤ᶠ[Filter.atTop] characteristic f₁ 0 + characteristic f₂ 0

Alias of ValueDistribution.characteristic_mul_zero_eventuallyLE.

---

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

theorem ValueDistribution.characteristic_mul_top_le {f₁ f₂ : ℂ → ℂ} {r : ℝ} (hr : 1 ≤ r) (h₁f₁ : Meromorphic f₁) (h₂f₁ : ∀ (z : ℂ), meromorphicOrderAt f₁ z ≠ ⊤) (h₁f₂ : Meromorphic f₂) (h₂f₂ : ∀ (z : ℂ), meromorphicOrderAt f₂ z ≠ ⊤) : characteristic (f₁ * f₂) ⊤ r ≤ (characteristic f₁ ⊤ + characteristic f₂ ⊤) r

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

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

theorem ValueDistribution.characteristic_top_mul_le {f₁ f₂ : ℂ → ℂ} {r : ℝ} (hr : 1 ≤ r) (h₁f₁ : Meromorphic f₁) (h₂f₁ : ∀ (z : ℂ), meromorphicOrderAt f₁ z ≠ ⊤) (h₁f₂ : Meromorphic f₂) (h₂f₂ : ∀ (z : ℂ), meromorphicOrderAt f₂ z ≠ ⊤) : characteristic (f₁ * f₂) ⊤ r ≤ (characteristic f₁ ⊤ + characteristic f₂ ⊤) r

Alias of ValueDistribution.characteristic_mul_top_le.

---

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

theorem ValueDistribution.characteristic_mul_top_eventuallyLE {f₁ f₂ : ℂ → ℂ} (h₁f₁ : Meromorphic f₁) (h₂f₁ : ∀ (z : ℂ), meromorphicOrderAt f₁ z ≠ ⊤) (h₁f₂ : Meromorphic f₂) (h₂f₂ : ∀ (z : ℂ), meromorphicOrderAt f₂ z ≠ ⊤) : characteristic (f₁ * f₂) ⊤ ≤ᶠ[Filter.atTop] characteristic f₁ ⊤ + characteristic f₂ ⊤

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

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

theorem ValueDistribution.characteristic_top_mul_eventually_le {f₁ f₂ : ℂ → ℂ} (h₁f₁ : Meromorphic f₁) (h₂f₁ : ∀ (z : ℂ), meromorphicOrderAt f₁ z ≠ ⊤) (h₁f₂ : Meromorphic f₂) (h₂f₂ : ∀ (z : ℂ), meromorphicOrderAt f₂ z ≠ ⊤) : characteristic (f₁ * f₂) ⊤ ≤ᶠ[Filter.atTop] characteristic f₁ ⊤ + characteristic f₂ ⊤

Alias of ValueDistribution.characteristic_mul_top_eventuallyLE.

---

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

@[simp]

theorem ValueDistribution.characteristic_pow_zero {f : ℂ → ℂ} {n : ℕ} (hf : Meromorphic f) : characteristic (f ^ n) 0 = n • characteristic f 0

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

@[simp]

theorem ValueDistribution.characteristic_pow_top {f : ℂ → ℂ} {n : ℕ} (hf : Meromorphic f) : characteristic (f ^ n) ⊤ = n • characteristic f ⊤

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