Source indexedtheorem · leanprover/lean4:v4.32.0

Kadiri.zeroImagSquareTailSummable_of_cumulative_count_le

PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:1748 to 1771

Source documentation

Square-tail summability from any cumulative dyadic count bound whose 4^(-k)-weighted series is summable.

Exact Lean statement

theorem zeroImagSquareTailSummable_of_cumulative_count_le {g : ℕ → ℝ}
    (hg : Summable fun k : ℕ => g k * (((2 : ℝ) ^ k)⁻¹) ^ (2 : ℕ))
    (hcount : ∀ k : ℕ, (Nat.card {rho : NontrivialZeros //
        |(rho : ℂ).im| < (2 : ℝ) ^ (k + 1)} : ℝ) ≤ g k) :
    zeroImagSquareTailSummable

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem zeroImagSquareTailSummable_of_cumulative_count_le {g : ℕ → ℝ}    (hg : Summable fun k : ℕ => g k * (((2 : ℝ) ^ k)⁻¹) ^ (2 : ℕ))    (hcount : ∀ k : ℕ, (Nat.card {rho : NontrivialZeros //        |(rho : ℂ).im| < (2 : ℝ) ^ (k + 1)} : ℝ) ≤ g k) :    zeroImagSquareTailSummable := by  apply zeroImagSquareTailSummable_of_dyadic_shell_source  unfold zeroImagDyadicShellSummableSource  rw [summable_sigma_of_nonneg]  · constructor    · intro k      haveI : Finite {rho : NontrivialZeros // zeroHeightDyadicShell k rho} :=        Set.finite_coe_iff.mpr (nontrivialZeros_dyadic_shell_finite k)      exact Summable.of_finite    · refine Summable.of_nonneg_of_le        (fun k => zeroHeightDyadicShellMass_nonneg k) (fun k => ?_) hg      have hmass := zeroHeightDyadicShellMass_le_count_inv_sq k      have hcard :          (Nat.card {rho : NontrivialZeros // zeroHeightDyadicShell k rho} : ℝ) ≤            g k := by        refine le_trans ?_ (hcount k)        exact_mod_cast zeroHeightDyadicShellCount_le_cumulative_count k      exact hmass.trans (mul_le_mul_of_nonneg_right hcard (sq_nonneg _))  · intro p    exact sq_nonneg _