# mathlibdocumentation

measure_theory.function.simple_func_dense

# 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 #

noncomputable def measure_theory.simple_func.nearest_pt_ind {α : Type u_1} (e : → α) :

nearest_pt_ind e N x is the index k such that e k is the nearest point to x among the points e 0, ..., e N. If more than one point are at the same distance from x, then nearest_pt_ind e N x returns the least of their indexes.

Equations
noncomputable def measure_theory.simple_func.nearest_pt {α : Type u_1} (e : → α) (N : ) :

nearest_pt e N x is the nearest point to x among the points e 0, ..., e N. If more than one point are at the same distance from x, then nearest_pt e N x returns the point with the least possible index.

Equations
@[simp]
theorem measure_theory.simple_func.nearest_pt_ind_zero {α : Type u_1} (e : → α) :
@[simp]
theorem measure_theory.simple_func.nearest_pt_zero {α : Type u_1} (e : → α) :
theorem measure_theory.simple_func.nearest_pt_ind_succ {α : Type u_1} (e : → α) (N : ) (x : α) :
x = ite (∀ (k : ), k Nedist (e (N + 1)) x < edist (e k) x) (N + 1)
theorem measure_theory.simple_func.nearest_pt_ind_le {α : Type u_1} (e : → α) (N : ) (x : α) :
theorem measure_theory.simple_func.edist_nearest_pt_le {α : Type u_1} (e : → α) (x : α) {k N : } (hk : k N) :
x edist (e k) x
theorem measure_theory.simple_func.tendsto_nearest_pt {α : Type u_1} {e : → α} {x : α} (hx : x closure (set.range e)) :
noncomputable def measure_theory.simple_func.approx_on {α : Type u_1} {β : Type u_2} (f : β → α) (hf : measurable f) (s : set α) (y₀ : α) (h₀ : y₀ s) (n : ) :

Approximate a measurable function by a sequence of simple functions F n such that F n x ∈ s.

Equations
@[simp]
theorem measure_theory.simple_func.approx_on_zero {α : Type u_1} {β : Type u_2} {f : β → α} (hf : measurable f) {s : set α} {y₀ : α} (h₀ : y₀ s) (x : β) :
y₀ h₀ 0) x = y₀
theorem measure_theory.simple_func.approx_on_mem {α : Type u_1} {β : Type u_2} {f : β → α} (hf : measurable f) {s : set α} {y₀ : α} (h₀ : y₀ s) (n : ) (x : β) :
y₀ h₀ n) x s
@[simp]
theorem measure_theory.simple_func.approx_on_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : β → α} (hf : measurable f) {g : γ → β} (hg : measurable g) {s : set α} {y₀ : α} (h₀ : y₀ s) (n : ) :
s y₀ h₀ n = y₀ h₀ n).comp g hg
theorem measure_theory.simple_func.tendsto_approx_on {α : Type u_1} {β : Type u_2} {f : β → α} (hf : measurable f) {s : set α} {y₀ : α} (h₀ : y₀ s) {x : β} (hx : f x ) :
filter.tendsto (λ (n : ), y₀ h₀ n) x) filter.at_top (𝓝 (f x))
theorem measure_theory.simple_func.edist_approx_on_mono {α : Type u_1} {β : Type u_2} {f : β → α} (hf : measurable f) {s : set α} {y₀ : α} (h₀ : y₀ s) (x : β) {m n : } (h : m n) :
edist ( y₀ h₀ n) x) (f x) edist ( y₀ h₀ m) x) (f x)
theorem measure_theory.simple_func.edist_approx_on_le {α : Type u_1} {β : Type u_2} {f : β → α} (hf : measurable f) {s : set α} {y₀ : α} (h₀ : y₀ s) (x : β) (n : ) :
edist ( y₀ h₀ n) x) (f x) edist y₀ (f x)
theorem measure_theory.simple_func.edist_approx_on_y0_le {α : Type u_1} {β : Type u_2} {f : β → α} (hf : measurable f) {s : set α} {y₀ : α} (h₀ : y₀ s) (x : β) (n : ) :
edist y₀ ( y₀ h₀ n) x) edist y₀ (f x) + edist y₀ (f x)

### Lp approximation by simple functions #

theorem measure_theory.simple_func.nnnorm_approx_on_le {β : Type u_2} {E : Type u_4} [normed_group E] {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} [normed_group E] {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} [normed_group E] {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} [normed_group E] {p : ℝ≥0∞} {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 (𝓝 0)
theorem measure_theory.simple_func.mem_ℒp_approx_on {β : Type u_2} {E : Type u_4} [normed_group E] {p : ℝ≥0∞} [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_univ_Lp_snorm {β : Type u_2} {E : Type u_4} [normed_group E] {p : ℝ≥0∞} {f : β → E} (hp_ne_top : p ) {μ : measure_theory.measure β} (fmeas : measurable f) (hf : μ < ) :
theorem measure_theory.simple_func.mem_ℒp_approx_on_univ {β : Type u_2} {E : Type u_4} [normed_group E] {p : ℝ≥0∞} [borel_space E] {f : β → E} {μ : measure_theory.measure β} (fmeas : measurable f) (hf : μ) (n : ) :
μ
theorem measure_theory.simple_func.tendsto_approx_on_univ_Lp {β : Type u_2} {E : Type u_4} [normed_group E] {p : ℝ≥0∞} [borel_space E] {f : β → E} [hp : fact (1 p)] (hp_ne_top : p ) {μ : measure_theory.measure β} (fmeas : measurable f) (hf : μ) :

### L1 approximation by simple functions #

theorem measure_theory.simple_func.tendsto_approx_on_L1_nnnorm {β : Type u_2} {E : Type u_4} [normed_group E] {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 (𝓝 0)
theorem measure_theory.simple_func.integrable_approx_on {β : Type u_2} {E : Type u_4} [normed_group E] [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_univ_L1_nnnorm {β : Type u_2} {E : Type u_4} [normed_group E] {f : β → E} {μ : measure_theory.measure β} (fmeas : measurable f) (hf : μ) :
filter.tendsto (λ (n : ), ∫⁻ (x : β), n) x - f x∥₊ μ) filter.at_top (𝓝 0)
theorem measure_theory.simple_func.integrable_approx_on_univ {β : Type u_2} {E : Type u_4} [normed_group E] [borel_space E] {f : β → E} {μ : measure_theory.measure β} (fmeas : measurable f) (hf : μ) (n : ) :

### 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} [normed_group F] (f : F) :
∃ (C : ), ∀ (x : α), f x C
theorem measure_theory.simple_func.mem_ℒp_zero {α : Type u_1} {E : Type u_4} [normed_group E] (f : E) (μ : measure_theory.measure α) :
theorem measure_theory.simple_func.mem_ℒp_top {α : Type u_1} {E : Type u_4} [normed_group E] (f : E) (μ : measure_theory.measure α) :
@[protected]
theorem measure_theory.simple_func.snorm'_eq {α : Type u_1} {F : Type u_5} [normed_group F] {p : } (f : F) (μ : measure_theory.measure α) :
= (∑ (y : F) in f.range, (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} [normed_group E] {μ : measure_theory.measure α} {p : ℝ≥0∞} (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} [normed_group E] {μ : measure_theory.measure α} (p : ℝ≥0∞) {f : E} (hf : ∀ (y : E), y 0μ (f ⁻¹' {y}) < ) :
theorem measure_theory.simple_func.mem_ℒp_iff {α : Type u_1} {E : Type u_4} [normed_group E] {μ : measure_theory.measure α} {p : ℝ≥0∞} {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} [normed_group E] {μ : 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} [normed_group E] {μ : measure_theory.measure α} {p : ℝ≥0∞} {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} [normed_group E] {μ : measure_theory.measure α} {p : ℝ≥0∞} {f : E} (hp_pos : p 0) (hp_ne_top : p ) :
theorem measure_theory.simple_func.integrable_iff_fin_meas_supp {α : Type u_1} {E : Type u_4} [normed_group E] {μ : measure_theory.measure α} {f : E} :
theorem measure_theory.simple_func.fin_meas_supp.integrable {α : Type u_1} {E : Type u_4} [normed_group E] {μ : 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} [normed_group E] [normed_group F] {μ : measure_theory.measure α} {f : E} {g : F} :
μ
theorem measure_theory.simple_func.mem_ℒp_of_is_finite_measure {α : Type u_1} {E : Type u_4} [normed_group E] (f : E) (p : ℝ≥0∞) (μ : measure_theory.measure α)  :
theorem measure_theory.simple_func.integrable_of_is_finite_measure {α : Type u_1} {E : Type u_4} [normed_group E] {μ : measure_theory.measure α} (f : E) :
theorem measure_theory.simple_func.measure_preimage_lt_top_of_integrable {α : Type u_1} {E : Type u_4} [normed_group E] {μ : 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} [normed_group E] {μ : measure_theory.measure α} {p : ℝ≥0∞} (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} [normed_group E] {μ : 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} [normed_group E] {μ : measure_theory.measure α} {p : ℝ≥0∞} (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) [normed_group E] [borel_space E] (p : ℝ≥0∞) (μ : measure_theory.measure α) :

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

Equations

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} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : measure_theory.measure α} (f : ) :
@[protected]
theorem measure_theory.Lp.simple_func.eq' {α : Type u_1} {E : Type u_4} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : measure_theory.measure α} {f g : } :
f = gf = 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_scalar {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_field 𝕜] [ E]  :

If E is a normed space, Lp.simple_func E p μ is a has_scalar. 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} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_field 𝕜] [ 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} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_field 𝕜] [ 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]
noncomputable def measure_theory.Lp.simple_func.normed_space {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : measure_theory.measure α} [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
def measure_theory.Lp.simple_func.to_Lp {α : Type u_1} {E : Type u_4} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : 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} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : measure_theory.measure α} (f : E) (hf : μ) :
theorem measure_theory.Lp.simple_func.to_Lp_eq_mk {α : Type u_1} {E : Type u_4} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : measure_theory.measure α} (f : E) (hf : μ) :
theorem measure_theory.Lp.simple_func.to_Lp_zero {α : Type u_1} {E : Type u_4} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : measure_theory.measure α} :
theorem measure_theory.Lp.simple_func.to_Lp_add {α : Type u_1} {E : Type u_4} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : measure_theory.measure α} (f g : E) (hf : μ) (hg : μ) :
theorem measure_theory.Lp.simple_func.to_Lp_neg {α : Type u_1} {E : Type u_4} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : measure_theory.measure α} (f : E) (hf : μ) :
theorem measure_theory.Lp.simple_func.to_Lp_sub {α : Type u_1} {E : Type u_4} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : 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} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_field 𝕜] [ E] (f : E) (hf : μ) (c : 𝕜) :
theorem measure_theory.Lp.simple_func.norm_to_Lp {α : Type u_1} {E : Type u_4} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : 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} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : measure_theory.measure α} (f : ) :

Find a representative of a Lp.simple_func.

Equations
@[protected]
theorem measure_theory.Lp.simple_func.measurable {α : Type u_1} {E : Type u_4} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : measure_theory.measure α} (f : ) :

(to_simple_func f) is measurable.

@[protected]
theorem measure_theory.Lp.simple_func.ae_measurable {α : Type u_1} {E : Type u_4} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : measure_theory.measure α} (f : ) :
theorem measure_theory.Lp.simple_func.to_simple_func_eq_to_fun {α : Type u_1} {E : Type u_4} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : measure_theory.measure α} (f : ) :
@[protected]
theorem measure_theory.Lp.simple_func.mem_ℒp {α : Type u_1} {E : Type u_4} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : measure_theory.measure α} (f : ) :

to_simple_func f satisfies the predicate mem_ℒp.

theorem measure_theory.Lp.simple_func.to_Lp_to_simple_func {α : Type u_1} {E : Type u_4} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : measure_theory.measure α} (f : ) :
theorem measure_theory.Lp.simple_func.to_simple_func_to_Lp {α : Type u_1} {E : Type u_4} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : measure_theory.measure α} (f : E) (hfi : μ) :
theorem measure_theory.Lp.simple_func.add_to_simple_func {α : Type u_1} {E : Type u_4} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : measure_theory.measure α} (f g : ) :
theorem measure_theory.Lp.simple_func.neg_to_simple_func {α : Type u_1} {E : Type u_4} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : measure_theory.measure α} (f : ) :
theorem measure_theory.Lp.simple_func.sub_to_simple_func {α : Type u_1} {E : Type u_4} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : 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} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : measure_theory.measure α} [normed_field 𝕜] [ E] (k : 𝕜) (f : ) :
theorem measure_theory.Lp.simple_func.norm_to_simple_func {α : Type u_1} {E : Type u_4} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : measure_theory.measure α} [fact (1 p)] (f : ) :
noncomputable def measure_theory.Lp.simple_func.indicator_const {α : Type u_1} {E : Type u_4} [normed_group E] [borel_space E] (p : ℝ≥0∞) {μ : 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} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : 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} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : 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} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : 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} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : measure_theory.measure α} [fact (1 p)] :
@[protected]
theorem measure_theory.Lp.simple_func.uniform_embedding {α : Type u_1} {E : Type u_4} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : measure_theory.measure α} [fact (1 p)] :
@[protected]
theorem measure_theory.Lp.simple_func.uniform_inducing {α : Type u_1} {E : Type u_4} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : measure_theory.measure α} [fact (1 p)] :
@[protected]
theorem measure_theory.Lp.simple_func.dense_embedding {α : Type u_1} {E : Type u_4} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : 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} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : 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} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : measure_theory.measure α} [fact (1 p)] (hp_ne_top : p ) :
noncomputable def measure_theory.Lp.simple_func.coe_to_Lp (α : Type u_1) (E : Type u_4) (𝕜 : Type u_6) [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : measure_theory.measure α} [fact (1 p)] [normed_field 𝕜] [ 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 : ℝ≥0∞} {μ : measure_theory.measure α} {G : Type u_7} [borel_space G] (f g : ) :
@[protected, instance]
theorem measure_theory.Lp.simple_func.coe_fn_zero {α : Type u_1} (p : ℝ≥0∞) (μ : measure_theory.measure α) (G : Type u_7) [borel_space G]  :
0 =ᵐ[μ] 0
theorem measure_theory.Lp.simple_func.coe_fn_nonneg {α : Type u_1} {p : ℝ≥0∞} {μ : measure_theory.measure α} {G : Type u_7} [borel_space G] (f : ) :
0 ≤ᵐ[μ] f 0 f
theorem measure_theory.Lp.simple_func.exists_simple_func_nonneg_ae_eq {α : Type u_1} {p : ℝ≥0∞} {μ : measure_theory.measure α} {G : Type u_7} [borel_space G] {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 : ℝ≥0∞) (μ : measure_theory.measure α) (G : Type u_7) [borel_space G]  :
{g // 0 g}{g // 0 g}

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

Equations
theorem measure_theory.Lp.simple_func.dense_range_coe_simple_func_nonneg_to_Lp_nonneg {α : Type u_1} (p : ℝ≥0∞) (μ : measure_theory.measure α) (G : Type u_7) [borel_space G] [hp : fact (1 p)] (hp_ne_top : p ) :
theorem measure_theory.Lp.induction {α : Type u_1} {E : Type u_4} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : 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} [normed_group E] [borel_space E] {p : ℝ≥0∞} {μ : 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 fP gP (f + g)) (h_closed : is_closed {f : μ) | P f}) (h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] gP fP 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.L1.simple_func.to_Lp_one_eq_to_L1 {α : Type u_1} {E : Type u_4} [normed_group E] [borel_space E] {μ : measure_theory.measure α} (f : E) (hf : μ) :
@[protected]
theorem measure_theory.L1.simple_func.integrable {α : Type u_1} {E : Type u_4} [normed_group E] [borel_space E] {μ : measure_theory.measure α} (f : ) :
theorem measure_theory.integrable.induction {α : Type u_1} {E : Type u_4} [normed_group E] [borel_space E] {μ : measure_theory.measure α} (P : (α → E) → Prop) (h_ind : ∀ (c : E) ⦃s : set α⦄, μ s < P (s.indicator (λ (_x : α), c))) (h_add : ∀ ⦃f g : α → E⦄, P fP gP (f + g)) (h_closed : is_closed {f : μ) | P f}) (h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] gP fP g) ⦃f : α → E⦄ (hf : μ) :
P f

To prove something for an arbitrary integrable 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.
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}).