Commit 2025-12-04 09:22 bcfe5664

View on Github →

feat(NumberTheory): define Chebyshev functions (#32247) Defines the Chebyshev psi and theta functions and proves some simple results. Deduces an upper bound on theta using the existing bound on primorials. More substantial results will follow in subsequent PRs. This is the initial PR to upstream some material from the PrimeNumberTheoremAnd project.

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/Chebyshev.lean

added theorem Chebyshev.psi_eq_psi_coe_floor

added theorem Chebyshev.psi_eq_sum_Icc

added theorem Chebyshev.psi_eq_zero_of_lt_two

added theorem Chebyshev.psi_mono

added theorem Chebyshev.psi_nonneg

added theorem Chebyshev.theta_eq_log_primorial

added theorem Chebyshev.theta_eq_sum_Icc

added theorem Chebyshev.theta_eq_theta_coe_floor

added theorem Chebyshev.theta_eq_zero_of_lt_two

added theorem Chebyshev.theta_le_log4_mul_x

added theorem Chebyshev.theta_mono

added theorem Chebyshev.theta_nonneg