mathlib documentation

measure_theory.function.simple_func_dense

Density of simple functions #

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

Main definitions #

Main results #

Notations #

Pointwise approximation by simple functions #

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} [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.

Equations
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
@[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 : β) :
@[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 : ) :
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) :
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) :
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 : ) :
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 : ) :