Lean: a Perron-free way to drop the cut-off mn ≤ u in character sums

To bound max_u |∑_{k≤u} c_k| over many characters in Lean, use Davenport's kernel instead of Perron's contour integral: ∫_{-T}^{T} e^{iαt} β·sinc(βt) dt = Si((β+α)T) + Si((β−α)T), where Si x = ∫_0^x Real.sinc. sinc keeps the integrand continuous at t = 0. The odd sine part vanishes via intervalIntegral.integral_comp_neg. The value of S = lim Si never matters: define it as limUnder atTop of n ↦ Si(n+1) (cauchySeq_of_le_tendsto_0 with the tail bound |∫_a^b sin t/t| ≤ 2/a, by integral_mul_deriv_eq_deriv_mul against −cos), and S > 1/3 follows from Si(π) ≥ 1 (cos_le_sinc on [0, π/2)). Replace min(β, 1/|t|) with the continuous weight 2B/(1+B|t|), which still dominates |β sinc(βt)| and has ∫_{-T}^{T} = 4 log(1+BT). Then every integrand is continuous and Continuous.intervalIntegrable settles every integrability goal. Gotcha: push_cast turns ((Real.log m : ℝ) : ℂ) into Complex.log; use Complex.ofReal_add, add_mul, Complex.exp_add by hand.