# mathlib3documentation

measure_theory.function.simple_func_dense_lp

# Density of simple functions #

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

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

## Main definitions #

• `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_univ_Lp` (Lᵖ convergence): If `E` is a `normed_add_comm_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 `α → β`.

### Lp approximation by simple functions #

theorem measure_theory.simple_func.nnnorm_approx_on_le {β : Type u_2} {E : Type u_4} {f : β E} (hf : measurable f) {s : set E} {y₀ : E} (h₀ : y₀ s) (x : β) (n : ) :
y₀ h₀ n) x - f x‖₊ f x - y₀‖₊
theorem measure_theory.simple_func.norm_approx_on_y₀_le {β : Type u_2} {E : Type u_4} {f : β E} (hf : measurable f) {s : set E} {y₀ : E} (h₀ : y₀ s) (x : β) (n : ) :
y₀ h₀ n) x - y₀ f x - y₀ + f x - y₀
theorem measure_theory.simple_func.norm_approx_on_zero_le {β : Type u_2} {E : Type u_4} {f : β E} (hf : measurable f) {s : set E} (h₀ : 0 s) (x : β) (n : ) :
0 h₀ n) x f x + f x
theorem measure_theory.simple_func.tendsto_approx_on_Lp_snorm {β : Type u_2} {E : Type u_4} {p : ennreal} {f : β E} (hf : measurable f) {s : set E} {y₀ : E} (h₀ : y₀ s) (hp_ne_top : p ) {μ : measure_theory.measure β} (hμ : ∀ᵐ (x : β) μ, f x ) (hi : measure_theory.snorm (λ (x : β), f x - y₀) p μ < ) :
filter.tendsto (λ (n : ), measure_theory.snorm ( y₀ h₀ n) - f) p μ) filter.at_top (nhds 0)
theorem measure_theory.simple_func.mem_ℒp_approx_on {β : Type u_2} {E : Type u_4} {p : ennreal} [borel_space E] {f : β E} {μ : measure_theory.measure β} (fmeas : measurable f) (hf : μ) {s : set E} {y₀ : E} (h₀ : y₀ s) (hi₀ : measure_theory.mem_ℒp (λ (x : β), y₀) p μ) (n : ) :
measure_theory.mem_ℒp s y₀ h₀ n) p μ
theorem measure_theory.simple_func.tendsto_approx_on_range_Lp_snorm {β : Type u_2} {E : Type u_4} {p : ennreal} [borel_space E] {f : β E} (hp_ne_top : p ) {μ : measure_theory.measure β} (fmeas : measurable f) [topological_space.separable_space {0})] (hf : μ < ) :
filter.tendsto (λ (n : ), measure_theory.snorm ( {0}) 0 _ n) - f) p μ) filter.at_top (nhds 0)
theorem measure_theory.simple_func.mem_ℒp_approx_on_range {β : Type u_2} {E : Type u_4} {p : ennreal} [borel_space E] {f : β E} {μ : measure_theory.measure β} (fmeas : measurable f) [topological_space.separable_space {0})] (hf : μ) (n : ) :
theorem measure_theory.simple_func.tendsto_approx_on_range_Lp {β : Type u_2} {E : Type u_4} {p : ennreal} [borel_space E] {f : β E} [hp : fact (1 p)] (hp_ne_top : p ) {μ : measure_theory.measure β} (fmeas : measurable f) [topological_space.separable_space {0})] (hf : μ) :
theorem measure_theory.mem_ℒp.exists_simple_func_snorm_sub_lt {β : Type u_2} {p : ennreal} {E : Type u_1} {f : β E} {μ : measure_theory.measure β} (hf : μ) (hp_ne_top : p ) {ε : ennreal} (hε : ε 0) :
(g : , measure_theory.snorm (f - g) p μ < ε

Any function in `ℒp` can be approximated by a simple function if `p < ∞`.

### L1 approximation by simple functions #

theorem measure_theory.simple_func.tendsto_approx_on_L1_nnnorm {β : Type u_2} {E : Type u_4} {f : β E} (hf : measurable f) {s : set E} {y₀ : E} (h₀ : y₀ s) {μ : measure_theory.measure β} (hμ : ∀ᵐ (x : β) μ, f x ) (hi : measure_theory.has_finite_integral (λ (x : β), f x - y₀) μ) :
filter.tendsto (λ (n : ), ∫⁻ (x : β), y₀ h₀ n) x - f x‖₊ μ) filter.at_top (nhds 0)
theorem measure_theory.simple_func.integrable_approx_on {β : Type u_2} {E : Type u_4} [borel_space E] {f : β E} {μ : measure_theory.measure β} (fmeas : measurable f) (hf : μ) {s : set E} {y₀ : E} (h₀ : y₀ s) (hi₀ : measure_theory.integrable (λ (x : β), y₀) μ) (n : ) :
measure_theory.integrable s y₀ h₀ n) μ
theorem measure_theory.simple_func.tendsto_approx_on_range_L1_nnnorm {β : Type u_2} {E : Type u_4} {f : β E} {μ : measure_theory.measure β} [topological_space.separable_space {0})] (fmeas : measurable f) (hf : μ) :
filter.tendsto (λ (n : ), ∫⁻ (x : β), {0}) 0 _ n) x - f x‖₊ μ) filter.at_top (nhds 0)

### 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}) < ∞`.
theorem measure_theory.simple_func.exists_forall_norm_le {α : Type u_1} {F : Type u_5} (f : F) :
(C : ), (x : α), f x C
theorem measure_theory.simple_func.mem_ℒp_zero {α : Type u_1} {E : Type u_4} (f : E) (μ : measure_theory.measure α) :
theorem measure_theory.simple_func.mem_ℒp_top {α : Type u_1} {E : Type u_4} (f : E) (μ : measure_theory.measure α) :
@[protected]
theorem measure_theory.simple_func.snorm'_eq {α : Type u_1} {F : Type u_5} {p : } (f : F) (μ : measure_theory.measure α) :
= f.range.sum (λ (y : F), y‖₊ ^ p * μ (f ⁻¹' {y})) ^ (1 / p)
theorem measure_theory.simple_func.measure_preimage_lt_top_of_mem_ℒp {α : Type u_1} {E : Type u_4} {μ : measure_theory.measure α} {p : ennreal} (hp_pos : p 0) (hp_ne_top : p ) (f : E) (hf : μ) (y : E) (hy_ne : y 0) :
μ (f ⁻¹' {y}) <
theorem measure_theory.simple_func.mem_ℒp_of_finite_measure_preimage {α : Type u_1} {E : Type u_4} {μ : measure_theory.measure α} (p : ennreal) {f : E} (hf : (y : E), y 0 μ (f ⁻¹' {y}) < ) :
theorem measure_theory.simple_func.mem_ℒp_iff {α : Type u_1} {E : Type u_4} {μ : measure_theory.measure α} {p : ennreal} {f : E} (hp_pos : p 0) (hp_ne_top : p ) :
(y : E), y 0 μ (f ⁻¹' {y}) <
theorem measure_theory.simple_func.integrable_iff {α : Type u_1} {E : Type u_4} {μ : measure_theory.measure α} {f : E} :
(y : E), y 0 μ (f ⁻¹' {y}) <
theorem measure_theory.simple_func.mem_ℒp_iff_integrable {α : Type u_1} {E : Type u_4} {μ : measure_theory.measure α} {p : ennreal} {f : E} (hp_pos : p 0) (hp_ne_top : p ) :
theorem measure_theory.simple_func.mem_ℒp_iff_fin_meas_supp {α : Type u_1} {E : Type u_4} {μ : measure_theory.measure α} {p : ennreal} {f : E} (hp_pos : p 0) (hp_ne_top : p ) :
theorem measure_theory.simple_func.fin_meas_supp.integrable {α : Type u_1} {E : Type u_4} {μ : measure_theory.measure α} {f : E} (h : f.fin_meas_supp μ) :
theorem measure_theory.simple_func.integrable_pair {α : Type u_1} {E : Type u_4} {F : Type u_5} {μ : measure_theory.measure α} {f : E} {g : F} :
theorem measure_theory.simple_func.measure_preimage_lt_top_of_integrable {α : Type u_1} {E : Type u_4} {μ : measure_theory.measure α} (f : E) (hf : μ) {x : E} (hx : x 0) :
μ (f ⁻¹' {x}) <
theorem measure_theory.simple_func.measure_support_lt_top {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [has_zero β] (f : β) (hf : (y : β), y 0 μ (f ⁻¹' {y}) < ) :
theorem measure_theory.simple_func.measure_support_lt_top_of_mem_ℒp {α : Type u_1} {E : Type u_4} {μ : measure_theory.measure α} {p : ennreal} (f : E) (hf : μ) (hp_ne_zero : p 0) (hp_ne_top : p ) :
theorem measure_theory.simple_func.measure_support_lt_top_of_integrable {α : Type u_1} {E : Type u_4} {μ : measure_theory.measure α} (f : E) (hf : μ) :
theorem measure_theory.simple_func.measure_lt_top_of_mem_ℒp_indicator {α : Type u_1} {E : Type u_4} {μ : measure_theory.measure α} {p : ennreal} (hp_pos : p 0) (hp_ne_top : p ) {c : E} (hc : c 0) {s : set α} (hs : measurable_set s) (hcs : μ) :
μ s <

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

def measure_theory.Lp.simple_func {α : Type u_1} (E : Type u_4) (p : ennreal) (μ : measure_theory.measure α) :

`Lp.simple_func` is a subspace of Lp consisting of equivalence classes of an integrable simple function.

Equations
Instances for `↥measure_theory.Lp.simple_func`

Simple functions in Lp space form a `normed_space`.

@[norm_cast]
theorem measure_theory.Lp.simple_func.coe_coe {α : Type u_1} {E : Type u_4} {p : ennreal} {μ : measure_theory.measure α} (f : ) :
@[protected]
theorem measure_theory.Lp.simple_func.eq' {α : Type u_1} {E : Type u_4} {p : ennreal} {μ : measure_theory.measure α} {f g : } :
f = g f = g

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

@[protected]
def measure_theory.Lp.simple_func.has_smul {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} {p : ennreal} {μ : measure_theory.measure α} [normed_ring 𝕜] [ E] [ E] :

If `E` is a normed space, `Lp.simple_func E p μ` is a `has_smul`. Not declared as an instance as it is (as of writing) used only in the construction of the Bochner integral.

Equations
@[simp, norm_cast]
theorem measure_theory.Lp.simple_func.coe_smul {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} {p : ennreal} {μ : measure_theory.measure α} [normed_ring 𝕜] [ E] [ E] (c : 𝕜) (f : ) :
(c f) = c f
@[protected]
def measure_theory.Lp.simple_func.module {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} {p : ennreal} {μ : measure_theory.measure α} [normed_ring 𝕜] [ E] [ E] :

If `E` is a normed space, `Lp.simple_func E p μ` is a module. Not declared as an instance as it is (as of writing) used only in the construction of the Bochner integral.

Equations
@[protected]
theorem measure_theory.Lp.simple_func.has_bounded_smul {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} {p : ennreal} {μ : measure_theory.measure α} [normed_ring 𝕜] [ E] [ E] [fact (1 p)] :

If `E` is a normed space, `Lp.simple_func E p μ` is a normed space. Not declared as an instance as it is (as of writing) used only in the construction of the Bochner integral.

@[protected]
def measure_theory.Lp.simple_func.normed_space {α : Type u_1} {E : Type u_4} {p : ennreal} {μ : measure_theory.measure α} {𝕜 : Type u_2} [normed_field 𝕜] [ E] [fact (1 p)] :

If `E` is a normed space, `Lp.simple_func E p μ` is a normed space. Not declared as an instance as it is (as of writing) used only in the construction of the Bochner integral.

Equations
@[reducible]
def measure_theory.Lp.simple_func.to_Lp {α : Type u_1} {E : Type u_4} {p : ennreal} {μ : measure_theory.measure α} (f : E) (hf : μ) :

Construct the equivalence class `[f]` of a simple function `f` satisfying `mem_ℒp`.

Equations
theorem measure_theory.Lp.simple_func.to_Lp_eq_to_Lp {α : Type u_1} {E : Type u_4} {p : ennreal} {μ : measure_theory.measure α} (f : E) (hf : μ) :
theorem measure_theory.Lp.simple_func.to_Lp_eq_mk {α : Type u_1} {E : Type u_4} {p : ennreal} {μ : measure_theory.measure α} (f : E) (hf : μ) :
theorem measure_theory.Lp.simple_func.to_Lp_add {α : Type u_1} {E : Type u_4} {p : ennreal} {μ : measure_theory.measure α} (f g : E) (hf : μ) (hg : μ) :
theorem measure_theory.Lp.simple_func.to_Lp_neg {α : Type u_1} {E : Type u_4} {p : ennreal} {μ : measure_theory.measure α} (f : E) (hf : μ) :
theorem measure_theory.Lp.simple_func.to_Lp_sub {α : Type u_1} {E : Type u_4} {p : ennreal} {μ : measure_theory.measure α} (f g : E) (hf : μ) (hg : μ) :
theorem measure_theory.Lp.simple_func.to_Lp_smul {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} {p : ennreal} {μ : measure_theory.measure α} [normed_ring 𝕜] [ E] [ E] (f : E) (hf : μ) (c : 𝕜) :
theorem measure_theory.Lp.simple_func.norm_to_Lp {α : Type u_1} {E : Type u_4} {p : ennreal} {μ : measure_theory.measure α} [fact (1 p)] (f : E) (hf : μ) :
noncomputable def measure_theory.Lp.simple_func.to_simple_func {α : Type u_1} {E : Type u_4} {p : ennreal} {μ : measure_theory.measure α} (f : ) :

Find a representative of a `Lp.simple_func`.

Equations
@[protected, measurability]
theorem measure_theory.Lp.simple_func.measurable {α : Type u_1} {E : Type u_4} {p : ennreal} {μ : measure_theory.measure α} (f : ) :

`(to_simple_func f)` is measurable.

@[protected]
theorem measure_theory.Lp.simple_func.strongly_measurable {α : Type u_1} {E : Type u_4} {p : ennreal} {μ : measure_theory.measure α} (f : ) :
@[protected, measurability]
theorem measure_theory.Lp.simple_func.ae_measurable {α : Type u_1} {E : Type u_4} {p : ennreal} {μ : measure_theory.measure α} (f : ) :
@[protected]
@[protected]
theorem measure_theory.Lp.simple_func.mem_ℒp {α : Type u_1} {E : Type u_4} {p : ennreal} {μ : measure_theory.measure α} (f : ) :

`to_simple_func f` satisfies the predicate `mem_ℒp`.

theorem measure_theory.Lp.simple_func.to_simple_func_to_Lp {α : Type u_1} {E : Type u_4} {p : ennreal} {μ : measure_theory.measure α} (f : E) (hfi : μ) :
theorem measure_theory.Lp.simple_func.add_to_simple_func {α : Type u_1} {E : Type u_4} {p : ennreal} {μ : measure_theory.measure α} (f g : ) :
theorem measure_theory.Lp.simple_func.sub_to_simple_func {α : Type u_1} {E : Type u_4} {p : ennreal} {μ : measure_theory.measure α} (f g : ) :
theorem measure_theory.Lp.simple_func.smul_to_simple_func {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} {p : ennreal} {μ : measure_theory.measure α} [normed_ring 𝕜] [ E] [ E] (k : 𝕜) (f : ) :
theorem measure_theory.Lp.simple_func.norm_to_simple_func {α : Type u_1} {E : Type u_4} {p : ennreal} {μ : measure_theory.measure α} [fact (1 p)] (f : ) :
noncomputable def measure_theory.Lp.simple_func.indicator_const {α : Type u_1} {E : Type u_4} (p : ennreal) {μ : measure_theory.measure α} {s : set α} (hs : measurable_set s) (hμs : μ s ) (c : E) :

The characteristic function of a finite-measure measurable set `s`, as an `Lp` simple function.

Equations
@[simp]
theorem measure_theory.Lp.simple_func.coe_indicator_const {α : Type u_1} {E : Type u_4} {p : ennreal} {μ : measure_theory.measure α} {s : set α} (hs : measurable_set s) (hμs : μ s ) (c : E) :
c) = c
theorem measure_theory.Lp.simple_func.to_simple_func_indicator_const {α : Type u_1} {E : Type u_4} {p : ennreal} {μ : measure_theory.measure α} {s : set α} (hs : measurable_set s) (hμs : μ s ) (c : E) :
@[protected]
theorem measure_theory.Lp.simple_func.induction {α : Type u_1} {E : Type u_4} {p : ennreal} {μ : measure_theory.measure α} (hp_pos : p 0) (hp_ne_top : p ) {P : Prop} (h_ind : (c : E) {s : set α} (hs : (hμs : μ s < ), P ) (h_add : ⦃f g : ⦄ (hf : μ) (hg : μ), ) (f : ) :
P f

To prove something for an arbitrary `Lp` simple function, with `0 < p < ∞`, it suffices to show that the property holds for (multiples of) characteristic functions of finite-measure measurable sets and is closed under addition (of functions with disjoint support).

@[protected]
theorem measure_theory.Lp.simple_func.uniform_continuous {α : Type u_1} {E : Type u_4} {p : ennreal} {μ : measure_theory.measure α} [fact (1 p)] :
@[protected]
theorem measure_theory.Lp.simple_func.uniform_embedding {α : Type u_1} {E : Type u_4} {p : ennreal} {μ : measure_theory.measure α} [fact (1 p)] :
@[protected]
theorem measure_theory.Lp.simple_func.uniform_inducing {α : Type u_1} {E : Type u_4} {p : ennreal} {μ : measure_theory.measure α} [fact (1 p)] :
@[protected]
theorem measure_theory.Lp.simple_func.dense_embedding {α : Type u_1} {E : Type u_4} {p : ennreal} {μ : measure_theory.measure α} [fact (1 p)] (hp_ne_top : p ) :
@[protected]
theorem measure_theory.Lp.simple_func.dense_inducing {α : Type u_1} {E : Type u_4} {p : ennreal} {μ : measure_theory.measure α} [fact (1 p)] (hp_ne_top : p ) :
@[protected]
theorem measure_theory.Lp.simple_func.dense_range {α : Type u_1} {E : Type u_4} {p : ennreal} {μ : measure_theory.measure α} [fact (1 p)] (hp_ne_top : p ) :
def measure_theory.Lp.simple_func.coe_to_Lp (α : Type u_1) (E : Type u_4) (𝕜 : Type u_6) {p : ennreal} {μ : measure_theory.measure α} [fact (1 p)] [normed_ring 𝕜] [ E] [ E] :
→L[𝕜] μ)

The embedding of Lp simple functions into Lp functions, as a continuous linear map.

Equations
theorem measure_theory.Lp.simple_func.coe_fn_le {α : Type u_1} {p : ennreal} {μ : measure_theory.measure α} {G : Type u_7} (f g : ) :
@[protected, instance]
theorem measure_theory.Lp.simple_func.coe_fn_zero {α : Type u_1} (p : ennreal) (μ : measure_theory.measure α) (G : Type u_7)  :
0 =ᵐ[μ] 0
theorem measure_theory.Lp.simple_func.coe_fn_nonneg {α : Type u_1} {p : ennreal} {μ : measure_theory.measure α} {G : Type u_7} (f : ) :
0 ≤ᵐ[μ] f 0 f
theorem measure_theory.Lp.simple_func.exists_simple_func_nonneg_ae_eq {α : Type u_1} {p : ennreal} {μ : measure_theory.measure α} {G : Type u_7} {f : } (hf : 0 f) :
(f' : , 0 f' f =ᵐ[μ] f'
def measure_theory.Lp.simple_func.coe_simple_func_nonneg_to_Lp_nonneg {α : Type u_1} (p : ennreal) (μ : measure_theory.measure α) (G : Type u_7)  :
{g // 0 g} {g // 0 g}

Coercion from nonnegative simple functions of Lp to nonnegative functions of Lp.

Equations
theorem measure_theory.Lp.induction {α : Type u_1} {E : Type u_4} {p : ennreal} {μ : measure_theory.measure α} [fact (1 p)] (hp_ne_top : p ) (P : μ) Prop) (h_ind : (c : E) {s : set α} (hs : (hμs : μ s < ), P ) (h_add : ⦃f g : α E⦄ (hf : μ) (hg : μ), P P P ) (h_closed : is_closed {f : μ) | P f}) (f : μ)) :
P f

To prove something for an arbitrary `Lp` function in a second countable Borel normed group, it suffices to show that

• the property holds for (multiples of) characteristic functions;
• the set of functions in `Lp` for which the property holds is closed.
theorem measure_theory.mem_ℒp.induction {α : Type u_1} {E : Type u_4} {p : ennreal} {μ : measure_theory.measure α} [fact (1 p)] (hp_ne_top : p ) (P : E) Prop) (h_ind : (c : E) ⦃s : set α⦄, μ s < P (s.indicator (λ (_x : α), c))) (h_add : ⦃f g : α E⦄, P f P g P (f + g)) (h_closed : is_closed {f : μ) | P f}) (h_ae : ⦃f g : α E⦄, f =ᵐ[μ] g P f P g) ⦃f : α E⦄ (hf : μ) :
P f

To prove something for an arbitrary `mem_ℒp` function in a second countable Borel normed group, it suffices to show that

• the property holds for (multiples of) characteristic functions;
• the set of functions in the `Lᵖ` space for which the property holds is closed.
• the property is closed under the almost-everywhere equal relation.

It is possible to make the hypotheses in the induction steps a bit stronger, and such conditions can be added once we need them (for example in `h_add` it is only necessary to consider the sum of a simple function with a multiple of a characteristic function and that the intersection of their images is a subset of `{0}`).

theorem measure_theory.mem_ℒp.induction_dense {α : Type u_1} {E : Type u_4} {p : ennreal} {μ : measure_theory.measure α} (hp_ne_top : p ) (P : E) Prop) (h0P : (c : E) ⦃s : set α⦄, μ s < {ε : ennreal}, ε 0 ( (g : α E), measure_theory.snorm (g - s.indicator (λ (x : α), c)) p μ ε P g)) (h1P : (f g : α E), P f P g P (f + g)) (h2P : (f : α E), ) {f : α E} (hf : μ) {ε : ennreal} (hε : ε 0) :
(g : α E), measure_theory.snorm (f - g) p μ ε P g

If a set of ae strongly measurable functions is stable under addition and approximates characteristic functions in `ℒp`, then it is dense in `ℒp`.

theorem measure_theory.L1.simple_func.to_Lp_one_eq_to_L1 {α : Type u_1} {E : Type u_4} {μ : measure_theory.measure α} (f : E) (hf : μ) :
@[protected]
theorem measure_theory.L1.simple_func.integrable {α : Type u_1} {E : Type u_4} {μ : measure_theory.measure α} (f : ) :
theorem measure_theory.integrable.induction {α : Type u_1} {E : Type u_4} {μ : measure_theory.measure α} (P : E) Prop) (h_ind : (c : E) ⦃s : set α⦄, μ s < P (s.indicator (λ (_x : α), c))) (h_add : ⦃f g : α E⦄, P f P g P (f + g)) (h_closed : is_closed {f : μ) | P f}) (h_ae : ⦃f g : α E⦄, f =ᵐ[μ] g P f P g) ⦃f : α E⦄ (hf : μ) :
P f

To prove something for an arbitrary integrable function in a normed group, it suffices to show that

• the property holds for (multiples of) characteristic functions;
• the set of functions in the `L¹` space for which the property holds is closed.
It is possible to make the hypotheses in the induction steps a bit stronger, and such conditions can be added once we need them (for example in `h_add` it is only necessary to consider the sum of a simple function with a multiple of a characteristic function and that the intersection of their images is a subset of `{0}`).