Source indexedtheorem · leanprover/lean4:v4.32.0

Kadiri.zeroImagDyadicShellCountBoundSource_of_cumulative_count_bound

PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:1076 to 1088

Source documentation

A cumulative dyadic count source gives the dyadic shell-count source.

Exact Lean statement

theorem zeroImagDyadicShellCountBoundSource_of_cumulative_count_bound
    (hsrc : zeroImagDyadicCumulativeCountBoundSource) :
    zeroImagDyadicShellCountBoundSource

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem zeroImagDyadicShellCountBoundSource_of_cumulative_count_bound    (hsrc : zeroImagDyadicCumulativeCountBoundSource) :    zeroImagDyadicShellCountBoundSource := by  rcases hsrc with ⟨C, hC_nonneg, hcount⟩  refine ⟨C, hC_nonneg, ?_⟩  intro k  have hcard_nat := zeroHeightDyadicShellCount_le_cumulative_count k  have hcard :      (Nat.card {rho : NontrivialZeros // zeroHeightDyadicShell k rho} : ℝ) ≤        (Nat.card {rho : NontrivialZeros //          |(rho : ℂ).im| < (2 : ℝ) ^ (k + 1)} : ℝ) := by    exact_mod_cast hcard_nat  exact hcard.trans (hcount k)