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

Admissible bound mono

admissible_bound.mono

Plain-language statement

For positive parameters A,B,C,RA,B,C,R, the classical error-bound function A(logxR)Bexp ⁣(ClogxR)A\left(\frac{\log x}{R}\right)^B\exp\!\left(-C\sqrt{\frac{\log x}{R}}\right) is nonincreasing once xexp ⁣(R(2B/C)2)x\ge \exp\!\left(R(2B/C)^2\right).

analytic number theoryprime numbersasymptotics

Source project: Prime Number Theorem and More

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Analytic On div Removable zero

AnalyticOn_divRemovable_zero

Plain-language statement

Let ff be analytic on an open set ss containing 00, and suppose f(0)=0f(0)=0. Define g(z)=f(z)/zg(z)=f(z)/z for z0z\ne0 and g(0)=f(0)g(0)=f'(0). Then the apparent singularity at 00 is removable and gg is analytic throughout ss.

analytic number theoryprime numbersasymptotics

Source project: Prime Number Theorem and More

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Analytic On div Removable zero closed Ball

AnalyticOn_divRemovable_zero_closedBall

Plain-language statement

Suppose R>0R>0 and ff is analytic on the closed disc zR|z|\le R with f(0)=0f(0)=0. Define g(z)=f(z)/zg(z)=f(z)/z for z0z\ne0 and g(0)=f(0)g(0)=f'(0). Then gg is analytic on the entire closed disc, including at the removed singularity.

analytic number theoryprime numbersasymptotics

Source project: Prime Number Theorem and More

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Sum moebius pmul eq prod one sub

ArithmeticFunction.sum_moebius_pmul_eq_prod_one_sub

Plain-language statement

If g is a multiplicative arithmetic function, then for any n0n \neq 0, dnμ(d)g(d)=pn(1g(p))\sum_{d | n} \mu(d) \cdot g(d) = \prod_{p | n} (1 - g(p)).

analytic number theoryprime numbersasymptotics

Source project: Prime Number Theorem and More

Person-level attribution pending.

View proof record