InverseSquareZeroSum.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Convergence of inverse-square weights from the ordinary zero count

theorem OAI.Ostmann.zero_height_log_three_halves line 13

theorem OAI.Ostmann.inverse_square_weights_summable line 59

Source documentation

Only the ordinary O(T log T) count is needed, not a zero-free region.

theorem inverse_square_weights_summable {ι : Type*} (h : ι → ℝ)
    (Q K : ℝ) (hQ : 1 ≤ Q) (hK : 0 ≤ K) (hh : ∀ i, 0 ≤ h i)
    (hcount : ∀ (S : Finset ι) (t : ℝ), 0 ≤ t →
      ((S.filter (fun i => h i ≤ t)).card : ℝ) ≤ K * (t + 1) * Real.log (Q * (t + 2))) :
    Summable (fun i => ((1 + h i) ^ 2)⁻¹) := by
…