From 726ac9e93dcd69fd1e9330ebc39af57adbd6892c Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Tue, 24 Dec 2024 06:50:23 +0100
Subject: [PATCH] Update firstMain.lean

---
 Nevanlinna/firstMain.lean | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)

diff --git a/Nevanlinna/firstMain.lean b/Nevanlinna/firstMain.lean
index 852f9da..46fb339 100644
--- a/Nevanlinna/firstMain.lean
+++ b/Nevanlinna/firstMain.lean
@@ -39,6 +39,34 @@ noncomputable def MeromorphicOn.N_infty
   fun r ↦ ∑ᶠ z, (max 0 (-((hf.restrict |r|).divisor z))) * log (r * ‖z‖⁻¹)
 
 
+theorem Nevanlinna_counting₁₁
+  {f : ℂ → ℂ}
+  {a : ℂ}
+  (hf : MeromorphicOn f ⊤) :
+  (hf.add (MeromorphicOn.const a)).N_infty = hf.N_infty := by
+
+  have {z : ℂ} : 0 < (hf z trivial).order → (hf z trivial).order = ((hf.add (MeromorphicOn.const a)) z trivial).order:= by
+    intro h
+
+    let A := (MeromorphicAt.const a)
+    rw [←MeromorphicAt.order_add_of_ne_orders (hf z trivial)]
+    simp
+    sorry
+
+  funext r
+  unfold MeromorphicOn.N_infty
+  let A := (hf.restrict |r|).divisor.finiteSupport (isCompact_closedBall 0 |r|)
+  repeat
+    rw [finsum_eq_sum_of_support_subset (s := A.toFinset)]
+  apply Finset.sum_congr rfl
+  intro x hx
+  congr 2
+  
+  simp at hx
+
+  sorry
+
+
 theorem Nevanlinna_counting₀
   {f : ℂ → ℂ}
   (hf : MeromorphicOn f ⊤) :