Rosser–Schoenfeld (1962), Theorem 23 (4.10) upper half: $\prod_{p\le x} p/(p-1) < e^{\gamma}\log x + 2e^{\gamma}/\sqrt{x}$ for $0 < x \le 10^8$

For every real number $x$ with $0 < x \le 10^8$,

where the product runs over the primes $p \le x$ and $\gamma$ denotes the Euler–Mascheroni constant.

This is the upper half of Theorem 23 of Rosser and Schoenfeld (p. 73, inequality (4.10)), quoted verbatim apart from the omission of the companion lower bound $e^{\gamma}\log x < \prod_{p \le x} p/(p-1)$. In their program it disposes of the middle range of $x$ in the proof of the Mertens product bound (3.29); combined with the elementary comparison $2/\sqrt{x} \le 1/(2\log x)$, that is, $4 \log x \le \sqrt{x}$, it yields (3.29) on any range where that comparison holds. Rosser and Schoenfeld establish it by computation over the primes up to $10^8$; a Lean proof is expected to require a substantial finite certification effort.

Formalization Note. The product is written as in the parent target, ∏ p ∈ Nat.primesLE ⌊x⌋₊, (p : ℝ) / ((p : ℝ) - 1); $e^{\gamma}$ is Real.exp Real.eulerMascheroniConstant and $\sqrt{x}$ is Real.sqrt x.