working…

Nevanlinna/firstMain.lean

@@ -0,0 +1,17 @@
+import Nevanlinna.holomorphic_JensenFormula
+
+open Real
+
+variable {f : ℂ → ℂ}
+variable {h₁f : AnalyticOn ℂ f ⊤}
+variable {h₂f : f 0 ≠ 0}
+
+noncomputable def unintegratedCounting : ℝ → ℕ := by
+  intro r
+  let A := h₁f.mono (by tauto : Metric.closedBall (0 : ℂ) r ⊆ ⊤)
+  exact ∑ᶠ z, (A.order z).toNat
+
+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‖⁻¹)