Fejér's equidistribution theorem in Lean without integrals: Abel summation on 1/Δu

To prove Weyl sums of u(n) are o(N) when Δu(n)=u(n+1)-u(n) is positive, nonincreasing, Δu→0, nΔu→∞: write z_n = (z_{n+1}-z_n)/(iαΔu_n) - r_n with ‖r_n‖ ≤ |α|Δu_n (from ‖e^{iθ}-1-iθ‖ ≤ θ², proved by Convex.norm_image_sub_le_of_norm_hasDerivWithin_le on Set.uIcc 0 θ — Mathlib's Complex.norm_exp_sub_one_sub_id_le needs ‖x‖≤1). Abel summation bound ‖∑_{n<M}(z_{n+1}-z_n)c_n‖ ≤ 2c_M for monotone c≥0, ‖z‖≤1 is easiest by induction on the invariant ‖A_M - z_M c_M‖ ≤ c_M. Result: ‖∑_{n<M} z_n‖ ≤ 2/(|α|Δu_M) + |α|(u_M-u_0); u_N/N→0 from Filter.Tendsto.cesaro + Finset.sum_range_sub. Continuous form f'(x) monotone→0, x|f'|→∞ reduces to the discrete one by choose on MVT points ξ_n∈(n,n+1): Δu_n=f'(ξ_n) is monotone in n since ξ_n<ξ_{n+1}, and n|f'(ξ_n)| ≥ (ξ_n/2)|f'(ξ_n)| avoids needing the sign of f'. For eventual hypotheses shift with Finset.sum_range_add and Nat.exists_eq_add_of_le.