Documentation

Mathlib.MeasureTheory.Function.ContinuousMapDense

Approximation in Lᵖ by continuous functions #

This file proves that bounded continuous functions are dense in Lp E p μ, for p < ∞, if the domain α of the functions is a normal topological space and the measure μ is weakly regular. It also proves the same results for approximation by continuous functions with compact support when the space is locally compact and μ is regular.

The result is presented in several versions. First concrete versions giving an approximation up to ε in these various contexts, and then abstract versions stating that the topological closure of the relevant subgroups of Lp are the whole space.

Versions with Integrable instead of Memℒp are specialized to the case p = 1. Versions with boundedContinuous instead of HasCompactSupport drop the locally compact assumption and give only approximation by a bounded continuous function.

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 Mathlib/MeasureTheory/Integral/VitaliCaratheodory.lean.

theorem MeasureTheory.exists_continuous_eLpNorm_sub_le_of_closed {α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] {E : Type u_2} [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [NormedSpace E] [μ.OuterRegular] (hp : p ) {s : Set α} {u : Set α} (s_closed : IsClosed s) (u_open : IsOpen u) (hsu : s u) (hs : μ s ) (c : E) {ε : ENNReal} (hε : ε 0) :
∃ (f : αE), Continuous f MeasureTheory.eLpNorm (fun (x : α) => f x - s.indicator (fun (_y : α) => c) x) p μ ε (∀ (x : α), f x c) Function.support f u MeasureTheory.Memℒp f p μ

A variant of Urysohn's lemma, ℒ^p version, for an outer regular measure μ: consider two sets s ⊆ u which are respectively closed and open with μ s < ∞, and a vector c. Then one may find a continuous function f equal to c on s and to 0 outside of u, bounded by ‖c‖ everywhere, and such that the ℒ^p norm of f - s.indicator (fun y ↦ c) is arbitrarily small. Additionally, this function f belongs to ℒ^p.

@[deprecated MeasureTheory.exists_continuous_eLpNorm_sub_le_of_closed]
theorem MeasureTheory.exists_continuous_snorm_sub_le_of_closed {α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] {E : Type u_2} [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [NormedSpace E] [μ.OuterRegular] (hp : p ) {s : Set α} {u : Set α} (s_closed : IsClosed s) (u_open : IsOpen u) (hsu : s u) (hs : μ s ) (c : E) {ε : ENNReal} (hε : ε 0) :
∃ (f : αE), Continuous f MeasureTheory.eLpNorm (fun (x : α) => f x - s.indicator (fun (_y : α) => c) x) p μ ε (∀ (x : α), f x c) Function.support f u MeasureTheory.Memℒp f p μ

Alias of MeasureTheory.exists_continuous_eLpNorm_sub_le_of_closed.


A variant of Urysohn's lemma, ℒ^p version, for an outer regular measure μ: consider two sets s ⊆ u which are respectively closed and open with μ s < ∞, and a vector c. Then one may find a continuous function f equal to c on s and to 0 outside of u, bounded by ‖c‖ everywhere, and such that the ℒ^p norm of f - s.indicator (fun y ↦ c) is arbitrarily small. Additionally, this function f belongs to ℒ^p.

theorem MeasureTheory.Memℒp.exists_hasCompactSupport_eLpNorm_sub_le {α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] {E : Type u_2} [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [NormedSpace E] [R1Space α] [WeaklyLocallyCompactSpace α] [μ.Regular] (hp : p ) {f : αE} (hf : MeasureTheory.Memℒp f p μ) {ε : ENNReal} (hε : ε 0) :

In a locally compact space, any function in ℒp can be approximated by compactly supported continuous functions when p < ∞, version in terms of eLpNorm.

@[deprecated MeasureTheory.Memℒp.exists_hasCompactSupport_eLpNorm_sub_le]
theorem MeasureTheory.Memℒp.exists_hasCompactSupport_snorm_sub_le {α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] {E : Type u_2} [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [NormedSpace E] [R1Space α] [WeaklyLocallyCompactSpace α] [μ.Regular] (hp : p ) {f : αE} (hf : MeasureTheory.Memℒp f p μ) {ε : ENNReal} (hε : ε 0) :

Alias of MeasureTheory.Memℒp.exists_hasCompactSupport_eLpNorm_sub_le.


In a locally compact space, any function in ℒp can be approximated by compactly supported continuous functions when p < ∞, version in terms of eLpNorm.

theorem MeasureTheory.Memℒp.exists_hasCompactSupport_integral_rpow_sub_le {α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] {E : Type u_2} [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} [NormedSpace E] [R1Space α] [WeaklyLocallyCompactSpace α] [μ.Regular] {p : } (hp : 0 < p) {f : αE} (hf : MeasureTheory.Memℒp f (ENNReal.ofReal p) μ) {ε : } (hε : 0 < ε) :
∃ (g : αE), HasCompactSupport g ∫ (x : α), f x - g x ^ pμ ε Continuous g MeasureTheory.Memℒp g (ENNReal.ofReal p) μ

In a locally compact space, any function in ℒp can be approximated by compactly supported continuous functions when 0 < p < ∞, version in terms of .

theorem MeasureTheory.Integrable.exists_hasCompactSupport_lintegral_sub_le {α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] {E : Type u_2} [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} [NormedSpace E] [R1Space α] [WeaklyLocallyCompactSpace α] [μ.Regular] {f : αE} (hf : MeasureTheory.Integrable f μ) {ε : ENNReal} (hε : ε 0) :
∃ (g : αE), HasCompactSupport g ∫⁻ (x : α), f x - g x‖₊μ ε Continuous g MeasureTheory.Integrable g μ

In a locally compact space, any integrable function can be approximated by compactly supported continuous functions, version in terms of ∫⁻.

theorem MeasureTheory.Integrable.exists_hasCompactSupport_integral_sub_le {α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] {E : Type u_2} [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} [NormedSpace E] [R1Space α] [WeaklyLocallyCompactSpace α] [μ.Regular] {f : αE} (hf : MeasureTheory.Integrable f μ) {ε : } (hε : 0 < ε) :
∃ (g : αE), HasCompactSupport g ∫ (x : α), f x - g xμ ε Continuous g MeasureTheory.Integrable g μ

In a locally compact space, any integrable function can be approximated by compactly supported continuous functions, version in terms of .

theorem MeasureTheory.Memℒp.exists_boundedContinuous_eLpNorm_sub_le {α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] {E : Type u_2} [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [NormedSpace E] [μ.WeaklyRegular] (hp : p ) {f : αE} (hf : MeasureTheory.Memℒp f p μ) {ε : ENNReal} (hε : ε 0) :
∃ (g : BoundedContinuousFunction α E), MeasureTheory.eLpNorm (f - g) p μ ε MeasureTheory.Memℒp (⇑g) p μ

Any function in ℒp can be approximated by bounded continuous functions when p < ∞, version in terms of eLpNorm.

@[deprecated MeasureTheory.Memℒp.exists_boundedContinuous_eLpNorm_sub_le]
theorem MeasureTheory.Memℒp.exists_boundedContinuous_snorm_sub_le {α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] {E : Type u_2} [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [NormedSpace E] [μ.WeaklyRegular] (hp : p ) {f : αE} (hf : MeasureTheory.Memℒp f p μ) {ε : ENNReal} (hε : ε 0) :
∃ (g : BoundedContinuousFunction α E), MeasureTheory.eLpNorm (f - g) p μ ε MeasureTheory.Memℒp (⇑g) p μ

Alias of MeasureTheory.Memℒp.exists_boundedContinuous_eLpNorm_sub_le.


Any function in ℒp can be approximated by bounded continuous functions when p < ∞, version in terms of eLpNorm.

theorem MeasureTheory.Memℒp.exists_boundedContinuous_integral_rpow_sub_le {α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] {E : Type u_2} [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} [NormedSpace E] [μ.WeaklyRegular] {p : } (hp : 0 < p) {f : αE} (hf : MeasureTheory.Memℒp f (ENNReal.ofReal p) μ) {ε : } (hε : 0 < ε) :
∃ (g : BoundedContinuousFunction α E), ∫ (x : α), f x - g x ^ pμ ε MeasureTheory.Memℒp (⇑g) (ENNReal.ofReal p) μ

Any function in ℒp can be approximated by bounded continuous functions when 0 < p < ∞, version in terms of .

theorem MeasureTheory.Integrable.exists_boundedContinuous_lintegral_sub_le {α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] {E : Type u_2} [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} [NormedSpace E] [μ.WeaklyRegular] {f : αE} (hf : MeasureTheory.Integrable f μ) {ε : ENNReal} (hε : ε 0) :
∃ (g : BoundedContinuousFunction α E), ∫⁻ (x : α), f x - g x‖₊μ ε MeasureTheory.Integrable (⇑g) μ

Any integrable function can be approximated by bounded continuous functions, version in terms of ∫⁻.

theorem MeasureTheory.Integrable.exists_boundedContinuous_integral_sub_le {α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] {E : Type u_2} [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} [NormedSpace E] [μ.WeaklyRegular] {f : αE} (hf : MeasureTheory.Integrable f μ) {ε : } (hε : 0 < ε) :
∃ (g : BoundedContinuousFunction α E), ∫ (x : α), f x - g xμ ε MeasureTheory.Integrable (⇑g) μ

Any integrable function can be approximated by bounded continuous functions, version in terms of .

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

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

theorem ContinuousMap.toLp_denseRange {α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] (E : Type u_2) [NormedAddCommGroup E] (μ : MeasureTheory.Measure α) {p : ENNReal} [SecondCountableTopologyEither α E] [_i : Fact (1 p)] (𝕜 : Type u_3) [NormedField 𝕜] [NormedAlgebra 𝕜] [NormedSpace 𝕜 E] [CompactSpace α] [μ.WeaklyRegular] [MeasureTheory.IsFiniteMeasure μ] (hp : p ) :

Continuous functions are dense in MeasureTheory.Lp, 1 ≤ p < ∞. This theorem assumes that the domain is a compact space because otherwise ContinuousMap.toLp is undefined. Use BoundedContinuousFunction.toLp_denseRange if the domain is not a compact space.