mathlib documentation

measure_theory.simple_func_dense

Density of simple functions

Show that each Borel measurable function can be approximated, both pointwise and in norm, by a sequence of simple functions.

Main definitions

Notations

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

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
theorem measure_theory.simple_func.nearest_pt_ind_succ {α : Type u_1} [measurable_space α] [emetric_space α] [opens_measurable_space α] (e : → α) (N : ) (x : α) :
(measure_theory.simple_func.nearest_pt_ind e (N + 1)) x = ite (∀ (k : ), k Nedist (e (N + 1)) x < edist (e k) x) (N + 1) ((measure_theory.simple_func.nearest_pt_ind e N) x)

theorem measure_theory.simple_func.edist_nearest_pt_le {α : Type u_1} [measurable_space α] [emetric_space α] [opens_measurable_space α] (e : → α) (x : α) {k N : } :

def measure_theory.simple_func.approx_on {α : Type u_1} {β : Type u_2} [measurable_space α] [emetric_space α] [opens_measurable_space α] [measurable_space β] (f : β → α) (hf : measurable f) (s : set α) (y₀ : α) (h₀ : y₀ s) [topological_space.separable_space s] :

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 α] [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 α] [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 α] [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 α] [emetric_space α] [opens_measurable_space α] [measurable_space β] {f : β → α} (hf : measurable f) {s : set α} {y₀ : α} (h₀ : y₀ s) [topological_space.separable_space s] {x : β} :
f x closure sfilter.tendsto (λ (n : ), (measure_theory.simple_func.approx_on f hf s y₀ h₀ n) x) filter.at_top (𝓝 (f x))

theorem measure_theory.simple_func.edist_approx_on_le {α : Type u_1} {β : Type u_2} [measurable_space α] [emetric_space α] [opens_measurable_space α] [measurable_space β] {f : β → α} (hf : measurable f) {s : set α} {y₀ : α} (h₀ : y₀ s) [topological_space.separable_space s] (x : β) (n : ) :
edist ((measure_theory.simple_func.approx_on f hf s y₀ h₀ n) x) (f x) edist y₀ (f x)

theorem measure_theory.simple_func.edist_approx_on_y0_le {α : Type u_1} {β : Type u_2} [measurable_space α] [emetric_space α] [opens_measurable_space α] [measurable_space β] {f : β → α} (hf : measurable f) {s : set α} {y₀ : α} (h₀ : y₀ s) [topological_space.separable_space s] (x : β) (n : ) :
edist y₀ ((measure_theory.simple_func.approx_on f hf s y₀ h₀ n) x) edist y₀ (f x) + edist y₀ (f x)

theorem measure_theory.simple_func.norm_approx_on_zero_le {β : Type u_2} {E : Type u_4} [measurable_space β] [measurable_space E] [normed_group E] [opens_measurable_space E] {f : β → E} (hf : measurable f) {s : set E} (h₀ : 0 s) [topological_space.separable_space s] (x : β) (n : ) :

theorem measure_theory.simple_func.tendsto_approx_on_l1_edist {β : Type u_2} {E : Type u_4} [measurable_space β] [measurable_space E] [normed_group E] [opens_measurable_space E] {f : β → E} (hf : measurable f) {s : set E} {y₀ : E} (h₀ : y₀ s) [topological_space.separable_space s] {μ : measure_theory.measure β} :
(∀ᵐ (x : β) ∂μ, f x closure s)measure_theory.has_finite_integral (λ (x : β), f x - y₀) μfilter.tendsto (λ (n : ), ∫⁻ (x : β), edist ((measure_theory.simple_func.approx_on f hf s y₀ h₀ n) x) (f x) μ) filter.at_top (𝓝 0)

theorem measure_theory.simple_func.integrable_approx_on {β : Type u_2} {E : Type u_4} [measurable_space β] [measurable_space E] [normed_group E] [borel_space E] {f : β → E} {μ : measure_theory.measure β} (hf : measure_theory.integrable f μ) {s : set E} {y₀ : E} (h₀ : y₀ s) [topological_space.separable_space s] (hi₀ : measure_theory.integrable (λ (x : β), y₀) μ) (n : ) :