Bounds on LCM(1..n) in Mathlib

Stream: PrimeNumberTheorem+

[J. J. Issai (project started by GRP)]

Snir Broshi said:

J. J. Issai (project started by GRP) said:

Well I can poorly bound it by $4^{n + c\sqrt{n}}$, and Erd{\o}s can do better with elementary means. However I thought it would have a good bound in MathLib (at least log(lcmint(n)) should be bounded by a constant in Mathlib).

IIUC bounds on it are related to the prime-number-theory so would live in the PNT+ repo, see #general > livestream announcement @ 💬
I suggest asking for this statement in #PrimeNumberTheorem+

I thought there might be a nice bound on LCM(1..n) in Mathlib or in this project. (I'd be happy with log(LCM(1..n)) < 5n.) So I ask on Snir's suggestion, is there? (Of course, above I should have said bounded by a constant times n. Oops.)

[Rushil Raghavan]

I'm not sure if general upper bounds on the expression lcm(1,..,n) specifically are in the project, but if you have log lcm(1,...,n) = Chebyshev psi (n), then we do have the estimate psi(n) < 1.11 n in the Blueprint. The proof is not formalized yet, however.

[Snir Broshi]

If we show

theorem foo (n : ℕ) : ArithmeticFunction.log (L n) = psi n := sorry

then using docs#ArithmeticFunction.vonMangoldt_le_log we could get an upper bound of log (n!) or n log n, which is a start

[Terence Tao]

We have very nearly formalized the bound ψ x ≤ 6 * a * x / 5 + (log (x/5) / log 6) * (5 * log x - 5) for 30 ≤ x, where a = (7/15) * Real.log 2 + (3/10) * Real.log 3 + (1/6) * Real.log 5 is about 0.9213. See https://alexkontorovich.github.io/PrimeNumberTheoremAnd/blueprint/secondary-chapter.html#chebyshev-estimates-sec ; only a few minor sorries remain to finish this off. Ignoring the lower order term, this is a bound roughly of the form $1.105 x$. The optimal constant (if one wants a bound that holds for all $x>0$) is $\psi(x) \leq 1.03883 x$ (due to Rosser and Schoenfeld), which is stated in the blueprint but for which no proof has yet been attempted. The slightly weaker $\psi(x) \leq 1.11 x$, essentially due to Chebyshev, should be doable soon, the main remaining issue is how to deal with the medium range $30 \leq x \leq 10^6$.

docs#Chebyshev.psi_le already has the weaker bound psi x ≤ Real.log 4 * x + 2 * √x * Real.log x which is the same as bounding the lcm by $4^{n+2\sqrt{n}}$ as you initially noted.

It seems that Real.log (L n) = Chebyshev.psi n is not yet in Mathlib; I'll add it to Lcm.lean as some bonus results.

EDIT: docs#primorial_le_4_pow is closely related to the upper bound $L_n \leq 4^{n+2\sqrt{n}}$ since the primorial of $n$ is actually most of $L_n$ already (there is a correction term coming from the primes $p \leq \sqrt{n}$); this may be another route for your specific application.