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

Mu pnt

mu_pnt

Project documentation

The summatory Möbius function has sublinear growth: as xx\to\infty, n<xμ(n)=o(x).\sum_{n<\lfloor x\rfloor}\mu(n)=o(x). This is the Möbius-function form of the prime number theorem.

analytic number theoryprime numbersasymptotics

Source project: Prime Number Theorem and More

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Norm fourier le integral deriv div

norm_fourier_le_integral_deriv_div

Plain-language statement

Fourier-transform decay from an integrable derivative: for integrable, differentiable g with integrable derivative, ‖𝓕 g w‖ ≤ (∫ ‖deriv g x‖) / (2π·|w|).

analytic number theoryprime numbersasymptotics

Source project: Prime Number Theorem and More

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Norm interval Integral exp neg mul sinc tail le

norm_intervalIntegral_exp_neg_mul_sinc_tail_le

Plain-language statement

For a>0a>0 and 1RB1\le R\le B, the damped sinc integral over the finite tail [R,B][R,B] satisfies the uniform estimate RBeaxsinc(x)dx4R.\left|\int_R^B e^{-ax}\operatorname{sinc}(x)\,dx\right|\le\frac{4}{R}.

analytic number theoryprime numbersasymptotics

Source project: Prime Number Theorem and More

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Norm sin div kernel tail le integral norm

norm_sin_div_kernel_tail_le_integral_norm

Plain-language statement

Let ff be integrable, R>0R>0, and KT(u)=sin(Tu)/(πu)K_T(u)=\sin(Tu)/(\pi u) for u0u\ne0, with the project's value KT(0)=0K_T(0)=0. Removing the part of the convolution outside [R,R][-R,R] incurs at most RKT(u)f(xu)duRRKT(u)f(xu)du1πRRf(u)du.\left\|\int_{\mathbb R}K_T(u)f(x-u)\,du-\int_{-R}^{R}K_T(u)f(x-u)\,du\right\|\le\frac{1}{\pi R}\int_{\mathbb R}\|f(u)\|\,du. The estimate is uniform in xx and TT.

analytic number theoryprime numbersasymptotics

Source project: Prime Number Theorem and More

Person-level attribution pending.

View proof record