Smooth approximation in Lᵖ with control of the support

Mathlib's MeasureTheory.MemLp.exist_eLpNorm_sub_le approximates a function in Lᵖ, p < ∞, by smooth compactly supported functions, with no control on where the approximants live. If the function vanishes off a closed set s, the approximants can be taken to be supported in any neighbourhood t of s, for example a closed thickening Metric.cthickening δ s with δ > 0: multiply an approximant by a smooth cutoff with values in [0, 1] that equals 1 on s and has topological support in t. Multiplying by the cutoff does not increase the distance to the function, which is unchanged by it.

Such support control is what is needed to pass a statement about an operator off the support of its argument from smooth functions to all of Lᵖ.

theorem MeasureTheory.MemLp.exist_contDiff_tsupport_subset_eLpNorm_sub_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : Measure E} [IsFiniteMeasureOnCompacts μ] {p : ENNReal} (hp : p ≠ ⊤) (hp₁ : 1 ≤ p) {f : E → F} (hf : MemLp f p μ) {s t : Set E} (hs : IsClosed s) (ht : t ∈ nhdsSet s) (hfs : ∀ᵐ (y : E) ∂μ, y ∉ s → f y = 0) {ε : ℝ} (hε : 0 < ε) : ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ (↑⊤) g ∧ tsupport g ⊆ t ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε

A function in Lᵖ, 1 ≤ p < ∞, vanishing almost everywhere off a closed set s is the Lᵖ limit of smooth compactly supported functions supported in t, for any neighbourhood t of s.