Uniform prime-weighted reciprocal tails and degree cutoffs.

The Mertens lower bound for the prime sum after excluding a finite bad-prime set.

noncomputable def CCDN.mertensError : ℝ

The explicit constant log 4 + 6 + E₁ in Mertens' first theorem: for every x ≥ 1, |∑_{p ≤ x} log p / p - log x| ≤ mertensError (Mertens.prime_sum_bounded_error).

Equations

• CCDN.mertensError = Real.log 4 + 6 + CCDN.Mertens.E₁

theorem CCDN.mertensError_pos : 0 < mertensError

The Mertens error constant mertensError is positive.

theorem CCDN.prime_sum_lower_sdiff {x : ℝ} (hx : 1 ≤ x) (B : Finset ℕ) : Real.log x - mertensError - ∑ p ∈ B, Real.log ↑p / ↑p ≤ ∑ p ∈ Finset.filter Nat.Prime (Finset.Ioc 0 ⌊x⌋₊) \ B, Real.log ↑p / ↑p

The first Mertens estimate retains an explicit charge for excluded primes.

theorem CCDN.prime_mem_upto_iff {t : ℝ} (ht : 0 ≤ t) {p : ℕ} (hp : Nat.Prime p) : p ∈ Finset.filter Nat.Prime (Finset.Ioc 0 ⌊t⌋₊) ↔ ↑p ≤ t

For t ≥ 0, a prime p lies in the set of primes in (0, ⌊t⌋] if and only if p ≤ t.

noncomputable def CCDN.primeBlockMass : ℝ

An explicit constant bounding the prime weight ∑ log p / p over the primes in any interval (L, 4 L] with L ≥ 1.

Equations

• CCDN.primeBlockMass = Real.log 4 + 2 * CCDN.mertensError

theorem CCDN.primeBlockMass_pos : 0 < primeBlockMass

The prime block constant primeBlockMass is positive.

theorem CCDN.prime_interval_weight_le {L T : ℝ} (hL : 1 ≤ L) (hLT : L ≤ T) (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) (hlo : ∀ p ∈ P, L < ↑p) (hhi : ∀ p ∈ P, ↑p ≤ T) : ∑ p ∈ P, Real.log ↑p / ↑p ≤ Real.log T - Real.log L + 2 * mertensError

Mertens bounds an arbitrary prime interval, with its logarithmic width and two absolute error terms.

theorem CCDN.prime_sqrt_tail_le {L : ℝ} (hL : 1 ≤ L) (S : Finset ℕ) (hprime : ∀ p ∈ S, Nat.Prime p) (hlo : ∀ p ∈ S, L < ↑p) : ∑ p ∈ S, Real.log ↑p / ↑p / √↑p ≤ 2 * primeBlockMass / √L

The reciprocal-square-root tail over any finite set of primes is uniform in its upper endpoint.

theorem CCDN.weighted_prime_sum_lower_cutoff {x L C : ℝ} (hx : 1 ≤ x) (hL : 1 ≤ L) (hC : 0 ≤ C) (B : Finset ℕ) (N : ℕ → ℝ) (hN : ∀ p ∈ Finset.filter Nat.Prime (Finset.Ioc 0 ⌊x⌋₊) \ B, L < ↑p → 0 < N p) (hupper : ∀ p ∈ Finset.filter Nat.Prime (Finset.Ioc 0 ⌊x⌋₊) \ B, L < ↑p → N p ≤ ↑p + C * √↑p) : Real.log x - Real.log L - 2 * mertensError - ∑ p ∈ B, Real.log ↑p / ↑p - C * (2 * primeBlockMass / √L) ≤ ∑ p ∈ Finset.filter Nat.Prime (Finset.Ioc 0 ⌊x⌋₊) \ B with L < ↑p, Real.log ↑p / N p

Good-prime reciprocal sum with an explicit lower cutoff. Its error is O(C/sqrt(L)), with absolute constants, and its small-prime cost is log(L).