From 9068ad406e85eca17b99c97bf8a7774944ed2dde Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Thu, 5 Dec 2024 16:53:48 +0100
Subject: [PATCH] Update firstMain.lean

---
 Nevanlinna/firstMain.lean | 96 +++++++++++++++++++++++++++++++++++----
 1 file changed, 88 insertions(+), 8 deletions(-)

diff --git a/Nevanlinna/firstMain.lean b/Nevanlinna/firstMain.lean
index abdfa50..1fd5127 100644
--- a/Nevanlinna/firstMain.lean
+++ b/Nevanlinna/firstMain.lean
@@ -1,14 +1,94 @@
+import Mathlib.MeasureTheory.Integral.CircleIntegral
 import Nevanlinna.divisor
+import Nevanlinna.stronglyMeromorphicOn
+import Nevanlinna.meromorphicOn_divisor
 
 open Real
 
 
-noncomputable def Divisor.Nevanlinna.n
-  (D : Divisor ⊤) :
-  ℝ → ℤ :=
-  fun r ↦ ∑ᶠ z ∈ Metric.ball (0 : ℂ) r, D z
-
-noncomputable def Divisor.Nevanlinna.integratedCounting
-  (D : Divisor ⊤) :
+-- Lang p. 164
+noncomputable def MeromorphicOn.N_zero
+  {f : ℂ → ℂ}
+  (h₁f : MeromorphicOn f ⊤) :
   ℝ → ℝ :=
-  fun r ↦ ∑ᶠ z ∈ Metric.ball (0 : ℂ) r, (D z) * log (r * ‖z‖⁻¹)
+  fun r ↦ ∑ᶠ z ∈ Metric.ball (0 : ℂ) r, (max 0 (h₁f.divisor z)) * log (r * ‖z‖⁻¹)
+
+noncomputable def MeromorphicOn.N_infty
+  {f : ℂ → ℂ}
+  (h₁f : MeromorphicOn f ⊤) :
+  ℝ → ℝ :=
+  fun r ↦ ∑ᶠ z ∈ Metric.ball (0 : ℂ) r, (max 0 (-(h₁f.divisor z))) * log (r * ‖z‖⁻¹)
+
+theorem Nevanlinna_counting
+  {f : ℂ → ℂ}
+  (h₁f : MeromorphicOn f ⊤) :
+  h₁f.N_zero - h₁f.N_infty = fun r ↦ ∑ᶠ z ∈ Metric.ball (0 : ℂ) r, (h₁f.divisor z) * log (r * ‖z‖⁻¹) := by
+  sorry
+
+--
+
+noncomputable def logpos : ℝ → ℝ :=
+  fun r ↦ max 0 (log r)
+
+theorem loglogpos
+  {r : ℝ} :
+  log r = logpos r - logpos r⁻¹ := by
+  unfold logpos
+  rw [log_inv]
+  by_cases h : 0 ≤ log r
+  · simp [h]
+  · simp at h
+    have : 0 ≤ -log r := Left.nonneg_neg_iff.2 (le_of_lt h)
+    simp [h, this]
+    exact neg_nonneg.mp this
+
+--
+
+noncomputable def MeromorphicOn.m_infty
+  {f : ℂ → ℂ}
+  (h₁f : MeromorphicOn f ⊤) :
+  ℝ → ℝ :=
+  fun r ↦ (2 * π)⁻¹ * ∫ x in (0)..(2 * π), logpos ‖f (circleMap 0 r x)‖
+
+theorem Nevanlinna_proximity
+  {f : ℂ → ℂ}
+  {r : ℝ}
+  (h₁f : MeromorphicOn f ⊤) :
+  (2 * π)⁻¹ * ∫ x in (0)..(2 * π), log ‖f (circleMap 0 r x)‖ = (h₁f.m_infty r) - (h₁f.inv.m_infty r) := by
+  unfold MeromorphicOn.m_infty
+  rw [← mul_sub]; congr
+  rw [← intervalIntegral.integral_sub]; congr
+  funext x
+  simp_rw [loglogpos]; congr
+  exact Eq.symm (IsAbsoluteValue.abv_inv Norm.norm (f (circleMap 0 r x)))
+  --
+  sorry
+
+noncomputable def MeromorphicOn.T_infty
+  {f : ℂ → ℂ}
+  (hf : MeromorphicOn f ⊤) :
+  ℝ → ℝ :=
+  hf.m_infty + hf.N_infty
+
+theorem Nevanlinna_firstMain₁
+  {f : ℂ → ℂ}
+  (h₁f : MeromorphicOn f ⊤)
+  (h₂f : StronglyMeromorphicAt f 0)
+  (h₃f : f 0 ≠ 0) :
+  (fun r ↦ log ‖f 0‖) + h₁f.inv.T_infty = h₁f.T_infty := by
+  funext r
+  simp
+  unfold MeromorphicOn.T_infty
+  unfold MeromorphicOn.N_infty
+  unfold MeromorphicOn.m_infty
+  simp
+
+  sorry
+
+theorem Nevanlinna_firstMain₂
+  {f : ℂ → ℂ}
+  {a : ℂ}
+  {r : ℝ}
+  (h₁f : MeromorphicOn f ⊤) :
+  |(h₁f.T_infty r) - ((h₁f.sub (MeromorphicOn.const a)).T_infty r)| ≤ logpos ‖a‖ + log 2 := by
+  sorry