The Bombieri-Vinogradov theorem, Bombieri 1965 and A. I. Vinogradov 1965, classical form with the maximum over y <= x
A sorry-free Lean 4 proof of the Bombieri-Vinogradov theorem in its classical form: for every A > 0 there is B > 0 such that the sum over q <= x^{1/2} (log x)^{-B} of the maximum over y <= x and over reduced residues a mod q of |psi(y; q, a) - y/phi(q)| is << x (log x)^{-A}. The same form is proved for theta(y; q, a), for pi(y; q, a) against liD(y)/phi(q) with liD(y) the sum of 1/log n over 2 <= n <= y, and for pi(y; q, a) against pi(y)/phi(q), the level of distribution 1/2 input of sieve methods. The proof runs from a zero-free region for Dirichlet L-functions and Siegel's theorem through…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-22-000026
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-22-000026/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-22-000026/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'