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 57 research declarations. Search 10,000 more complete Mathlib declarations.

1 topic

57 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
Project-declaredLean 4.32.0

Borel Caratheodory closed Ball

borelCaratheodory_closedBall

Project documentation

A closed-disc form of the Borel–Carathéodory theorem. Let R,M>0R,M>0, let ff be analytic on zR|z|\le R, assume f(0)=0f(0)=0, and suppose Ref(z)M\operatorname{Re}f(z)\le M throughout that disc. If r<Rr<R and zr|z|\le r, then f(z)2MrRr.|f(z)|\le \frac{2Mr}{R-r}.

analytic number theoryprime numbersasymptotics

Source project: Prime Number Theorem and More

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Abs rem le

BrunTitchmarsh.abs_rem_le

Plain-language statement

For the Selberg sieve that removes primes up to zz from an interval [x,x+y][x,x+y], with x,y>0x,y>0 and z1z\ge1, the remainder in the expected count of multiples of every nonzero integer dd is uniformly bounded: rd5|r_d|\le5.

analytic number theoryprime numbersasymptotics

Source project: Prime Number Theorem and More

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Is Big O nat Top of at Top

BrunTitchmarsh.IsBigO.nat_Top_of_atTop

Plain-language statement

Suppose sequences f,g:NRf,g:\mathbb N\to\mathbb R satisfy f(n)=O(g(n))f(n)=O(g(n)) as nn\to\infty, and f(n)=0f(n)=0 whenever g(n)=0g(n)=0. Then a single constant bounds f(n)|f(n)| by that constant times g(n)|g(n)| for every natural number nn, not only for all sufficiently large nn.

analytic number theoryprime numbersasymptotics

Source project: Prime Number Theorem and More

Person-level attribution pending.

View proof record