Commit 2025-12-27 08:07 b86fd5c9

View on Github →

feat(NumberTheory.Chebyshev): prove connection between prime counting and theta (#32281) Uses Abel summation to express the prime counting function in terms of the Chebyshev theta function. This upstreams some results from PrimeNumberTheoremAnd.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/SpecialFunctions/Log/InvLog.lean

added theorem Real.deriv_inv_log

added theorem Real.not_continuousAt_inv_log_neg_one

added theorem Real.not_continuousAt_inv_log_one

added theorem Real.not_differentiableAt_inv_log_zero

Modified Mathlib/Computability/AkraBazzi/SumTransform.lean

modified theorem AkraBazziRecurrence.deriv_smoothingFn

Modified Mathlib/NumberTheory/AbelSummation.lean

added theorem sum_mul_eq_sub_integral_mul₁

Modified Mathlib/NumberTheory/Chebyshev.lean

added theorem Chebyshev.eventually_primeCounting_le

added theorem Chebyshev.integrableOn_theta_div_id_mul_log_sq

added theorem Chebyshev.integral_one_div_log_sq_isBigO

added theorem Chebyshev.integral_theta_div_log_sq_isBigO

added theorem Chebyshev.integral_theta_div_log_sq_isLittleO

added theorem Chebyshev.intervalIntegrable_one_div_log_sq

added theorem Chebyshev.primeCounting_eq_theta_div_log_add_integral

added theorem Chebyshev.primeCounting_sub_theta_div_log_isBigO