Documentation

Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

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.

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 #

Second Part of the First Main Theorem #

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.

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.