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 : ℕ) : α →ₛ ℕ: thesimple_funcsending eachx : αto the pointe kwhich is the nearest toxamonge 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 insand approximatesf.
Main results #
tendsto_approx_on(pointwise convergence): Iff x ∈ s, then the sequence of simple approximationsmeasure_theory.simple_func.approx_on f hf s y₀ h₀ n, evaluated atx, tends tof xasntends 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}
[measurable_space α]
[pseudo_emetric_space α]
[opens_measurable_space α]
(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
- measure_theory.simple_func.nearest_pt_ind e (N + 1) = measure_theory.simple_func.piecewise (⋂ (k : ℕ) (H : k ≤ N), {x : α | has_edist.edist (e (N + 1)) x < has_edist.edist (e k) x}) _ (measure_theory.simple_func.const α (N + 1)) (measure_theory.simple_func.nearest_pt_ind e N)
- measure_theory.simple_func.nearest_pt_ind e 0 = measure_theory.simple_func.const α 0
noncomputable
def
measure_theory.simple_func.nearest_pt
{α : Type u_1}
[measurable_space α]
[pseudo_emetric_space α]
[opens_measurable_space α]
(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.
@[simp]
theorem
measure_theory.simple_func.nearest_pt_ind_zero
{α : Type u_1}
[measurable_space α]
[pseudo_emetric_space α]
[opens_measurable_space α]
(e : ℕ → α) :
@[simp]
theorem
measure_theory.simple_func.nearest_pt_zero
{α : Type u_1}
[measurable_space α]
[pseudo_emetric_space α]
[opens_measurable_space α]
(e : ℕ → α) :
theorem
measure_theory.simple_func.nearest_pt_ind_succ
{α : Type u_1}
[measurable_space α]
[pseudo_emetric_space α]
[opens_measurable_space α]
(e : ℕ → α)
(N : ℕ)
(x : α) :
⇑(measure_theory.simple_func.nearest_pt_ind e (N + 1)) x = ite (∀ (k : ℕ), k ≤ N → has_edist.edist (e (N + 1)) x < has_edist.edist (e k) x) (N + 1) (⇑(measure_theory.simple_func.nearest_pt_ind e N) x)
theorem
measure_theory.simple_func.nearest_pt_ind_le
{α : Type u_1}
[measurable_space α]
[pseudo_emetric_space α]
[opens_measurable_space α]
(e : ℕ → α)
(N : ℕ)
(x : α) :
⇑(measure_theory.simple_func.nearest_pt_ind e N) x ≤ N
theorem
measure_theory.simple_func.edist_nearest_pt_le
{α : Type u_1}
[measurable_space α]
[pseudo_emetric_space α]
[opens_measurable_space α]
(e : ℕ → α)
(x : α)
{k N : ℕ}
(hk : k ≤ N) :
has_edist.edist (⇑(measure_theory.simple_func.nearest_pt e N) x) x ≤ has_edist.edist (e k) x
theorem
measure_theory.simple_func.tendsto_nearest_pt
{α : Type u_1}
[measurable_space α]
[pseudo_emetric_space α]
[opens_measurable_space α]
{e : ℕ → α}
{x : α}
(hx : x ∈ closure (set.range e)) :
filter.tendsto (λ (N : ℕ), ⇑(measure_theory.simple_func.nearest_pt e N) x) filter.at_top (nhds x)
noncomputable
def
measure_theory.simple_func.approx_on
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[pseudo_emetric_space α]
[opens_measurable_space α]
[measurable_space β]
(f : β → α)
(hf : measurable f)
(s : set α)
(y₀ : α)
(h₀ : y₀ ∈ s)
[topological_space.separable_space ↥s]
(n : ℕ) :
Approximate a measurable function by a sequence of simple functions F n such that
F n x ∈ s.
Equations
- measure_theory.simple_func.approx_on f hf s y₀ h₀ n = (measure_theory.simple_func.nearest_pt (λ (k : ℕ), k.cases_on y₀ (coe ∘ topological_space.dense_seq ↥s)) n).comp f hf
@[simp]
theorem
measure_theory.simple_func.approx_on_zero
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[pseudo_emetric_space α]
[opens_measurable_space α]
[measurable_space β]
{f : β → α}
(hf : measurable f)
{s : set α}
{y₀ : α}
(h₀ : y₀ ∈ s)
[topological_space.separable_space ↥s]
(x : β) :
⇑(measure_theory.simple_func.approx_on f hf s y₀ h₀ 0) x = y₀
theorem
measure_theory.simple_func.approx_on_mem
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[pseudo_emetric_space α]
[opens_measurable_space α]
[measurable_space β]
{f : β → α}
(hf : measurable f)
{s : set α}
{y₀ : α}
(h₀ : y₀ ∈ s)
[topological_space.separable_space ↥s]
(n : ℕ)
(x : β) :
⇑(measure_theory.simple_func.approx_on f hf s y₀ h₀ n) x ∈ s
@[simp]
theorem
measure_theory.simple_func.approx_on_comp
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[pseudo_emetric_space α]
[opens_measurable_space α]
[measurable_space β]
{γ : Type u_3}
[measurable_space γ]
{f : β → α}
(hf : measurable f)
{g : γ → β}
(hg : measurable g)
{s : set α}
{y₀ : α}
(h₀ : y₀ ∈ s)
[topological_space.separable_space ↥s]
(n : ℕ) :
measure_theory.simple_func.approx_on (f ∘ g) _ s y₀ h₀ n = (measure_theory.simple_func.approx_on f hf s y₀ h₀ n).comp g hg
theorem
measure_theory.simple_func.tendsto_approx_on
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[pseudo_emetric_space α]
[opens_measurable_space α]
[measurable_space β]
{f : β → α}
(hf : measurable f)
{s : set α}
{y₀ : α}
(h₀ : y₀ ∈ s)
[topological_space.separable_space ↥s]
{x : β}
(hx : f x ∈ closure s) :
filter.tendsto (λ (n : ℕ), ⇑(measure_theory.simple_func.approx_on f hf s 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}
[measurable_space α]
[pseudo_emetric_space α]
[opens_measurable_space α]
[measurable_space β]
{f : β → α}
(hf : measurable f)
{s : set α}
{y₀ : α}
(h₀ : y₀ ∈ s)
[topological_space.separable_space ↥s]
(x : β)
{m n : ℕ}
(h : m ≤ n) :
has_edist.edist (⇑(measure_theory.simple_func.approx_on f hf s y₀ h₀ n) x) (f x) ≤ has_edist.edist (⇑(measure_theory.simple_func.approx_on f hf s y₀ h₀ m) x) (f x)
theorem
measure_theory.simple_func.edist_approx_on_le
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[pseudo_emetric_space α]
[opens_measurable_space α]
[measurable_space β]
{f : β → α}
(hf : measurable f)
{s : set α}
{y₀ : α}
(h₀ : y₀ ∈ s)
[topological_space.separable_space ↥s]
(x : β)
(n : ℕ) :
has_edist.edist (⇑(measure_theory.simple_func.approx_on f hf s y₀ h₀ n) x) (f x) ≤ has_edist.edist y₀ (f x)
theorem
measure_theory.simple_func.edist_approx_on_y0_le
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[pseudo_emetric_space α]
[opens_measurable_space α]
[measurable_space β]
{f : β → α}
(hf : measurable f)
{s : set α}
{y₀ : α}
(h₀ : y₀ ∈ s)
[topological_space.separable_space ↥s]
(x : β)
(n : ℕ) :
has_edist.edist y₀ (⇑(measure_theory.simple_func.approx_on f hf s y₀ h₀ n) x) ≤ has_edist.edist y₀ (f x) + has_edist.edist y₀ (f x)