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

Residue Of Tends To

ResidueOfTendsTo

Plain-language statement

Let ff be holomorphic on a punctured neighborhood of pp. If (sp)f(s)A(sp),(s-p)f(s)\longrightarrow A\qquad(s\to p), then ff differs from its principal part A/(sp)A/(s-p) by a bounded function on some punctured neighborhood of pp. In asymptotic notation, f(s)=Asp+O(1).f(s)=\frac{A}{s-p}+O(1).

analytic number theoryprime numbersasymptotics

Source project: Prime Number Theorem and More

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Sin div error interval bound

sin_div_error_interval_bound

Plain-language statement

Interval form of sin_div_error_pointwise_bound: integrating the pointwise bound over [-1, 1] controls the windowed error integral by (D / π) · vol (Ioc (-1) 1).

analytic number theoryprime numbersasymptotics

Source project: Prime Number Theorem and More

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Sin div error pointwise bound

sin_div_error_pointwise_bound

Plain-language statement

Pointwise bound on the sin-div windowed error term: scaling by the normalized sinc kernel and a mean-value estimate on g (x - u) - g x gives a bound D / π that is independent of the height T.

analytic number theoryprime numbersasymptotics

Source project: Prime Number Theorem and More

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Smooth urysohn support Ioo

smooth_urysohn_support_Ioo

Plain-language statement

Given a<ba<b and c<dc<d, there is a smooth compactly supported function Ψ:RR\Psi:\mathbb R\to\mathbb R with 1[b,c]Ψ1(a,d)\mathbf 1_{[b,c]}\le\Psi\le\mathbf 1_{(a,d)} and support exactly (a,d)(a,d). In the usual ordered case a<bc<da<b\le c<d, this is a smooth cutoff equal to 11 on [b,c][b,c], strictly supported in (a,d)(a,d), and taking values between 00 and 11.

analytic number theoryprime numbersasymptotics

Source project: Prime Number Theorem and More

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Smoothed Chebyshev Pull2

SmoothedChebyshevPull2

Plain-language statement

For the smoothed Chebyshev integrand F(s)=ζ(s)ζ(s)M(1ε~)(s)Xs,F(s)=-\frac{\zeta'(s)}{\zeta(s)}\,\mathcal M(\widetilde{1_\varepsilon})(s)X^s, the central part of the normalized vertical integral on Res=σ1\operatorname{Re}s=\sigma_1 can be shifted to Res=σ2<σ1\operatorname{Re}s=\sigma_2<\sigma_1. With the project's contour-piece notation, the complete decomposition is I37=I3I4+I5+I6+I7,I_{37}=I_3-I_4+I_5+I_6+I_7, where I3I_3 and I7I_7 are the unchanged tails, I5I_5 is the new central vertical side, and I4,I6I_4,I_6 are the horizontal connectors.

analytic number theoryprime numbersasymptotics

Source project: Prime Number Theorem and More

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Smooth Existence

SmoothExistence

Plain-language statement

There exists a smooth nonnegative function ν:RR\nu:\mathbb R\to\mathbb R supported in [1/2,2][1/2,2] and normalized to have multiplicative mass one: 0ν(x)dxx=1.\int_0^\infty \nu(x)\,\frac{dx}{x}=1.

analytic number theoryprime numbersasymptotics

Source project: Prime Number Theorem and More

Person-level attribution pending.

View proof record