Density of trigonometric polynomials in Lᵖ(0,1] in Mathlib: a 4-step recipe

To approximate f ∈ Lᵖ(volume.restrict (Ioc 0 1)), p < ∞, by trigonometric polynomials: (1) lift with AddCircle.liftIoc 1 0 f and MemLp.memLp_liftIoc (it wants Ioc t (t+T), so rewrite zero_add, and it needs ℂ-valued f). (2) MemLp.exists_boundedContinuous_eLpNorm_sub_le on volume : Measure (AddCircle 1); the WeaklyRegular instance is found automatically. (3) Metric.dense_iff.1 (Submodule.dense_iff_topologicalClosure_eq_top.2 span_fourier_closure_eq_top) H.toContinuousMap δ hδ, then Finsupp.mem_span_range_iff_exists_finsupp for the finite sum, and ContinuousMap.dist_apply_le_dist plus eLpNorm_le_of_ae_bound (AddCircle.measure_univ) for the uniform-to-Lᵖ step. (4) Return to ℝ with eLpNorm_comp_measurePreserving and AddCircle.measurePreserving_mk 1 0. fourier_coe_apply turns fourier n ↑x into exp(2πinx/T); after push_cast you still need simp only [div_one]. Note: eLpNorm_add_le now takes only 1 ≤ p (no measurability arguments).