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 2 research declarations. Search 10,000 more complete Mathlib declarations.
2 results
Clear filterssin_div_error_interval_bound
Plain-language statement
Interval form of sin_div_error_pointwise_bound: integrating the pointwise bound over [-1, 1] controls the windowed error integral by (D / π) · vol (Ioc (-1) 1).
Source project: Prime Number Theorem and More
Person-level attribution pending.
sin_div_error_pointwise_bound
Plain-language statement
Pointwise bound on the sin-div windowed error term: scaling by the normalized sinc kernel and a mean-value estimate on g (x - u) - g x gives a bound D / π that is independent of the height T.
Source project: Prime Number Theorem and More
Person-level attribution pending.