Update firstMain.lean

Nevanlinna/firstMain.lean

@@ -11,28 +11,49 @@ noncomputable def MeromorphicOn.N_zero
   {f : ℂ → ℂ}
   (h₁f : MeromorphicOn f ⊤) :
   ℝ → ℝ :=
-  fun r ↦ ∑ᶠ z ∈ Metric.ball (0 : ℂ) r, (max 0 (h₁f.divisor z)) * log (r * ‖z‖⁻¹)
+  fun r ↦ ∑ᶠ z ∈ Metric.closedBall (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‖⁻¹)
+  fun r ↦ ∑ᶠ z ∈ Metric.closedBall (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
+  h₁f.N_zero - h₁f.N_infty = fun r ↦ ∑ᶠ z ∈ Metric.closedBall (0 : ℂ) r, (h₁f.divisor z) * log (r * ‖z‖⁻¹) := by
+
+  funext r
+  simp only [Pi.sub_apply]
+
+  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
 
 --
 
-noncomputable def logpos : ℝ → ℝ :=
+noncomputable def logpos : ℝ → ℝ := fun r ↦ max 0 (log r)
-  fun r ↦ max 0 (log r)
 
-theorem loglogpos
+theorem loglogpos {r : ℝ} : log r = logpos r - logpos r⁻¹ := by
-  {r : ℝ} :
-  log r = logpos r - logpos r⁻¹ := by
   unfold logpos
   rw [log_inv]
   by_cases h : 0 ≤ log r