Source-pinned research

Research proof index

Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.

This index contains 3 research declarations. Search 10,000 more complete Mathlib declarations.

1 topic

3 results

Clear filters
Project-declaredLean 4.32.0

Zeta zero re mem of im pos

Backlund.zeta_zero_re_mem_of_im_pos

Plain-language statement

Every zero ss of the Riemann zeta function in the upper half-plane lies in the critical strip: if ζ(s)=0\zeta(s)=0 and Ims>0\operatorname{Im}s>0, then 0Res1.0\le\operatorname{Re}s\le1.

analytic number theoryprime numbersasymptotics

Source project: Prime Number Theorem and More

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Zeta Counting crude majorant

Backlund.zetaCounting_crude_majorant

Plain-language statement

The Riemann zeta zero-counting function has a crude polynomial bound: there is a constant A>0A>0 such that, for every T2T\ge2, Nζ(T)AT3/2.|N_\zeta(T)|\le A T^{3/2}.

analytic number theoryprime numbersasymptotics

Source project: Prime Number Theorem and More

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Zeta Surrogate zeros in closed Ball₀ count

Backlund.zetaSurrogate_zeros_in_closedBall₀_count

Plain-language statement

Let Z(s)Z(s) be the project's entire zeta surrogate, obtained by removing the pole of ζ(s)\zeta(s) at s=1s=1. There is a constant C>0C>0 such that, for every R1R\ge1, the total multiplicity of the zeros of ZZ in sR|s|\le R is bounded by C(1+R)3/2.C(1+R)^{3/2}.

analytic number theoryprime numbersasymptotics

Source project: Prime Number Theorem and More

Person-level attribution pending.

View proof record