---
id: F-009
title: Formal Chebyshev upper bound for prime reciprocal sums
tier: lean
polarity: positive
depends_on: [F-008]
supersedes: []
verifier: export PATH="$HOME/.elan/bin:$PATH"; diff -u verified_math/F-009_prime-reciprocal-loglog-upper/lean/Research/PrimeReciprocalBound.lean workspace/experiments/experiment_2_elementary_upper_bound/lean/Research/PrimeReciprocalBound.lean && (cd workspace/experiments/experiment_2_elementary_upper_bound/lean && lake build)
date: 2026-07-11
---

## Statement

There is a positive real constant `E` such that, for all sufficiently large
real `x`,

\[
\sum_{p\le x}\frac1p\le E\log\log x.
\]

Formal theorem:

```lean
theorem eventually_primeReciprocalSum_le_loglog :
  ∃ E : ℝ, 0 < E ∧ ∀ᶠ x : ℝ in atTop,
    primeReciprocalSum x ≤ E * log (log x)
```

The file also proves a global bound
`π(⌊t⌋)/t² ≤ D/(t log t)` for `t≥2` and the exact antiderivative of
`1/(t log t)`.

## Proof / verification

Starting from F-008's formal Abel identity, use Mathlib's kernel-checked
`Chebyshev.eventually_primeCounting_le`.  Below the Chebyshev threshold, the
crude bound `π(⌊t⌋)≤⌊t⌋+1≤2t` is absorbed by enlarging the constant.  Integral
monotonicity and the formally proved identity
`∫₂ˣ dt/(t log t)=log log x-log log 2` give the result.  All step-function
integrability obligations are discharged through Mathlib's Abel-summation
integrability lemma.

Lean accepts the sources in `lean/` with no `sorry`, `admit`, or axioms.
