# mathlib3documentation

measure_theory.function.simple_func_dense

# Density of simple functions #

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

Show that each Borel measurable function can be approximated pointwise 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.

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

## Notations #

• α →ₛ β (local notation): the type of 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]
@[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 N has_edist.edist (e (N + 1)) x < has_edist.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) :
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 (nhds (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) :
has_edist.edist ( y₀ h₀ n) x) (f x) has_edist.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 : ) :
has_edist.edist ( y₀ h₀ n) x) (f x) (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 : ) :
( y₀ h₀ n) x) (f x) + (f x)