18 lines
534 B
Plaintext
18 lines
534 B
Plaintext
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‖⁻¹)
|