Mawia small-range reciprocal-prime upper bound

Proved

TaoFivePrimes.mawia_reciprocal_sum_upper_bound_small

by Eyal1990 · Sep 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

analytic-number-theorymertens-theoremprimes

For every real x with 2 ≤ x ≤ 10^8, the reciprocal-prime sum through x is at most the logarithmic main term plus the Meissel–Mertens constant and 4/(log x)^3.

Preamble

import Mathlib

Formal statement

namespace TaoFivePrimes
theorem mawia_reciprocal_sum_upper_bound_small (x : ℝ) (hx : 2 ≤ x) (hsmall : x ≤ 10 ^ 8) :
    (∑ p ∈ Nat.primesLE ⌊x⌋₊, 1 / (p : ℝ)) ≤
      Real.log (Real.log x) +
        (Real.eulerMascheroniConstant +
          ∑' p : Nat.Primes, (Real.log (1 - 1 / (p : ℝ)) + 1 / (p : ℝ))) +
        4 / (Real.log x) ^ 3 := by
  sorry
end TaoFivePrimes

Source

R. Mawia, “Explicit estimates for some summatory functions of primes,” Integers 17 (2017), Theorem 10.12.30 (Mawia reciprocal-prime estimate; source given on the parent theorem as section 2).

View graph