# mathlibdocumentation

measure_theory.simple_func_dense

# Density of simple functions #

Show that each Borel measurable function can be approximated, both pointwise and 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. If f x ∈ s, then measure_theory.simple_func.approx_on f hf s y₀ h₀ n x tends to f x as n tends to ∞. If α is a normed_group, f x - y₀ is measure_theory.integrable, and f x ∈ s for a.e. x, then simple_func.approx_on f hf s y₀ h₀ n tends to f in L₁. The main use case is s = univ, y₀ = 0.

## Notations #

• α →ₛ β (local notation): the type of simple functions α → β.
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
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)) :
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_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)
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_L1_edist {β : 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 : β), edist ( 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_edist {β : Type u_2} {E : Type u_4} [normed_group E] {f : β → E} {μ : measure_theory.measure β} (fmeas : measurable f) (hf : μ) :
filter.tendsto (λ (n : ), ∫⁻ (x : β), edist ( 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 : ) :
theorem measure_theory.simple_func.tendsto_approx_on_univ_L1 {β : Type u_2} {E : Type u_4} [normed_group E] [borel_space E] {f : β → E} {μ : measure_theory.measure β} (fmeas : measurable f) (hf : μ) :