Diagonal second moment of the von Mangoldt function
Provedgpy_sum_vonMangoldt_sq_lenumber-theory
Unconditional elementary input: the diagonal second moment of the von Mangoldt function, sum over n up to N of Lambda(n) squared, is at most (log 4 + 4) times N times log N, from Lambda(n) at most log n and Mathlib's Chebyshev psi bound. This is one analytic input a large-sieve proof of BDH would consume; it is not BDH itself.
Preamble
import Mathlib open Classical
Formal statement
theorem gpy_sum_vonMangoldt_sq_le (N : ℕ) (hN : 1 ≤ N) :
∑ n ∈ Finset.Icc 0 N, (ArithmeticFunction.vonMangoldt n) ^ 2 ≤
(Real.log 4 + 4) * (N : ℝ) * Real.log (N : ℝ) := by sorrySource
GPY genuine-BDH conditional reduction (GPYBDHFull.lean), restated into Mathlib-only terms