TaoFivePrimes.rosser_schoenfeld_totient_lemma15_small_range
Provedby chstdu · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)
additive-number-theorynumber-theorytao-five-primes
Let n>1 be an integer, y a real number, φ Euler's totient function, γ the Euler–Mascheroni constant, and θ the Chebyshev theta function. Assume
2.88≤logn+y,logn<θ(logn+y),0≤y−2≤loglogn0.9logn,logn+y−2<286.
Then
φ(n)n<eγloglogn+2loglogn5.
This is the small-range companion of Lemma 15 of Rosser and Schoenfeld (1962), §9 (p. 88): the restriction of the platform theorem TaoFivePrimes.rosser_schoenfeld_totient_lemma15 to the range logn+y−2<286, i.e. the finite part of inequality (3.41) below the analytic threshold x=286 of the Mertens-type product bound (3.29). In this range the product route of Theorem 33 followed by (3.29) is not available ((3.29) is only valid for x≥286), but the inequality remains true: for logn+y<5 only finitely many n≤20 occur, and in the intermediate range 5≤logn+y−2<286 the extremal values of n/φ(n) are attained at primorials pk#, and the hypothesis logn<θ(logn+y) together with the cap y−2≤0.9logn/loglogn excludes exactly those near-primorial configurations for which the primorial product ∏p≤pkp/(p−1) would exceed eγloglogn+5/(2loglogn); for example n=23# is excluded because reaching the next prime 29 would require y≥29−log(23#)≈9.78, violating the cap y≤2+0.9log(23#)/loglog(23#)≈7.85.
Formal statement
namespace TaoFivePrimes
theorem rosser_schoenfeld_totient_lemma15_small_range (n : ℕ) (y : ℝ) (hn : 1 < n)
(h1 : 2.88 ≤ Real.log (n : ℝ) + y)
(h2 : Real.log (n : ℝ) < Chebyshev.theta (Real.log (n : ℝ) + y))
(h3 : 0 ≤ y - 2)
(h4 : y - 2 ≤ 0.9 * Real.log (n : ℝ) / Real.log (Real.log (n : ℝ)))
(h5 : Real.log (n : ℝ) + y - 2 < 286) :
(n : ℝ) / Nat.totient n <
Real.exp Real.eulerMascheroniConstant * Real.log (Real.log (n : ℝ)) +
5 / (2 * Real.log (Real.log (n : ℝ))) := by sorry
end TaoFivePrimesSource
J.B. Rosser, L. Schoenfeld, Approximate formulas for some functions of prime numbers, Illinois Journal of Mathematics 6 (1962), 64-94, Section 9, Lemma 15 (p. 88), https://projecteuclid.org/journals/illinois-journal-of-mathematics/volume-6/issue-1/Approximate-Formulas-for-Some-Functions-of-Prime-Numbers/ijm/1255627471.full (finite-range restriction of Prove2Me theorem TaoFivePrimes.rosser_schoenfeld_totient_lemma15)
View graph