Prove2Me

Rosser–Schoenfeld log-product bound (3.29), log form, 700≤x≤108700 \le x \le 10^8

Open
TaoFivePrimes.rosser_schoenfeld_product_log_bound_mid

by chstdu · Sep 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theory

For every real xx with 700≤x≤108700 \le x \le 10^8, the logarithmic form of the Rosser–Schoenfeld product bound (3.29) holds:

∑p≤⌊x⌋log⁡pp−1<γ+log⁡log⁡x+log⁡(1+12log⁡2x),\sum_{p \le \lfloor x \rfloor} \log \frac{p}{p-1} < \gamma + \log \log x + \log\left(1 + \frac{1}{2\log^2 x}\right),

where γ\gamma is the Euler–Mascheroni constant. Exponentiating recovers ∏p≤⌊x⌋pp−1<eγlog⁡x(1+12log⁡2x)\prod_{p \le \lfloor x \rfloor} \frac{p}{p-1} < e^{\gamma}\log x\left(1 + \frac{1}{2\log^2 x}\right) on the same range. This is the middle-range leg of the reduction of rosser_schoenfeld_product_bound, complementing the finite verification below 700700 and the large-range bound rosser_schoenfeld_product_log_bound_large above 10810^8.

Preamble
import Mathlib
Formal statement
namespace TaoFivePrimes
theorem rosser_schoenfeld_product_log_bound_mid (x : ℝ) (hx : 700 ≤ x) (hx' : x ≤ 10 ^ 8) :
    ∑ p ∈ Nat.primesLE ⌊x⌋₊, Real.log ((p : ℝ) / ((p : ℝ) - 1)) <
      Real.eulerMascheroniConstant + Real.log (Real.log x) +
        Real.log (1 + 1 / (2 * (Real.log x) ^ 2)) := by sorry
end TaoFivePrimes
Source
J.B. Rosser, L. Schoenfeld, Approximate formulas for some functions of prime numbers, Illinois J. Math. 6 (1962), 64–94; §8, p. 70, Theorem 8, inequality (3.29). https://doi.org/10.1215/ijm/1255631807

View graph