Uniform approximation by simple functions

Mathlib's MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ is a sequence of simple functions with values in s converging pointwise to a measurable function f whose values lie in the closure of the separable set s (MeasureTheory.SimpleFunc.tendsto_approxOn). When s is totally bounded the convergence is uniform: finitely many points of the dense sequence underlying approxOn already form an ε-net of closure s, and from then on every approximant is within ε of f.

Thus a measurable function with totally bounded range, such as a bounded measurable function into a finite-dimensional normed space, is a uniform limit of measurable finite-range functions whose values stay in any prescribed totally bounded set containing its range. This is the approximation behind integration of bounded measurable functions against projection-valued measures, where uniform rather than pointwise control is needed. It also shows that simple functions are dense in real L∞ for any measure: an essentially bounded function has a bounded measurable representative.

Main statements

• MeasureTheory.SimpleFunc.tendstoUniformlyOn_nearestPt — nearest-point projections onto the initial segments of a sequence converge uniformly to the identity on every totally bounded set in the closure of the sequence.
• MeasureTheory.SimpleFunc.tendstoUniformly_approxOn — for totally bounded s, the simple approximants approxOn f hf s y₀ h₀ n converge to f uniformly.
• MeasureTheory.SimpleFunc.toLpTop μ 𝕜: the class in L∞(μ) of a simple function, as a linear map.
• MeasureTheory.SimpleFunc.denseRange_toLpTop — simple functions are dense in real L∞.
• MeasureTheory.SimpleFunc.integrable_toLp — the class in Lᵖ, 0 < p < ∞, of a simple function is integrable.
• MeasureTheory.SimpleFunc.eLpNorm_eq_top_of_not_memLp — a simple function outside Lᵖ for one exponent 0 < p < ∞ has infinite L^q norm for every 0 < q < ∞.

theorem MeasureTheory.SimpleFunc.tendstoUniformlyOn_nearestPt {α : Type u_1} [MeasurableSpace α] [PseudoEMetricSpace α] [OpensMeasurableSpace α] {e : ℕ → α} {S : Set α} (hS : TotallyBounded S) (hSe : S ⊆ closure (Set.range e)) : TendstoUniformlyOn (fun (N : ℕ) => ⇑(nearestPt e N)) id Filter.atTop S

The nearest-point projections nearestPt e N onto {e 0, …, e N} converge to the identity uniformly on every totally bounded set contained in the closure of the range of e.

theorem MeasureTheory.SimpleFunc.tendstoUniformly_approxOn {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [PseudoEMetricSpace α] [OpensMeasurableSpace α] [MeasurableSpace β] {f : β → α} (hf : Measurable f) {s : Set α} {y₀ : α} (h₀ : y₀ ∈ s) [TopologicalSpace.SeparableSpace ↑s] (hs : TotallyBounded s) (hfs : ∀ (x : β), f x ∈ closure s) : TendstoUniformly (fun (n : ℕ) => ⇑(approxOn f hf s y₀ h₀ n)) f Filter.atTop

If s is totally bounded, the simple approximants approxOn f hf s y₀ h₀ n of a measurable function f with values in the closure of s converge to f uniformly.

noncomputable def MeasureTheory.SimpleFunc.toLpTop {α : Type u_1} [MeasurableSpace α] (μ : Measure α) (𝕜 : Type u_2) {E : Type u_3} [NormedAddCommGroup E] [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] : SimpleFunc α E →ₗ[𝕜] ↥(Lp E ⊤ μ)

The class in L∞(μ) of a simple function, as a linear map. This is Mathlib's MeasureTheory.SimpleFunc.toLp at exponent ∞, where every simple function is essentially bounded whatever the measure.

theorem MeasureTheory.SimpleFunc.coeFn_toLpTop {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {𝕜 : Type u_2} {E : Type u_3} [NormedAddCommGroup E] [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] (f : SimpleFunc α E) : ↑↑((toLpTop μ 𝕜) f) =ᵐ[μ] ⇑f

The class of a simple function in L∞ is almost everywhere the function.

theorem MeasureTheory.SimpleFunc.denseRange_toLpTop {α : Type u_1} [MeasurableSpace α] {μ : Measure α} : DenseRange ⇑(toLpTop μ ℝ)

Simple functions are dense in real L∞, for any measure: an essentially bounded function has a bounded measurable representative, which is a uniform limit of simple functions.

theorem MeasureTheory.SimpleFunc.integrable_toLp {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {E : Type u_2} [NormedAddCommGroup E] {p : ENNReal} {f : SimpleFunc α E} (hp0 : p ≠ 0) (hp : p ≠ ⊤) (hf : MemLp (⇑f) p μ) : Integrable (↑↑(MemLp.toLp (⇑f) hf)) μ

The class in Lᵖ, 0 < p < ∞, of a simple function is integrable: a simple function in Lᵖ has support of finite measure.

theorem MeasureTheory.SimpleFunc.eLpNorm_eq_top_of_not_memLp {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {E : Type u_2} [NormedAddCommGroup E] {p q : ENNReal} {f : SimpleFunc α E} (hp0 : p ≠ 0) (hp : p ≠ ⊤) (hq0 : q ≠ 0) (hq : q ≠ ⊤) (hf : ¬MemLp (⇑f) p μ) : eLpNorm (⇑f) q μ = ⊤

A simple function outside Lᵖ for one exponent 0 < p < ∞ has infinite L^q norm for every 0 < q < ∞.