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

---
 Nevanlinna/firstMain.lean | 25 +++++++++----------------
 1 file changed, 9 insertions(+), 16 deletions(-)

diff --git a/Nevanlinna/firstMain.lean b/Nevanlinna/firstMain.lean
index f4b4e9a..abdfa50 100644
--- a/Nevanlinna/firstMain.lean
+++ b/Nevanlinna/firstMain.lean
@@ -1,21 +1,14 @@
-import Mathlib.Analysis.Analytic.Meromorphic
-import Nevanlinna.holomorphic_JensenFormula
+import Nevanlinna.divisor
 
 open Real
 
-variable (f : ℂ → ℂ)
-variable {h₁f : MeromorphicOn f ⊤}
-variable {h₂f : f 0 ≠ 0}
 
+noncomputable def Divisor.Nevanlinna.n
+  (D : Divisor ⊤) :
+  ℝ → ℤ :=
+  fun r ↦ ∑ᶠ z ∈ Metric.ball (0 : ℂ) r, D z
 
-
-noncomputable def Nevanlinna.n : ℝ → ℤ := by
-  intro r
-  have : MeromorphicAt f z := by
-    exact h₁f (sorryAx ℂ true) trivial
-  exact ∑ᶠ z ∈ Metric.ball (0 : ℂ) r, (h₁f z trivial).order
-
-noncomputable def integratedCounting : ℝ → ℝ := by
-  intro r
-  -- Issue here: for s on the boundary of the ball, zero comes out.
-  exact ∑ᶠ s, (h₁f.order s).toNat * log (r * ‖s.1‖⁻¹)
+noncomputable def Divisor.Nevanlinna.integratedCounting
+  (D : Divisor ⊤) :
+  ℝ → ℝ :=
+  fun r ↦ ∑ᶠ z ∈ Metric.ball (0 : ℂ) r, (D z) * log (r * ‖z‖⁻¹)