Documentation

Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction

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 or Section 1.1 of Noguchi-Winkelmann, Nevanlinna Theory in Several Complex Variables and Diophantine Approximation for a detailed discussion.

TODO #

source
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.

Equations
Instances For

    Elementary Properties #

    source
    @[simp]
    theorem ValueDistribution.characteristic_sub_characteristic_eq_proximity_sub_proximity {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} (h : MeromorphicOn f Set.univ) (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.

    Behaviour under Arithmetic Operations #

    source
    theorem ValueDistribution.characteristic_mul_zero_le {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 ≠ ⊤) :
    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.

    source
    @[deprecated ValueDistribution.characteristic_mul_zero_le (since := "2025-12-11")]
    theorem ValueDistribution.characteristic_zero_mul_le {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 ≠ ⊤) :
    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.

    source
    theorem ValueDistribution.characteristic_mul_zero_eventuallyLE {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 ≠ ⊤) :
    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.

    source
    @[deprecated ValueDistribution.characteristic_mul_zero_eventuallyLE (since := "2025-12-11")]
    theorem ValueDistribution.characteristic_zero_mul_eventually_le {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 ≠ ⊤) :
    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.

    source
    theorem ValueDistribution.characteristic_mul_top_le {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 ≠ ⊤) :
    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.

    source
    @[deprecated ValueDistribution.characteristic_mul_top_le (since := "2025-12-11")]
    theorem ValueDistribution.characteristic_top_mul_le {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 ≠ ⊤) :
    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.

    source
    theorem ValueDistribution.characteristic_mul_top_eventuallyLE {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 ≠ ⊤) :
    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.

    source
    @[deprecated ValueDistribution.characteristic_mul_top_eventuallyLE (since := "2025-12-11")]
    theorem ValueDistribution.characteristic_top_mul_eventually_le {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 ≠ ⊤) :
    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.

    source
    @[simp]
    theorem ValueDistribution.characteristic_pow_zero {f : ℂ → ℂ} {n : ℕ} (hf : MeromorphicOn f Set.univ) :
    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.

    source
    @[simp]
    theorem ValueDistribution.characteristic_pow_top {f : ℂ → ℂ} {n : ℕ} (hf : MeromorphicOn f Set.univ) :
    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.