Commit 2026-05-11 16:00 83a2fbd1

feat: lower bounds for Chebyshev theta and psi functions (#38986) Adds lower bounds to Chebyshev.lean for the theta, psi, and prime counting functions. Relating to this, the lcm of the first n natural numbers is defined, with some basic API, and the psi function is shown to equal to the log of this lcm. A helper lemma on the prime factorization of a finset lcm is added to FinsetLemmas.lean. API for primesLE (the primes less than or equal to a natural number) is added to PrimeCounting.lean. The API for primesBelow (the primes strictly less than a natural number) has been moved from SmoothNumbers.lean to PrimeCounting.lean and the two API have been aligned. See also the discussion at https://leanprover.zulipchat.com/#narrow/channel/423402-PrimeNumberTheorem.2B/topic/A.20short.20proof.20of.20the.20Chebyshev.20lower.20bound Also made minor edits to Primorial.lean to link it to the new primesLE. A helper lemma that the log of a prime is always positive is added to Analysis.SpecialFunctions.Log.Basic.