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

Sum eq integral add integral deriv

sum_eq_integral_add_integral_deriv

Plain-language statement

A first-order Euler–Maclaurin formula. For 0ab0\le a\le b and a differentiable function ff whose derivative is continuous on [a,b][a,b], the sum over integers a<kb\lfloor a\rfloor<k\le\lfloor b\rfloor equals f(a)B1(a)f(b)B1(b)+abf(t)dt+abf(t)B1(t)dt,f(a)B_1(a)-f(b)B_1(b)+\int_a^b f(t)\,dt+\int_a^b f'(t)B_1(t)\,dt, where B1(t)=tt12B_1(t)=t-\lfloor t\rfloor-\tfrac12.

analytic number theoryprime numbersasymptotics

Source project: Prime Number Theorem and More

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Iterated Deriv sub

W1.iteratedDeriv_sub

Plain-language statement

For two nn-times continuously differentiable functions ff and gg, the nnth iterated derivative distributes over subtraction: (fg)(n)=f(n)g(n).(f-g)^{(n)}=f^{(n)}-g^{(n)}.

analytic number theoryprime numbersasymptotics

Source project: Prime Number Theorem and More

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

W21 approximation

W21_approximation

Plain-language statement

Let ff be a twice differentiable complex-valued function whose first two derivatives are integrable, and let gg be a twice differentiable compactly supported cutoff that equals 11 on [1,1][-1,1] and vanishes outside (2,2)(-2,2). Then g(x/R)f(x)g(x/R)f(x) converges to ff as RR\to\infty in the project norm h=Rh(x)dx+14π2Rh(x)dx.\|h\|=\int_{\mathbb R}|h(x)|\,dx+\frac{1}{4\pi^2}\int_{\mathbb R}|h''(x)|\,dx.

analytic number theoryprime numbersasymptotics

Source project: Prime Number Theorem and More

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Weak PNT

WeakPNT''

Plain-language statement

The Chebyshev function is asymptotic to the identity: ψ(x)x\psi(x)\sim x as xx\to\infty. Equivalently, ψ(x)/x1\psi(x)/x\to1.

analytic number theoryprime numbersasymptotics

Source project: Prime Number Theorem and More

Person-level attribution pending.

View proof record