# mathlibdocumentation

measure_theory.function.continuous_map_dense

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

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.

theorem measure_theory.Lp.bounded_continuous_function_dense {α : Type u_1} [normal_space α] [borel_space α] (E : Type u_2) {p : ennreal} [fact (1 p)] (hp : p ) (μ : measure_theory.measure α) [ E] [μ.weakly_regular] :

A function in Lp can be approximated in Lp by continuous functions.

theorem bounded_continuous_function.to_Lp_dense_range {α : Type u_1} [normal_space α] [borel_space α] (E : Type u_2) {p : ennreal} [fact (1 p)] (hp : p ) (μ : measure_theory.measure α) (𝕜 : Type u_3) [normed_field 𝕜] [ 𝕜] [ E] [μ.weakly_regular]  :
theorem continuous_map.to_Lp_dense_range {α : Type u_1} [normal_space α] [borel_space α] (E : Type u_2) {p : ennreal} [fact (1 p)] (hp : p ) (μ : measure_theory.measure α) (𝕜 : Type u_3) [normed_field 𝕜] [ 𝕜] [ E] [μ.weakly_regular]  :