Density of simple functions #

Show that each Borel measurable function can be approximated pointwise, and each Lᵖ Borel measurable function can be approximated in Lᵖ norm, by a sequence of simple functions.

Main definitions #

• measure_theory.simple_func.nearest_pt (e : ℕ → α) (N : ℕ) : α →ₛ ℕ: the simple_func sending each x : α to the point e k which is the nearest to x among e 0, ..., e N.
• measure_theory.simple_func.approx_on (f : β → α) (hf : measurable f) (s : set α) (y₀ : α) (h₀ : y₀ ∈ s) [separable_space s] (n : ℕ) : β →ₛ α : a simple function that takes values in s and approximates f.
• measure_theory.Lp.simple_func, the type of Lp simple functions
• coe_to_Lp, the embedding of Lp.simple_func E p μ into Lp E p μ

Main results #

• tendsto_approx_on (pointwise convergence): If f x ∈ s, then the sequence of simple approximations measure_theory.simple_func.approx_on f hf s y₀ h₀ n, evaluated at x, tends to f x as n tends to ∞.
• tendsto_approx_on_univ_Lp (Lᵖ convergence): If E is a normed_group and f is measurable and mem_ℒp (for p < ∞), then the simple functions simple_func.approx_on f hf s 0 h₀ n may be considered as elements of Lp E p μ, and they tend in Lᵖ to f.
• Lp.simple_func.dense_embedding: the embedding coe_to_Lp of the Lp simple functions into Lp is dense.
• Lp.simple_func.induction, Lp.induction, mem_ℒp.induction, integrable.induction: to prove a predicate for all elements of one of these classes of functions, it suffices to check that it behaves correctly on simple functions.

TODO #

For E finite-dimensional, simple functions α →ₛ E are dense in L^∞ -- prove this.

Notations #

• α →ₛ β (local notation): the type of simple functions α → β.
• α →₁ₛ[μ] E: the type of L1 simple functions α → β.

Pointwise approximation by simple functions #

Lp approximation by simple functions #

L1 approximation by simple functions #

Properties of simple functions in Lp spaces #

A simple function f : α →ₛ E into a normed group E verifies, for a measure μ:

• mem_ℒp f 0 μ and mem_ℒp f ∞ μ, since f is a.e.-measurable and bounded,
• for 0 < p < ∞, mem_ℒp f p μ ↔ integrable f μ ↔ f.fin_meas_supp μ ↔ ∀ y ≠ 0, μ (f ⁻¹' {y}) < ∞.

Construction of the space of Lp simple functions, and its dense embedding into Lp.

Simple functions in Lp space form a normed_space.

Implementation note: If Lp.simple_func E p μ were defined as a 𝕜-submodule of Lp E p μ, then the next few lemmas, putting a normed 𝕜-group structure on Lp.simple_func E p μ, would be unnecessary. But instead, Lp.simple_func E p μ is defined as an add_subgroup of Lp E p μ, which does not permit this (but has the advantage of working when E itself is a normed group, i.e. has no scalar action).