Approximation in Lᵖ by continuous functions #

This file proves that bounded continuous functions are dense in Lp E p μ, for 1 ≤ p < ∞, if the domain α of the functions is a normal topological space and the measure μ is weakly regular.

The result is presented in several versions:

• measure_theory.Lp.bounded_continuous_function_dense: The subgroup measure_theory.Lp.bounded_continuous_function of Lp E p μ, the additive subgroup of Lp E p μ consisting of equivalence classes containing a continuous representative, is dense in Lp E p μ.
• bounded_continuous_function.to_Lp_dense_range: For finite-measure μ, the continuous linear map bounded_continuous_function.to_Lp p μ 𝕜 from α →ᵇ E to Lp E p μ has dense range.
• continuous_map.to_Lp_dense_range: For compact α and finite-measure μ, the continuous linear map continuous_map.to_Lp p μ 𝕜 from C(α, E) to Lp E p μ has dense range.

Note that for p = ∞ this result is not true: the characteristic function of the set [0, ∞) in ℝ cannot be continuously approximated in L∞.

The proof is in three steps. First, since simple functions are dense in Lp, it suffices to prove the result for a scalar multiple of a characteristic function of a measurable set s. Secondly, since the measure μ is weakly regular, the set s can be approximated above by an open set and below by a closed set. Finally, since the domain α is normal, we use Urysohn's lemma to find a continuous function interpolating between these two sets.

Related results #

Are you looking for a result on "directional" approximation (above or below with respect to an order) of functions whose codomain is ℝ≥0∞ or ℝ, by semicontinuous functions? See the Vitali-Carathéodory theorem, in the file measure_theory.vitali_caratheodory.