mathlib documentation

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:

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.