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

1 topic

2 results

Clear filters
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