22 lines
609 B
Plaintext
22 lines
609 B
Plaintext
import Mathlib.Analysis.Analytic.Meromorphic
|
||
import Nevanlinna.holomorphic_JensenFormula
|
||
|
||
open Real
|
||
|
||
variable (f : ℂ → ℂ)
|
||
variable {h₁f : MeromorphicOn f ⊤}
|
||
variable {h₂f : f 0 ≠ 0}
|
||
|
||
|
||
|
||
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‖⁻¹)
|