Arithmetic preliminaries for primitive sets above x

This file collects the exact divisor identities, factorial decompositions, and bounded-error Mertens estimate used later in the normalization and tail-sum arguments.

Main statements

• mertensEstimate

theorem PrimitiveSetsAboveX.mertensEstimate : ∃ (C : ℝ), 0 < C ∧ ∀ ⦃t : ℕ⦄, 2 ≤ t → |mertensPartialSum t - Real.log ↑t| ≤ C

Bounded-error form of Mertens' estimate: ∑_{q ≤ t} Λ(q) / q = log t + O(1) on the natural numbers.