Approximation in Lᵖ by continuous functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

mem_ℒp.exists_has_compact_support_snorm_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 snorm (f - g) p μ is small.
mem_ℒp.exists_has_compact_support_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 bounded_continuous instead of has_compact_support drop the locally compact assumption and give only approximation by a bounded continuous function.

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.

source

theorem measure_theory.exists_continuous_snorm_sub_le_of_closed {α : Type u_1} [measurable_space α] [topological_space α] [normal_space α] [borel_space α] {E : Type u_2} [normed_add_comm_group E] {μ : measure_theory.measure α} {p : ennreal} [normed_space ℝ E] [μ.outer_regular] (hp : p ≠ ⊤) {s u : set α} (s_closed : is_closed s) (u_open : is_open u) (hsu : s ⊆ u) (hs : ⇑μ s ≠ ⊤) (c : E) {ε : ennreal} (hε : ε ≠ 0) :

∃ (f : α → E), continuous f ∧ measure_theory.snorm (λ (x : α), f x - s.indicator (λ (y : α), c) x) p μ ≤ ε ∧ (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ function.support f ⊆ u ∧ measure_theory.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 (λ y, c) is arbitrarily small. Additionally, this function f belongs to ℒ^p.

source

theorem measure_theory.mem_ℒp.exists_has_compact_support_snorm_sub_le {α : Type u_1} [measurable_space α] [topological_space α] [normal_space α] [borel_space α] {E : Type u_2} [normed_add_comm_group E] {μ : measure_theory.measure α} {p : ennreal} [normed_space ℝ E] [locally_compact_space α] [μ.regular] (hp : p ≠ ⊤) {f : α → E} (hf : measure_theory.mem_ℒp f p μ) {ε : ennreal} (hε : ε ≠ 0) :

∃ (g : α → E), has_compact_support g ∧ measure_theory.snorm (f - g) p μ ≤ ε ∧ continuous g ∧ measure_theory.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 snorm.

source

theorem measure_theory.mem_ℒp.exists_has_compact_support_integral_rpow_sub_le {α : Type u_1} [measurable_space α] [topological_space α] [normal_space α] [borel_space α] {E : Type u_2} [normed_add_comm_group E] {μ : measure_theory.measure α} [normed_space ℝ E] [locally_compact_space α] [μ.regular] {p : ℝ} (hp : 0 < p) {f : α → E} (hf : measure_theory.mem_ℒp f (ennreal.of_real p) μ) {ε : ℝ} (hε : 0 < ε) :

∃ (g : α → E), has_compact_support g ∧ ∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε ∧ continuous g ∧ measure_theory.mem_ℒp g (ennreal.of_real 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 ∫.

source

theorem measure_theory.integrable.exists_has_compact_support_lintegral_sub_le {α : Type u_1} [measurable_space α] [topological_space α] [normal_space α] [borel_space α] {E : Type u_2} [normed_add_comm_group E] {μ : measure_theory.measure α} [normed_space ℝ E] [locally_compact_space α] [μ.regular] {f : α → E} (hf : measure_theory.integrable f μ) {ε : ennreal} (hε : ε ≠ 0) :

∃ (g : α → E), has_compact_support g ∧ ∫⁻ (x : α), ↑‖f x - g x‖₊ ∂μ ≤ ε ∧ continuous g ∧ measure_theory.integrable g μ

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

source

theorem measure_theory.integrable.exists_has_compact_support_integral_sub_le {α : Type u_1} [measurable_space α] [topological_space α] [normal_space α] [borel_space α] {E : Type u_2} [normed_add_comm_group E] {μ : measure_theory.measure α} [normed_space ℝ E] [locally_compact_space α] [μ.regular] {f : α → E} (hf : measure_theory.integrable f μ) {ε : ℝ} (hε : 0 < ε) :

∃ (g : α → E), has_compact_support g ∧ ∫ (x : α), ‖f x - g x‖ ∂μ ≤ ε ∧ continuous g ∧ measure_theory.integrable g μ

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

source

theorem measure_theory.mem_ℒp.exists_bounded_continuous_snorm_sub_le {α : Type u_1} [measurable_space α] [topological_space α] [normal_space α] [borel_space α] {E : Type u_2} [normed_add_comm_group E] {μ : measure_theory.measure α} {p : ennreal} [normed_space ℝ E] [μ.weakly_regular] (hp : p ≠ ⊤) {f : α → E} (hf : measure_theory.mem_ℒp f p μ) {ε : ennreal} (hε : ε ≠ 0) :

∃ (g : bounded_continuous_function α E), measure_theory.snorm (f - ⇑g) p μ ≤ ε ∧ measure_theory.mem_ℒp ⇑g p μ

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

source

theorem measure_theory.mem_ℒp.exists_bounded_continuous_integral_rpow_sub_le {α : Type u_1} [measurable_space α] [topological_space α] [normal_space α] [borel_space α] {E : Type u_2} [normed_add_comm_group E] {μ : measure_theory.measure α} [normed_space ℝ E] [μ.weakly_regular] {p : ℝ} (hp : 0 < p) {f : α → E} (hf : measure_theory.mem_ℒp f (ennreal.of_real p) μ) {ε : ℝ} (hε : 0 < ε) :

∃ (g : bounded_continuous_function α E), ∫ (x : α), ‖f x - ⇑g x‖ ^ p ∂μ ≤ ε ∧ measure_theory.mem_ℒp ⇑g (ennreal.of_real p) μ

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

source

theorem measure_theory.integrable.exists_bounded_continuous_lintegral_sub_le {α : Type u_1} [measurable_space α] [topological_space α] [normal_space α] [borel_space α] {E : Type u_2} [normed_add_comm_group E] {μ : measure_theory.measure α} [normed_space ℝ E] [μ.weakly_regular] {f : α → E} (hf : measure_theory.integrable f μ) {ε : ennreal} (hε : ε ≠ 0) :

∃ (g : bounded_continuous_function α E), ∫⁻ (x : α), ↑‖f x - ⇑g x‖₊ ∂μ ≤ ε ∧ measure_theory.integrable ⇑g μ

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

source

theorem measure_theory.integrable.exists_bounded_continuous_integral_sub_le {α : Type u_1} [measurable_space α] [topological_space α] [normal_space α] [borel_space α] {E : Type u_2} [normed_add_comm_group E] {μ : measure_theory.measure α} [normed_space ℝ E] [μ.weakly_regular] {f : α → E} (hf : measure_theory.integrable f μ) {ε : ℝ} (hε : 0 < ε) :

∃ (g : bounded_continuous_function α E), ∫ (x : α), ‖f x - ⇑g x‖ ∂μ ≤ ε ∧ measure_theory.integrable ⇑g μ

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

source

theorem measure_theory.Lp.bounded_continuous_function_dense {α : Type u_1} [measurable_space α] [topological_space α] [normal_space α] [borel_space α] (E : Type u_2) [normed_add_comm_group E] {μ : measure_theory.measure α} {p : ennreal} [normed_space ℝ E] [second_countable_topology_either α E] [fact (1 ≤ p)] (hp : p ≠ ⊤) [μ.weakly_regular] :

(measure_theory.Lp.bounded_continuous_function E p μ).topological_closure = ⊤

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

source

theorem bounded_continuous_function.to_Lp_dense_range {α : Type u_1} [measurable_space α] [topological_space α] [normal_space α] [borel_space α] (E : Type u_2) [normed_add_comm_group E] (μ : measure_theory.measure α) {p : ennreal} [second_countable_topology_either α E] [fact (1 ≤ p)] (hp : p ≠ ⊤) (𝕜 : Type u_3) [normed_field 𝕜] [normed_algebra ℝ 𝕜] [normed_space 𝕜 E] [μ.weakly_regular] [measure_theory.is_finite_measure μ] :

dense_range ⇑(bounded_continuous_function.to_Lp p μ 𝕜)

source

theorem continuous_map.to_Lp_dense_range {α : Type u_1} [measurable_space α] [topological_space α] [normal_space α] [borel_space α] (E : Type u_2) [normed_add_comm_group E] (μ : measure_theory.measure α) {p : ennreal} [second_countable_topology_either α E] [fact (1 ≤ p)] (hp : p ≠ ⊤) (𝕜 : Type u_3) [normed_field 𝕜] [normed_algebra ℝ 𝕜] [normed_space 𝕜 E] [compact_space α] [μ.weakly_regular] [measure_theory.is_finite_measure μ] :

dense_range ⇑(continuous_map.to_Lp p μ 𝕜)

Approximation in Lᵖ by continuous functions #

Related results #