Admissible bound mono
admissible_bound.mono
Plain-language statement
For positive parameters , the classical error-bound function is nonincreasing once .
Source project: Prime Number Theorem and More
Person-level attribution pending.
Source-pinned research
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.
57 results
Clear filtersadmissible_bound.mono
Plain-language statement
For positive parameters , the classical error-bound function is nonincreasing once .
Source project: Prime Number Theorem and More
Person-level attribution pending.
AnalyticOn_divRemovable_zero
Plain-language statement
Let be analytic on an open set containing , and suppose . Define for and . Then the apparent singularity at is removable and is analytic throughout .
Source project: Prime Number Theorem and More
Person-level attribution pending.
AnalyticOn_divRemovable_zero_closedBall
Plain-language statement
Suppose and is analytic on the closed disc with . Define for and . Then is analytic on the entire closed disc, including at the removed singularity.
Source project: Prime Number Theorem and More
Person-level attribution pending.
ArithmeticFunction.LSeries_d_eq_riemannZeta_pow
Plain-language statement
The L-series of d k equals ζ(s)^k for Re(s) > 1.
Source project: Prime Number Theorem and More
Person-level attribution pending.
ArithmeticFunction.sum_moebius_pmul_eq_prod_one_sub
Plain-language statement
If g is a multiplicative arithmetic function, then for any , .
Source project: Prime Number Theorem and More
Person-level attribution pending.
auto_cheby_fourier_summable
Plain-language statement
The series ∑ f(n)/n · 𝓕ψ(log(n/x)/(2π)) is summable for x ≥ 1.
Source project: Prime Number Theorem and More
Person-level attribution pending.