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 : MeromorphicOn 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 : MeromorphicOn f Set.univ) (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 : MeromorphicOn f Set.univ) : 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 : MeromorphicOn f Set.univ) : |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 : MeromorphicOn 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 : MeromorphicOn 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 : MeromorphicOn 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.

@[deprecated ValueDistribution.isBigO_characteristic_sub_characteristic_shift (since := "2025-10-06")]

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

Alias of ValueDistribution.isBigO_characteristic_sub_characteristic_shift.

---

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.