# Documentation

Mathlib.MeasureTheory.Function.SimpleFuncDense

# Density of simple functions #

Show that each Borel measurable function can be approximated pointwise by a sequence of simple functions.

## Main definitions #

• MeasureTheory.SimpleFunc.nearestPt (e : ℕ → α) (N : ℕ) : α →ₛ ℕ: the SimpleFunc sending each x : α to the point e k which is the nearest to x among e 0, ..., e N.
• MeasureTheory.SimpleFunc.approxOn (f : β → α) (hf : Measurable f) (s : Set α) (y₀ : α) (h₀ : y₀ ∈ s) [SeparableSpace s] (n : ℕ) : β →ₛ α : a simple function that takes values in s and approximates f.

## Main results #

• tendsto_approxOn (pointwise convergence): If f x ∈ s, then the sequence of simple approximations MeasureTheory.SimpleFunc.approxOn 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 MeasureTheory.SimpleFunc.nearestPtInd {α : Type u_1} [] (e : α) :

nearestPtInd 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 nearestPtInd e N x returns the least of their indexes.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def MeasureTheory.SimpleFunc.nearestPt {α : Type u_1} [] (e : α) (N : ) :

nearestPt 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 nearestPt e N x returns the point with the least possible index.

Instances For
@[simp]
theorem MeasureTheory.SimpleFunc.nearestPtInd_zero {α : Type u_1} [] (e : α) :
@[simp]
theorem MeasureTheory.SimpleFunc.nearestPt_zero {α : Type u_1} [] (e : α) :
theorem MeasureTheory.SimpleFunc.nearestPtInd_succ {α : Type u_1} [] (e : α) (N : ) (x : α) :
↑() x = if ∀ (k : ), k Nedist (e (N + 1)) x < edist (e k) x then N + 1 else
theorem MeasureTheory.SimpleFunc.nearestPtInd_le {α : Type u_1} [] (e : α) (N : ) (x : α) :
N
theorem MeasureTheory.SimpleFunc.edist_nearestPt_le {α : Type u_1} [] (e : α) (x : α) {k : } {N : } (hk : k N) :
edist () x edist (e k) x
theorem MeasureTheory.SimpleFunc.tendsto_nearestPt {α : Type u_1} [] {e : α} {x : α} (hx : x closure ()) :
Filter.Tendsto (fun N => ) Filter.atTop (nhds x)
noncomputable def MeasureTheory.SimpleFunc.approxOn {α : Type u_1} {β : Type u_2} [] [] (f : βα) (hf : ) (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.

Instances For
@[simp]
theorem MeasureTheory.SimpleFunc.approxOn_zero {α : Type u_1} {β : Type u_2} [] [] {f : βα} (hf : ) {s : Set α} {y₀ : α} (h₀ : y₀ s) (x : β) :
↑(MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ 0) x = y₀
theorem MeasureTheory.SimpleFunc.approxOn_mem {α : Type u_1} {β : Type u_2} [] [] {f : βα} (hf : ) {s : Set α} {y₀ : α} (h₀ : y₀ s) (n : ) (x : β) :
↑(MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) x s
@[simp]
theorem MeasureTheory.SimpleFunc.approxOn_comp {α : Type u_1} {β : Type u_2} [] [] {γ : Type u_7} [] {f : βα} (hf : ) {g : γβ} (hg : ) {s : Set α} {y₀ : α} (h₀ : y₀ s) (n : ) :
theorem MeasureTheory.SimpleFunc.tendsto_approxOn {α : Type u_1} {β : Type u_2} [] [] {f : βα} (hf : ) {s : Set α} {y₀ : α} (h₀ : y₀ s) {x : β} (hx : f x ) :
Filter.Tendsto (fun n => ↑(MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) x) Filter.atTop (nhds (f x))
theorem MeasureTheory.SimpleFunc.edist_approxOn_mono {α : Type u_1} {β : Type u_2} [] [] {f : βα} (hf : ) {s : Set α} {y₀ : α} (h₀ : y₀ s) (x : β) {m : } {n : } (h : m n) :
edist (↑(MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) x) (f x) edist (↑(MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ m) x) (f x)
theorem MeasureTheory.SimpleFunc.edist_approxOn_le {α : Type u_1} {β : Type u_2} [] [] {f : βα} (hf : ) {s : Set α} {y₀ : α} (h₀ : y₀ s) (x : β) (n : ) :
edist (↑(MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) x) (f x) edist y₀ (f x)
theorem MeasureTheory.SimpleFunc.edist_approxOn_y0_le {α : Type u_1} {β : Type u_2} [] [] {f : βα} (hf : ) {s : Set α} {y₀ : α} (h₀ : y₀ s) (x : β) (n : ) :
edist y₀ (↑(MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) x) edist y₀ (f x) + edist y₀ (f x)