Fourier series of |sin| in Lean via Mathlib's pointwise Fourier theorem

To prove |sin(πu)| = Σ_{m≥0} 4/(π(2m+1)(2m+3))(1 - cos(2π(m+1)u)): compute fourierCoeffOn zero_lt_one (fun x => (Real.sin (π*x) : ℂ)) n by applying fourierCoeffOn_of_hasDerivAt twice (f(0)=f(1)=0, f'' = -π² f, fourierCoeffOn.const_mul), giving 2/(π(1-4n²)); handle n = 0 separately with intervalIntegral.integral_ofReal + integral_comp_mul_left + integral_sin. Build F : C(UnitAddCircle, ℂ) as ⟨AddCircle.liftIco 1 0 f, AddCircle.liftIco_zero_continuous hf01 hfc.continuousOn⟩ (state hf01 and hfc as separate haves, otherwise by in the anonymous constructor fails with 'expected type not provided'). Then fourierCoeff_liftIco_eq + simpa only [zero_add] using! (as in ZetaValues), has_pointwise_sum_fourier_series_of_summable, HasSum.nat_add_neg and Complex.hasSum_re. Summability: Summable.of_norm_bounded_eventually against 2/π·1/n² (Real.summable_one_div_int_pow, needs Mathlib.Analysis.PSeries), excluding n = 0 via Set.Finite.compl_mem_cofinite. Extend from [0,1] to ℝ with Int.fract and Real.cos_add_int_mul_two_pi / Real.sin_add_int_mul_pi. Payoff: since all terms are ≥ 0, any bound for Σ w_i(1 - cos(mφ_i)) uniform in m gives Σ w_i|sin(φ_i/2)| ≤ (2/π)·bound via hasSum_le.