Commit 2026-11-11 18:16 99fb99cb

View on Github →

feat(NumberTheory/LSeries): the (weak) prime number theorem (#43238) This PR adds Mathlib/NumberTheory/LSeries/WeakPNT.lean, deducing the prime number theorem from the Wiener–Ikehara Tauberian theorem (#43233):

Chebyshev.isEquivalent_psi_id: ψ x ~ x
Chebyshev.isEquivalent_theta_id: θ x ~ x
Chebyshev.isEquivalent_primeCounting: the prime number theorem π x ~ x / log x
consecutive-prime asymptotics and prime-gap existence A version of the first three items for arithmetic progressions is also given.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Asymptotics/Lemmas.lean

added theorem Asymptotics.isLittleO_id_iff_tendsto

Modified Mathlib/NumberTheory/Chebyshev.lean

added theorem Chebyshev.isLittleO_card_prime_with_mul_log_sum_prime_log_with

added theorem Chebyshev.isLittleO_primeCounting_mul_log_sub_theta

added theorem Chebyshev.isLittleO_psi_sub_theta_id

added theorem Chebyshev.isLittleO_sum_vonMangoldt_with_sum_prime_log_with

added theorem Chebyshev.sum_range_vonMangoldt_le

Created Mathlib/NumberTheory/LSeries/WeakPNT.lean

added theorem ArithmeticFunction.vonMangoldt.tendsto_sum_modEq_div_atTop

added theorem ArithmeticFunction.vonMangoldt.tendsto_sum_residueClass_div_atTop

added theorem Chebyshev.exists_prime_of_theta_lt

added theorem Chebyshev.isEquivalent_psi_id

added theorem Chebyshev.isEquivalent_theta_id

added theorem Chebyshev.tendsto_psi_div_atTop

added theorem Chebyshev.tendsto_sum_log_prime_modEq_div_atTop

added theorem Chebyshev.tendsto_theta_div_atTop

added theorem Nat.eventually_exists_prime_mem_Ioc

added theorem Nat.eventually_exists_prime_mem_Ioc_sub

added theorem Nat.isEquivalent_card_prime_modEq

added theorem Nat.isEquivalent_log_lcmUpto_id

added theorem Nat.isEquivalent_log_primorial_id

added theorem Nat.isEquivalent_nth_prime_succ

added theorem Nat.isEquivalent_primeCounting

added theorem Nat.tendsto_card_prime_modEq_mul_log_div_atTop

added theorem Nat.tendsto_log_lcmUpto_div_atTop

added theorem Nat.tendsto_log_primorial_div_atTop

Modified docs/1000.yaml