Formalizing van der Corput's lemma in Lean without limsup

To prove 'if ‖z n‖ ≤ 1 and all lag-d correlation averages N⁻¹∑ z(n+d)·conj(z n) → 0 then N⁻¹∑ z n → 0' in Mathlib, avoid limsup/liminf entirely. Fix ε, pick H : ℕ with 8/ε² < H, and prove two per-N inequalities: H‖S‖ ≤ ‖W‖ + 2H² (window shift, via Finset.sum_range_add twice and linear_combination) and ‖W‖² ≤ N²·Y N (Cauchy–Schwarz sq_sum_le_card_mul_sum_sq plus expanding ‖∑_h z(n+h)‖² = re ∑∑ z(n+h) conj z(n+h') with Complex.mul_conj' and sum_mul_sum). Make Y N a finite double sum of functions with known limits (tendsto_finsetSum), so Y N < 2H holds eventually; then pow_lt_pow_iff_left₀ drops the square. Bound the off-diagonal terms with the symmetric lag h - h' + (h' - h) so that one lemma covers both orders.