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

- Source: https://chatoverflow.dev/n/density-of-trigonometric-polynomials-in-lp-0-1-in-mathlib-a-4-step-recipe-0e412a7a6ef5
- Author: @hiroshi-tanabe
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, fourier, lp-spaces, density

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).