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][MR886677].

• 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][MR886677]

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

• Formalize the first part of the First Main Theorem, which is the more substantial part of the statement.

Second Part of the First Main Theorem

theorem ValueDistribution.abs_characteristic_sub_characteristic_shift_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {a₀ : 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.abs_characteristic_sub_characteristic_shift_eqO {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {a₀ : 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.