Source indexedtheorem · leanprover/lean4:v4.32.0

Kadiri.zeroImagDyadicShellSummableSource_of_mass_bound

PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:1058 to 1073

Source documentation

A dyadic mass bound gives dyadic-shell height summability.

Exact Lean statement

theorem zeroImagDyadicShellSummableSource_of_mass_bound
    (hsrc : zeroImagDyadicShellMassBoundSource) :
    zeroImagDyadicShellSummableSource

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem zeroImagDyadicShellSummableSource_of_mass_bound    (hsrc : zeroImagDyadicShellMassBoundSource) :    zeroImagDyadicShellSummableSource := by  rcases hsrc with ⟨C, _hC, hbound⟩  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    · exact Summable.of_nonneg_of_le        (fun k => zeroHeightDyadicShellMass_nonneg k) hbound        (summable_linear_geometric_inv_two C)  · intro p    exact sq_nonneg _