Source indexedlemma · leanprover/lean4:v4.32.0

Kadiri.zeroHeightDyadicShellCount_le_cumulative_count

PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:792 to 802

Source documentation

A dyadic shell has no more zeros than the cumulative set below its top edge.

Exact Lean statement

lemma zeroHeightDyadicShellCount_le_cumulative_count (k : ℕ) :
    Nat.card {rho : NontrivialZeros // zeroHeightDyadicShell k rho} ≤
      Nat.card {rho : NontrivialZeros //
        |(rho : ℂ).im| < (2 : ℝ) ^ (k + 1)}

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma zeroHeightDyadicShellCount_le_cumulative_count (k : ℕ) :    Nat.card {rho : NontrivialZeros // zeroHeightDyadicShell k rho} ≤      Nat.card {rho : NontrivialZeros //        |(rho : ℂ).im| < (2 : ℝ) ^ (k + 1)} := by  classical  haveI : Finite {rho : NontrivialZeros //      |(rho : ℂ).im| < (2 : ℝ) ^ (k + 1)} :=    Set.finite_coe_iff.mpr      (nontrivialZeros_abs_im_lt_finite ((2 : ℝ) ^ (k + 1)))  exact Nat.card_le_card_of_injective (dyadicShellToCumulative k)    (dyadicShellToCumulative_injective k)