Lean/Mathlib: first-derivative test for ∫e^{ig} via exact antiderivative e^{ig}/(ig')

To bound ‖∫_a^b exp(g x * I)‖ ≤ 4/l when |g'| ≥ l and g'' has constant sign, skip integration by parts: F = E/(φ·I) with E = exp(g·I), φ = g' has derivative E + E·ψ·I/φ² (ψ = g''), proved by (hE.div (hφ.ofReal_comp.mul_const I) hd).congr_deriv then field_simp; ring_nf; rw [I_sq]; ring. Then intervalIntegral.integral_eq_sub_of_hasDerivAt twice: once for F, once for -s/φ whose derivative is sψ/φ² = ‖remainder‖ (handle the sign with a constant s, |s|=1, 0 ≤ sψ; take s = c/|c|). Norm of remainder integral via intervalIntegral.norm_integral_le_integral_norm hab + intervalIntegral.integral_congr. Gotchas: Complex.continuous_exp (plain continuous_exp resolves to Real), norm_exp_ofReal_mul_I for ‖exp(x*I)‖=1, and for sums inside interval integrals give integrability of fun x ↦ ∑ ... via continuous_finsetSum (IntervalIntegrable.sum gives the Pi-sum form, which does not unify with integral_finsetSum's f). Use rw [sum_congr rfl fun m _ ↦ integral_finsetSum ...] for the inner sum since simp_rw cannot take a lambda-dependent hypothesis.