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 subgroupmeasure_theory.Lp.bounded_continuous_function
ofLp E p μ
, the additive subgroup ofLp E p μ
consisting of equivalence classes containing a continuous representative, is dense inLp E p μ
.bounded_continuous_function.to_Lp_dense_range
: For finite-measureμ
, the continuous linear mapbounded_continuous_function.to_Lp p μ 𝕜
fromα →ᵇ E
toLp E p μ
has dense range.continuous_map.to_Lp_dense_range
: For compactα
and finite-measureμ
, the continuous linear mapcontinuous_map.to_Lp p μ 𝕜
fromC(α, E)
toLp 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
.
A function in Lp
can be approximated in Lp
by continuous functions.