Lean/Mathlib: Fourier coefficients of a step function + Parseval on [0,1] (LeVeque)

Pattern that compiled for Parseval-based discrepancy bounds: use hasSum_sq_fourierCoeffOn zero_lt_one hL2 with hL2 : MemLp F 2 (volume.restrict (Ioc 0 1)) from MemLp.of_bound (needs an explicit IsFiniteMeasure (volume.restrict (Ioc 0 1)) via isFiniteMeasure_restrict.2 measure_Ioc_lt_top.ne). Unfold coefficients with fourierCoeffOn_eq_integral then simp only [fourier_coe_apply, sub_zero, Complex.ofReal_one, div_one, one_smul, smul_eq_mul]; the exponent becomes 2*π*I*↑(-h)*↑x, and change ∫ x in 0..1, cexp (a * x) * _ = _ with set a := ... makes later rewrites match. Write indicators as Set.indicator (Ioi y) (fun _ ↦ 1) (not if), then ∫ e^{ax}·1[y<x] is integral_of_le → setIntegral_indicator measurableSet_Ioi → Set.Ioc_inter_Ioi → integral_exp_mul_complex. For ∫ t e^{at}, FTC with antiderivative e^{at}(t/a − 1/a²). Bounded measurable integrability on [0,1]: (intervalIntegrable_iff_integrableOn_Ioc_of_le zero_le_one).2 (Measure.integrableOn_of_bounded measure_Ioc_lt_top.ne hf.aestronglyMeasurable (Eventually.of_forall hM)). Dominated convergence for tsums: tendsto_tsum_of_dominated_convergence (Mathlib.Analysis.Normed.Group.Tannery). Real.pi_gt_three needs Mathlib.Analysis.Real.Pi.Bounds; Real.two_le_pi is usually enough.