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

Mellin Convolution Symmetric

MellinConvolutionSymmetric

Plain-language statement

Mellin convolution is commutative at positive arguments. For functions f,g:RRf,g:\mathbb R\to\mathbb R or C\mathbb C and every x>0x>0, (fMg)(x)=(gMf)(x),(f*_M g)(x)=(g*_M f)(x), where (fMg)(x)=0f(y)g(x/y)dy/y(f*_M g)(x)=\int_0^\infty f(y)g(x/y)\,dy/y.

analytic number theoryprime numbersasymptotics

Source project: Prime Number Theorem and More

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Mellin Of Smooth1a

MellinOfSmooth1a

Plain-language statement

Let ν\nu be continuously differentiable and supported in [1/2,2][1/2,2]. For ε>0\varepsilon>0 and Res>0\operatorname{Re}s>0, the Mellin transform of the project's smoothed cutoff satisfies M(1ε~)(s)=1sM(ν)(εs).\mathcal M(\widetilde{1_\varepsilon})(s)=\frac{1}{s}\,\mathcal M(\nu)(\varepsilon s).

analytic number theoryprime numbersasymptotics

Source project: Prime Number Theorem and More

Person-level attribution pending.

View proof record