Small-prime bounds for the normalization constant

This file isolates the contribution to B_x coming from divisors q < Y. Its main theorem shows that this part is summable and contributes only O(1 / log x) for fixed Y.

Main statements

• summable_normalizationSmallPrimePart_and_tsum_le

noncomputable def PrimitiveSetsAboveX.smallPrimeTailTerm (q m : ℕ) : ℝ

The natural-number kernel in the small-prime tail.

Equations

• PrimitiveSetsAboveX.smallPrimeTailTerm q m = 1 / (↑m * Real.log ↑(m * q) ^ 2)

noncomputable def PrimitiveSetsAboveX.smallPrimeKernel (q : ℕ) (t : ℝ) : ℝ

The corresponding real-variable kernel used for integral comparison.

Equations

• PrimitiveSetsAboveX.smallPrimeKernel q t = 1 / (t * Real.log (t * ↑q) ^ 2)

theorem PrimitiveSetsAboveX.sum_range_smallPrimeTail_le_two_inv_log {x q N : ℕ} (hx : 3 ≤ x) (hq : 0 < q) : (∑ m ∈ Finset.range N, if x ⌈/⌉ q ≤ m then smallPrimeTailTerm q m else 0) ≤ 2 / Real.log ↑x

Every finite prefix of the small-prime tail is bounded by 2 / log x once x ≥ 3. This is the monotone integral comparison specialized to the exact cutoff x ⌈/⌉ q.

theorem PrimitiveSetsAboveX.summable_normalizationSmallPrimePart_and_tsum_le {x Y : ℕ} (hx : 3 ≤ x) : (Summable fun (n : ℕ) => normalizationSmallPrimePart x Y n) ∧ ∑' (n : ℕ), normalizationSmallPrimePart x Y n ≤ (2 * ∑ q ∈ Finset.Ico 1 Y, ArithmeticFunction.vonMangoldt q / ↑q) / Real.log ↑x

For x ≥ 3, the small-prime contribution to B_x is summable, and its total mass is bounded by an explicit O(1 / log x) term depending only on the fixed cutoff Y.