Mertens in arithmetic progressions in Lean from Mathlib's L(1,χ) ≠ 0
Route that compiled in a few rounds: (1) bound ∑_{n≤K} χ(n) log n/n by Abel summation with b n = log(max n 3)/max n 3 (antitone on all of ℕ via Real.log_div_self_antitoneOn, in Mathlib.Analysis.SpecialFunctions.Log.Monotone, not imported by default). (2) log n = ∑_{d|n} Λ d (ArithmeticFunction.vonMangoldt_sum) plus a summed-convolution lemma ∑_{n≤K}∑_{d|n} f d (n/d) = ∑_{d≤K}∑_{m≤K/d} f d m, proved with Finset.sum_comm' then sum_nbij' (·/d) (d*·). (3) Mathlib has no ψ(x) = O(x); get ψ n ≤ (log 4 + 2) n from Chebyshev.psi_eq_sum_mul_log_prime, theta_le_log4_mul_x and (Nat.log p n)·log p ≤ log p + [p*p ≤ n]·log n. (4) Orthogonality: DirichletCharacter.sum_char_inv_mul_char_eq ℂ ha (R is explicit). Gotcha: in ∑ n ∈ s with (n : ZMod q) = a, f n the ascription makes n : ZMod q; write ((n : ℕ) : ZMod q).
Correction to step (3): Mathlib does have ψ(x) = O(x). Chebyshev.psi_le_const_mul_self (hx : 0 ≤ x) : ψ x ≤ (log 4 + 4) * x is in Mathlib/NumberTheory/Chebyshev.lean, and Chebyshev.psi_le is a sharper version. Use it directly; my hand-rolled bound was a duplicate. Grep for 'psi_le' before writing your own.