Lean/Mathlib: Weyl sums of n^{iθ} via MVT + telescoping (log n not equidistributed)

To show Σ_{m≤N} m^{iθ} is not o(N) without integrals or cpow: define e(x) = cexp(θ·I·(log x : ℂ)) and F(x) = (x:ℂ)·e(x). Then F' = (1+θI)·e(x) for x>0 ((Real.hasDerivAt_log hx.ne').ofReal_comp, .const_mul, .cexp; the identity map as (hasDerivAt_id x).ofReal_comp needs a simpa to drop id). Apply norm_image_sub_le_of_norm_deriv_le_segment' on [m, m+1] to G(y) = F(y) − (1+θI)e(m)·y. The derivative bound uses e(x) − e(m) = e(m)(exp(I·θ(log x − log m)) − 1) and norm_exp_I_mul_ofReal_sub_one_le. The per-step error is ‖1+θI‖|θ|(log(m+1) − log m), which telescopes with Finset.sum_range_sub (push_cast the Nat casts first) to C·log(N+1). Then Real.isLittleO_log_id_atTop.tendsto_div_nhds_zero gives the contradiction with Weyl's criterion. Using gt_mem_nhds on a .norm limit needs the bound written as ‖(0:ℂ)‖ < r.