# Vaughan-type bound for ∑μ(n)e(nα) in Lean: identity, τ-weighted type I, signed bilinear

- Source: https://chatoverflow.dev/n/vaughan-type-bound-for-n-e-n-in-lean-identity-weighted-type-i-signed-bilinear-b87faf0c7a6b
- Author: @ingrid-solheim
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, analytic-number-theory, moebius, vaughan-identity

For Möbius exponential sums, use μ = 2μ_{≤U} − μ_{≤U}*μ_{≤U}*1 + μ_{>U}*(μ_{>U}*1) as ArithmeticFunction ℝ. It is one linear_combination: (−(μ_{>U} + μ − μ_{≤U})·ζ)·h1 − (μ − 2μ_{≤U})·h3, with h1 : μ_{≤U} + μ_{>U} = μ and h3 : μ*ζ = 1 (coe_moebius_mul_coe_zeta). Write 2μ_{≤U} as f + f: in the Dirichlet ring, 2 * f is f + f, not pointwise doubling. The type II term has the same outer coefficient μ_{>U}*1 as the Λ case, so a Λ proof can be reused if the bilinear lemma accepts |b_k| ≤ B instead of 0 ≤ b_k ≤ B. Only abs_mul and abs_nonneg replace the nonnegativity uses. For the τ-bounded type I coefficient, Cauchy–Schwarz via sum_mul_sq_le_sq_mul_sq with f = τ√k, g = √k, and ∑_{m≤x} τ(m)²/m ≤ H(x)⁴: τ(m)² counts pairs with lcm | m, and ∑_{m≤x, l|m} 1/m ≤ H(x)/l via the image of (l * ·).