feat: first main theorem of value distribution theory (#30103)

Establish the first main theorem of value distribution theory in full.

This PR completes a major milestone in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane.

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

Author: kebekus

Mathlib/Analysis/Complex/ValueDistribution/FirstMainTheorem.lean

@@ -3,6 +3,7 @@ Copyright (c) 2025 Stefan Kebekus. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Stefan Kebekus
 -/
+import Mathlib.Analysis.Complex.JensenFormula
 import Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
 
 /-!
@@ -22,19 +23,99 @@ of the characteristic function `characteristic f ⊤` under modifications of `f`
 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.
+-/
+namespace ValueDistribution
+
+open Asymptotics Filter Function.locallyFinsuppWithin MeromorphicAt MeromorphicOn Metric Real
+
+section FirstPart
 
-### TODO
+variable {f : ℂ → ℂ} {R : ℝ}
 
-- Formalize the first part of the First Main Theorem, which is the more substantial part of the
-  statement.
+/-!
+## First Part of the First Main Theorem
 -/
-namespace ValueDistribution
+
+/--
+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.
+-/
+lemma characteristic_sub_characteristic_inv (h : MeromorphicOn f ⊤) :
+    characteristic f ⊤ - characteristic f⁻¹ ⊤ =
+      circleAverage (log ‖f ·‖) 0 - (divisor f Set.univ).logCounting := by
+  calc characteristic f ⊤ - characteristic f⁻¹ ⊤
+  _ = proximity f ⊤ - proximity f⁻¹ ⊤ - (logCounting f⁻¹ ⊤ - logCounting f ⊤) := by
+    unfold characteristic
+    ring
+  _ = circleAverage (log ‖f ·‖) 0 - (logCounting f⁻¹ ⊤ - logCounting f ⊤) := by
+    rw [proximity_sub_proximity_inv_eq_circleAverage h]
+  _ = circleAverage (log ‖f ·‖) 0 - (logCounting f 0 - logCounting f ⊤) := by
+    rw [logCounting_inv]
+  _ = circleAverage (log ‖f ·‖) 0 - (divisor f Set.univ).logCounting := by
+    rw [← ValueDistribution.log_counting_zero_sub_logCounting_top]
+
+/--
+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‖`.
+-/
+lemma characteristic_sub_characteristic_inv_of_ne_zero
+    (hf : MeromorphicOn f Set.univ) (hR : R ≠ 0) :
+    characteristic f ⊤ R - characteristic f⁻¹ ⊤ R = log ‖meromorphicTrailingCoeffAt f 0‖ := by
+  calc characteristic f ⊤ R - characteristic f⁻¹ ⊤ R
+  _ = (characteristic f ⊤ - characteristic f⁻¹ ⊤) R  := by simp
+  _ = circleAverage (log ‖f ·‖) 0 R - (divisor f Set.univ).logCounting R := by
+    rw [characteristic_sub_characteristic_inv hf]
+    rfl
+  _ = log ‖meromorphicTrailingCoeffAt f 0‖ := by
+    rw [MeromorphicOn.circleAverage_log_norm hR (hf.mono_set (by tauto))]
+    unfold Function.locallyFinsuppWithin.logCounting
+    have : (divisor f (closedBall 0 |R|)) = (divisor f Set.univ).toClosedBall R :=
+      (divisor_restrict hf (by tauto)).symm
+    simp [this, toClosedBall, restrictMonoidHom, restrict_apply]
+
+/--
+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‖`.
+-/
+lemma characteristic_sub_characteristic_inv_at_zero (h : MeromorphicOn f Set.univ) :
+    characteristic f ⊤ 0 - characteristic f⁻¹ ⊤ 0 = log ‖f 0‖ := by
+  calc characteristic f ⊤ 0 - characteristic f⁻¹ ⊤ 0
+  _ = (characteristic f ⊤ - characteristic f⁻¹ ⊤) 0 := by simp
+  _ = circleAverage (log ‖f ·‖) 0 0 - (divisor f Set.univ).logCounting 0 := by
+    rw [ValueDistribution.characteristic_sub_characteristic_inv h]
+    rfl
+  _ = log ‖f 0‖ := by
+    simp
+
+/--
+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 characteristic_sub_characteristic_inv_le (hf : MeromorphicOn f Set.univ) :
+    |characteristic f ⊤ R - characteristic f⁻¹ ⊤ R|
+      ≤ max |log ‖f 0‖| |log ‖meromorphicTrailingCoeffAt f 0‖| := by
+  by_cases h : R = 0
+  · simp [h, characteristic_sub_characteristic_inv_at_zero hf]
+  · simp [characteristic_sub_characteristic_inv_of_ne_zero hf h]
+
+/--
+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.
+-/
+theorem isBigO_characteristic_sub_characteristic_inv (h : MeromorphicOn f ⊤) :
+    (characteristic f ⊤ - characteristic f⁻¹ ⊤) =O[atTop] (1 : ℝ → ℝ) :=
+  isBigO_of_le' (c := max |log ‖f 0‖| |log ‖meromorphicTrailingCoeffAt f 0‖|) _
+    (fun R ↦ by simpa using characteristic_sub_characteristic_inv_le h (R := R))
+
+end FirstPart
+
+section SecondPart
 
 variable
   {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
-  {f : ℂ → E} {a₀ : E}
-
-open Asymptotics Filter Real
+  {a₀ : E} {f : ℂ → E}
 
 /-!
 ## Second Part of the First Main Theorem
@@ -74,10 +155,15 @@ Second part of the First Main Theorem of Value Distribution Theory, qualitative
 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.
 -/
-theorem abs_characteristic_sub_characteristic_shift_eqO (h : MeromorphicOn f ⊤) :
-    |characteristic f ⊤ - characteristic (f · - a₀) ⊤| =O[atTop] (1 : ℝ → ℝ) := by
-  simp_rw [isBigO_iff', eventually_atTop]
-  use log⁺ ‖a₀‖ + log 2, add_pos_of_nonneg_of_pos posLog_nonneg (log_pos one_lt_two), 0
-  simp [abs_characteristic_sub_characteristic_shift_le h]
+theorem isBigO_characteristic_sub_characteristic_shift (h : MeromorphicOn f ⊤) :
+    (characteristic f ⊤ - characteristic (f · - a₀) ⊤) =O[atTop] (1 : ℝ → ℝ) :=
+  isBigO_of_le' (c := log⁺ ‖a₀‖ + log 2) _
+    (fun R ↦ by simpa using abs_characteristic_sub_characteristic_shift_le h)
+
+@[deprecated (since := "2025-10-06")]
+alias abs_characteristic_sub_characteristic_shift_eqO :=
+  isBigO_characteristic_sub_characteristic_shift
+
+end SecondPart
 
 end ValueDistribution

docs/overview.yaml

@@ -362,6 +362,7 @@ Analysis:
     removable singularity: 'Complex.differentiableOn_update_limUnder_insert_of_isLittleO'
     Phragmen-Lindelöf principle: 'PhragmenLindelof.horizontal_strip'
     fundamental theorem of algebra: 'Complex.isAlgClosed'
+    First Main Theorem of Value Distribution Theory: 'ValueDistribution.characteristic_sub_characteristic_inv_le'
 
   Distribution theory:
     Schwartz space: 'SchwartzMap'