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.

• MeasureTheory.Memℒp.exists_hasCompactSupport_eLpNorm_sub_le states that, in a locally compact space, an ℒp function can be approximated by continuous functions with compact support, in the sense that eLpNorm (f - g) p μ is small.
• MeasureTheory.Memℒp.exists_hasCompactSupport_integral_rpow_sub_le: same result, but expressed in terms of ∫ ‖f - g‖^p.

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.

• MeasureTheory.Lp.boundedContinuousFunction_dense: The subgroup MeasureTheory.Lp.boundedContinuousFunction 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 μ.
• BoundedContinuousFunction.toLp_denseRange: For finite-measure μ, the continuous linear map BoundedContinuousFunction.toLp p μ 𝕜 from α →ᵇ E to Lp E p μ has dense range.
• ContinuousMap.toLp_denseRange: For compact α and finite-measure μ, the continuous linear map ContinuousMap.toLp 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 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 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 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) : ∃ (g : α → E), HasCompactSupport g ∧ MeasureTheory.eLpNorm (f - g) p μ ≤ ε ∧ Continuous g ∧ MeasureTheory.Memℒp g p μ

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) : ∃ (g : α → E), HasCompactSupport g ∧ MeasureTheory.eLpNorm (f - g) p μ ≤ ε ∧ Continuous g ∧ MeasureTheory.Memℒp g p μ

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

theorem MeasureTheory.Lp.boundedContinuousFunction_dense {α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] (E : Type u_2) [NormedAddCommGroup E] (μ : MeasureTheory.Measure α) {p : ENNReal} [NormedSpace ℝ E] [SecondCountableTopologyEither α E] [Fact (1 ≤ p)] (hp : p ≠ ⊤) [μ.WeaklyRegular] : Dense ↑(MeasureTheory.Lp.boundedContinuousFunction E p μ)

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

theorem MeasureTheory.Lp.boundedContinuousFunction_topologicalClosure {α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] (E : Type u_2) [NormedAddCommGroup E] (μ : MeasureTheory.Measure α) {p : ENNReal} [NormedSpace ℝ E] [SecondCountableTopologyEither α E] [Fact (1 ≤ p)] (hp : p ≠ ⊤) [μ.WeaklyRegular] : (MeasureTheory.Lp.boundedContinuousFunction E p μ).topologicalClosure = ⊤

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

theorem BoundedContinuousFunction.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] [μ.WeaklyRegular] [MeasureTheory.IsFiniteMeasure μ] (hp : p ≠ ⊤) : DenseRange ⇑(BoundedContinuousFunction.toLp p μ 𝕜)

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 ≠ ⊤) : DenseRange ⇑(ContinuousMap.toLp 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.