2024-12-05 13:51:00 +01:00
|
|
|
|
import Nevanlinna.divisor
|
2024-09-13 09:21:57 +02:00
|
|
|
|
|
|
|
|
|
|
open Real
|
|
|
|
|
|
|
|
|
|
|
|
|
2024-12-05 13:51:00 +01:00
|
|
|
|
noncomputable def Divisor.Nevanlinna.n
|
|
|
|
|
|
(D : Divisor ⊤) :
|
|
|
|
|
|
ℝ → ℤ :=
|
|
|
|
|
|
fun r ↦ ∑ᶠ z ∈ Metric.ball (0 : ℂ) r, D z
|
2024-09-14 08:38:04 +02:00
|
|
|
|
|
2024-12-05 13:51:00 +01:00
|
|
|
|
noncomputable def Divisor.Nevanlinna.integratedCounting
|
|
|
|
|
|
(D : Divisor ⊤) :
|
|
|
|
|
|
ℝ → ℝ :=
|
|
|
|
|
|
fun r ↦ ∑ᶠ z ∈ Metric.ball (0 : ℂ) r, (D z) * log (r * ‖z‖⁻¹)
|
