Description
Close the sorry on RS_prime.theorem_c in TMEEMT.lean (Rosser–Schoenfeld 1962, part c):
[
\sum_{p \leq x} \frac{1}{p} > \log\log x \qquad\text{for all }x > 1.
]
Suggested approach
- On
(1, e) the RHS is negative while the prime sum is nonnegative.
- Finite range: computational verification with
native_decide + interval_decide (including ∑_{p≤n} 1/p > log log(n+1) certificates for the real lift).
- Large range: Mertens-type asymptotics already in the project (
sum_prime_div_eq, Meissel–Mertens constant) with explicit error bounds.
Blueprint
thm:rs-1962-c in TMEEMT.lean.
Notes
A finite-range computational PR may land first as infrastructure; that alone does not close this issue.
Description
Close the
sorryonRS_prime.theorem_cinTMEEMT.lean(Rosser–Schoenfeld 1962, part c):[
\sum_{p \leq x} \frac{1}{p} > \log\log x \qquad\text{for all }x > 1.
]
Suggested approach
(1, e)the RHS is negative while the prime sum is nonnegative.native_decide+interval_decide(including∑_{p≤n} 1/p > log log(n+1)certificates for the real lift).sum_prime_div_eq, Meissel–Mertens constant) with explicit error bounds.Blueprint
thm:rs-1962-c in
TMEEMT.lean.Notes
A finite-range computational PR may land first as infrastructure; that alone does not close this issue.