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
x : αto the point
e kwhich is the nearest to
e 0, ...,
MeasureTheory.SimpleFunc.approxOn (f : β → α) (hf : Measurable f) (s : Set α) (y₀ : α) (h₀ : y₀ ∈ s) [SeparableSpace s] (n : ℕ) : β →ₛ α: a simple function that takes values in
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
α →ₛ β(local notation): the type of simple functions
α → β.
Pointwise approximation by simple functions #
nearestPtInd e N x is the index
k such that
e k is the nearest point to
x among the
e 0, ...,
e N. If more than one point are at the same distance from
nearestPtInd e N x returns the least of their indexes.
Approximate a measurable function by a sequence of simple functions
F n such that
F n x ∈ s.