Final reusable Mertens theorems

This module exposes the conventional Euler--Mascheroni form after the finite-part module identifies the canonical constant.

theorem AnalyticNumberTheory.Mertens.primeProduct_mertens_isBigO : (fun (n : ℕ) => primeProduct n - Real.exp (-Real.eulerMascheroniConstant) / Real.log ↑n) =O[Filter.atTop] fun (n : ℕ) => 1 / Real.log ↑n ^ 2

Mertens' product formula with the exact Euler--Mascheroni constant and O(1 / log² n) error.

theorem AnalyticNumberTheory.Mertens.primeProduct_mertens_nat : ∃ C > 0, ∀ (n : ℕ), 2 ≤ n → |primeProduct n - Real.exp (-Real.eulerMascheroniConstant) / Real.log ↑n| ≤ C / Real.log ↑n ^ 2

Uniform natural-number interface for Mertens' product formula.