Tail estimates for primitive sets above x

This file proves the logarithmic tail estimate used later in the Markov-chain arguments. It combines the arithmetic input from PrimitiveSetsAboveX.PreliminariesMertens, Abel summation, and explicit calculus on the model kernel 1 / log (mt)^2. The arithmetic input for the Mertens partial sums lives in PrimitiveSetsAboveX.PreliminariesMertens.

Main statements

• tailEstimate

theorem PrimitiveSetsAboveX.tailEstimate : ∃ (C : ℝ), 0 < C ∧ ∀ ⦃m y : ℕ⦄, 1 ≤ m → 2 ≤ y → |tailSum m y - 1 / Real.log ↑(m * y)| ≤ C / Real.log ↑(m * y) ^ 2

The logarithmic tail sum satisfies tailSum m y = 1 / log (my) + O(log(my)⁻²) uniformly for m ≥ 1 and y ≥ 2.