Source indexedlemma · leanprover/lean4:v4.32.0

Kadiri.positive_height_nontrivial_zero_count_le_NPrime

PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:173 to 181

Mathematical statement

Exact Lean statement

lemma positive_height_nontrivial_zero_count_le_NPrime (T : ℝ) :
    (Nat.card {rho : NontrivialZeros // 0 < (rho : ℂ).im ∧ (rho : ℂ).im < T} : ℝ) ≤
      riemannZeta.N' 0 T

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma positive_height_nontrivial_zero_count_le_NPrime (T : ℝ) :    (Nat.card {rho : NontrivialZeros // 0 < (rho : ℂ).im ∧ (rho : ℂ).im < T} : ℝ) ≤      riemannZeta.N' 0 T := by  have hcard :      Nat.card {rho : NontrivialZeros // 0 < (rho : ℂ).im ∧ (rho : ℂ).im < T} =        Nat.card (riemannZeta.zeroes_rect (.Ioo 0 1) (.Ioo 0 T)) :=    Nat.card_congr (positiveHeightNontrivialZeroEquivZeroesRect T)  rw [hcard, riemannZeta.N']  exact zeroes_rect_positive_height_card_le_zeroes_sum_order T