The First Main Theorem of Value Distribution Theory

The First Main Theorem of Value Distribution Theory is a two-part statement, establishing invariance of the characteristic function characteristic f ⊤ under modifications of f.

• If f is meromorphic on the complex plane, then the characteristic functions for the value ⊤ of the function f and f⁻¹ agree up to a constant, see Proposition 2.1 on p. 168 of Lang, Introduction to Complex Hyperbolic Spaces.

• If f is meromorphic on the complex plane, then the characteristic functions for the value ⊤ of the function f and f - const agree up to a constant, see Proposition 2.2 on p. 168 of Lang, Introduction to Complex Hyperbolic Spaces

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.

First Part of the First Main Theorem

theorem ValueDistribution.characteristic_sub_characteristic_inv {f : ℂ → ℂ} (h : Meromorphic f) : characteristic f ⊤ - characteristic f⁻¹ ⊤ = Real.circleAverage (fun (x : ℂ) => Real.log ‖f x‖) 0 - Function.locallyFinsuppWithin.logCounting (MeromorphicOn.divisor f Set.univ)

Helper lemma for the first part of the First Main Theorem: Given a meromorphic function f, compute difference between the characteristic functions of f and of its inverse.

theorem ValueDistribution.characteristic_sub_characteristic_inv_of_ne_zero {f : ℂ → ℂ} {R : ℝ} (hf : Meromorphic f) (hR : R ≠ 0) : characteristic f ⊤ R - characteristic f⁻¹ ⊤ R = Real.log ‖meromorphicTrailingCoeffAt f 0‖

Helper lemma for the first part of the First Main Theorem: Away from zero, the difference between the characteristic functions of f and f⁻¹ equals log ‖meromorphicTrailingCoeffAt f 0‖.

theorem ValueDistribution.characteristic_sub_characteristic_inv_at_zero {f : ℂ → ℂ} (h : Meromorphic f) : characteristic f ⊤ 0 - characteristic f⁻¹ ⊤ 0 = Real.log ‖f 0‖

Helper lemma for the first part of the First Main Theorem: At 0, the difference between the characteristic functions of f and f⁻¹ equals log ‖f 0‖.

theorem ValueDistribution.characteristic_sub_characteristic_inv_le {f : ℂ → ℂ} {R : ℝ} (hf : Meromorphic f) : |characteristic f ⊤ R - characteristic f⁻¹ ⊤ R| ≤ max |Real.log ‖f 0‖| |Real.log ‖meromorphicTrailingCoeffAt f 0‖|

First part of the First Main Theorem, quantitative version: If f is meromorphic on the complex plane, then the difference between the characteristic functions of f and f⁻¹ is bounded by an explicit constant.

theorem ValueDistribution.isBigO_characteristic_sub_characteristic_inv {f : ℂ → ℂ} (h : Meromorphic f) : (characteristic f ⊤ - characteristic f⁻¹ ⊤) =O[Filter.atTop] 1

First part of the First Main Theorem, qualitative version: If f is meromorphic on the complex plane, then the characteristic functions of f and f⁻¹ agree asymptotically up to a bounded function.

Second Part of the First Main Theorem

theorem ValueDistribution.abs_characteristic_sub_characteristic_shift_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {a₀ : E} {f : ℂ → E} {r : ℝ} (h : Meromorphic f) : |characteristic f ⊤ r - characteristic (fun (x : ℂ) => f x - a₀) ⊤ r| ≤ ‖a₀‖.posLog + Real.log 2

Second part of the First Main Theorem of Value Distribution Theory, quantitative version: If f is meromorphic on the complex plane, then the characteristic functions (for value ⊤) of f and f - a₀ differ at most by log⁺ ‖a₀‖ + log 2.

theorem ValueDistribution.isBigO_characteristic_sub_characteristic_shift {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {a₀ : E} {f : ℂ → E} (h : Meromorphic f) : (characteristic f ⊤ - characteristic (fun (x : ℂ) => f x - a₀) ⊤) =O[Filter.atTop] 1

Second part of the First Main Theorem of Value Distribution Theory, qualitative version: If f is meromorphic on the complex plane, then the characteristic functions for the value ⊤ of the function f and f - a₀ agree asymptotically up to a bounded function.

Postcomposition with an Automorphism of the Projective Line

theorem ValueDistribution.isBigO_characteristic_sub_characteristic_moebius {a b c d : ℂ} {f : ℂ → ℂ} (hf : Meromorphic f) (hΔ : a * d - b * c ≠ 0) : (characteristic f ⊤ - characteristic ((fun (x : ℂ) => a * f x + b) / fun (x : ℂ) => c * f x + d) ⊤) =O[Filter.atTop] 1

Reformulation of the first main theorem: Postcomposing a meromorphic function f : ℂ → ℂ with a Moebius transformation (=an automorphism of the projective line) changes the characteristic function for the value ⊤ only by a bounded function.