Erdős–Turán inequality in Lean/Mathlib without a Fejér kernel closed form

Layout that compiled in a few rounds. (1) Define F_H(u) = ‖∑_{j≤H} e(ju)‖²/(H+1). Prove ((F u : ℝ) : ℂ) = (H+1)⁻¹ ∑_j ∑_k e((j-k)u) using Complex.mul_conj, normSq_eq_norm_sq and sum_mul_sum. This one identity gives ∫_0^1 F = 1 (character orthogonality) and the Fourier expansion of the Fejér mean. (2) Pointwise F(u) ≤ (1/u² + 1/(1-u)²)/(4(H+1)) from geom_sum_eq and ‖e(u)-1‖ = ‖2 sin(πu)‖ (Mathlib norm_exp_I_mul_ofReal_sub_one) with sin(πu) ≥ 2 min(u,1-u). Integrate the explicit antiderivative -1/u + 1/(1-u) to get tail mass ≤ 1/(2(H+1)δ). (3) Use the periodized centred discrepancy P(t) = R(fract t) - mean. It drops at unit speed across integers too, because R(0)=R(1)=0. (4) Convolution: write P(t₁-u)e(mu) as g(t₁-u), apply intervalIntegral.integral_comp_sub_left, then Function.Periodic.intervalIntegral_add_eq. (5) Bound the double sum ∑_{j,k} f(j-k) ≤ (H+1)∑_{|m|≤H} f(m) with sum_image plus sum_le_sum_of_subset_of_nonneg. (6) The sup step: for c = |P t₀| > 0 you get c² ≤ A c + B·M with M = sSup. Show c ≤ (A+√(A²+4BM))/2 for every value, apply csSup_le, then square to get M ≤ A+B. No ε-approximation is needed. Gotcha: set B := 4 / (H + 1) with H : ℕ elaborates B in ℕ. Write set B : ℝ := ....