The Second Main Theorem of Value Distribution Theory

This file will, in the future, establish the second main theorem of Value Distribution Theory. At present, it collects material that will be used in the proof.

See Section VI.4 of Lang, Introduction to Complex Hyperbolic Spaces for a detailed discussion. A full formalized proof of the second main theorem is available at https://github.com/kebekus/ProjectVD

The Separation Lemma

This section proves the pointwise separation lemma, over a general normed field.

theorem Real.exists_sum_posLog_inv_norm_sub_le {𝕜 : Type u_1} [NormedField 𝕜] (s : Finset 𝕜) : ∃ (C : ℝ), ∀ (w : 𝕜), ∑ a ∈ s, ‖w - a‖⁻¹.posLog ≤ ‖∑ a ∈ s, (w - a)⁻¹‖.posLog + C

Separation lemma: for a finite set s of points, closeness to one point of s, measured by ∑ a ∈ s, log⁺ ‖· - a‖⁻¹, is detected by the single function log⁺ ‖∑ a ∈ s, (· - a)⁻¹‖, up to a constant depending only on s.