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

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