From c7a3804b0cc9661a74206dbc911eb5f6c527a578 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Mon, 9 Dec 2024 19:58:56 +0100
Subject: [PATCH] =?UTF-8?q?Implementing=E2=80=A6?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Nevanlinna/firstMain.lean | 72 +++++++++++++++++++++++----------------
 1 file changed, 42 insertions(+), 30 deletions(-)

diff --git a/Nevanlinna/firstMain.lean b/Nevanlinna/firstMain.lean
index ae14553..7f12a34 100644
--- a/Nevanlinna/firstMain.lean
+++ b/Nevanlinna/firstMain.lean
@@ -7,49 +7,61 @@ open Real
 
 
 -- Lang p. 164
+
+theorem MeromorphicOn.restrict
+  {f : ℂ → ℂ}
+  (h₁f : MeromorphicOn f ⊤)
+  (r : ℝ) :
+  MeromorphicOn f (Metric.closedBall 0 r) := by
+  exact fun x a => h₁f x trivial
+
 noncomputable def MeromorphicOn.N_zero
   {f : ℂ → ℂ}
-  (h₁f : MeromorphicOn f ⊤) :
+  (hf : MeromorphicOn f ⊤) :
   ℝ → ℝ :=
-  fun r ↦ ∑ᶠ z ∈ Metric.closedBall (0 : ℂ) r, (max 0 (h₁f.divisor z)) * log (r * ‖z‖⁻¹)
+  fun r ↦ ∑ᶠ z, (max 0 ((hf.restrict r).divisor z)) * log (r * ‖z‖⁻¹)
 
 noncomputable def MeromorphicOn.N_infty
   {f : ℂ → ℂ}
-  (h₁f : MeromorphicOn f ⊤) :
+  (hf : MeromorphicOn f ⊤) :
   ℝ → ℝ :=
-  fun r ↦ ∑ᶠ z ∈ Metric.closedBall (0 : ℂ) r, (max 0 (-(h₁f.divisor z))) * log (r * ‖z‖⁻¹)
+  fun r ↦ ∑ᶠ z, (max 0 (-((hf.restrict r).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.closedBall (0 : ℂ) r, (h₁f.divisor z) * log (r * ‖z‖⁻¹) := by
+  (hf : MeromorphicOn f ⊤) :
+  hf.N_zero - hf.N_infty = fun r ↦ ∑ᶠ z, ((hf.restrict r).divisor z) * log (r * ‖z‖⁻¹) := by
 
   funext r
   simp only [Pi.sub_apply]
+  unfold  MeromorphicOn.N_zero MeromorphicOn.N_infty
 
-  rw [finsum_eq_sum]
-  sorry
-
-  have h₁fr : MeromorphicOn f (Metric.ball (0 : ℂ) r) := by
-    sorry
-
-  let Sr :=
-
-  rw [finsum_eq_sum_of_support_subset _ h₄f]
-
-
-  have h₂U : IsCompact (Metric.closedBall (0 : ℂ) R) :=
-    isCompact_closedBall 0 R
-
-  have h'₂f : ∃ u : (Metric.closedBall (0 : ℂ) R), f u ≠ 0 := by
-    use ⟨0, Metric.mem_closedBall_self (le_of_lt hR)⟩
-
-  have h₃f : Set.Finite (Function.support h₁f.divisor) := by
-    exact Divisor.finiteSupport h₂U (StronglyMeromorphicOn.meromorphicOn h₁f).divisor
-
-  sorry
-
---
+  let A := (hf.restrict r).divisor.finiteSupport (isCompact_closedBall 0 r)
+  repeat
+    rw [finsum_eq_sum_of_support_subset (s := A.toFinset)]
+  rw [← Finset.sum_sub_distrib]
+  simp_rw [← sub_mul]
+  congr
+  funext x
+  congr
+  by_cases h : 0 ≤ (hf.restrict r).divisor x
+  · simp [h]
+  · have h' : 0 ≤ -((hf.restrict r).divisor x) := by
+      simp at h
+      apply Int.le_neg_of_le_neg
+      simp
+      exact Int.le_of_lt h
+    simp at h
+    simp [h']
+    linarith
+  --
+  repeat
+    intro x
+    contrapose
+    simp
+    intro hx
+    rw [hx]
+    tauto
 
 noncomputable def logpos : ℝ → ℝ := fun r ↦ max 0 (log r)
 
@@ -67,7 +79,7 @@ theorem loglogpos {r : ℝ} : log r = logpos r - logpos r⁻¹ := by
 
 noncomputable def MeromorphicOn.m_infty
   {f : ℂ → ℂ}
-  (h₁f : MeromorphicOn f ⊤) :
+  (_ : MeromorphicOn f ⊤) :
   ℝ → ℝ :=
   fun r ↦ (2 * π)⁻¹ * ∫ x in (0)..(2 * π), logpos ‖f (circleMap 0 r x)‖