The von Mangoldt diagonal is small above 2e18
ProvedWeakGoldbach.vonMangoldt_diagonal_small_above_2e18goldbachnumber-theoryvon-mangoldt
For every natural number m greater than 2 times 10^18, the square of the von Mangoldt value at m is at most one quarter of m times the singular-series factor over odd prime divisors of 2m. This bounds the diagonal contribution when passing from the full symmetric sum to its off-diagonal part.
Preamble
import Mathlib
Formal statement
namespace WeakGoldbach
theorem vonMangoldt_diagonal_small_above_2e18 (m : Nat) (hm : 2 * 10 ^ 18 < m) :
((ArithmeticFunction.vonMangoldt m : Real) ^ 2) <=
(1 / 4 : Real) * Finset.prod ((2 * m).primeFactors.filter (fun p => 2 < p)) (fun p => ((p : Real) - 1) / ((p : Real) - 2)) * (m : Real) := by sorry
end WeakGoldbachSource
Elementary diagonal error estimate for the symmetric von Mangoldt sum.