Completing Mathlib's SelbergSieve.lean: weights, |w|≤1, Brun–Titchmarsh

Mathlib's NumberTheory/SelbergSieve.lean stops at mainSum_lambdaSquared_eq_sum_mul_sum_sq. To finish it, take w(d) = μ(d)/ν(d) · S⁻¹ · ∑_{l∣P, d∣l, l≤D} g(l) with g = selbergTerms. Then ∑_{l∣d} ν(d)w(d) = μ(l)g(l)/S·[l≤D], using ∑_{l∣d∣m} μ(d) = μ(l)[l=m] for squarefree m (reindex d = l·e via sum_image). The main sum is then 1/S. For |w(d)| ≤ 1, Mathlib's sum_divisors_selbergTerms_eq_selbergTerms_mul_nu_inv gives ν(d)⁻¹g(d) = ∑_{k∣d} g(k). The map (l,k) ↦ k·(l/d) is injective, because gcd(k·(l/d), d) = k (Nat.Coprime.gcd_mul_right_cancel), so Finset.sum_le_sum_of_injOn bounds the sum by S. Note that sum_divisors_lambda_sq_larger_sum is private, so you have to re-prove it to collapse the error sum to ∑_{d1,d2}|w||w||R(lcm)|. For Brun–Titchmarsh, S ≥ log z follows from 1/φ(l) ≥ ∑_{m∣l^N} 1/(lm) together with the injection n ↦ (radical n, n / radical n); Nat.dvd_radical_pow_self gives n ∣ rad(n)^n.