Density of simple functions
Show that each Borel measurable function can be approximated,
both pointwise and in L¹ norm, 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. Iff x ∈ s, thenmeasure_theory.simple_func.approx_on f hf s y₀ h₀ n xtends tof xasntends to∞. Ifαis anormed_group,f x - y₀ismeasure_theory.integrable, andf x ∈ sfor a.e.x, thensimple_func.approx_on f hf s y₀ h₀ ntends tofinL₁. The main use case iss = univ,y₀ = 0.
Notations
α →ₛ β(local notation): the type of simple functionsα → β.
def
measure_theory.simple_func.nearest_pt_ind
{α : Type u_1}
[measurable_space α]
[emetric_space α]
[opens_measurable_space α]
(e : ℕ → α)
(a : ℕ) :
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 : α | edist (e (N + 1)) x < 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
def
measure_theory.simple_func.nearest_pt
{α : Type u_1}
[measurable_space α]
[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 α]
[emetric_space α]
[opens_measurable_space α]
(e : ℕ → α) :
@[simp]
theorem
measure_theory.simple_func.nearest_pt_zero
{α : Type u_1}
[measurable_space α]
[emetric_space α]
[opens_measurable_space α]
(e : ℕ → α) :
theorem
measure_theory.simple_func.nearest_pt_ind_succ
{α : Type u_1}
[measurable_space α]
[emetric_space α]
[opens_measurable_space α]
(e : ℕ → α)
(N : ℕ)
(x : α) :
theorem
measure_theory.simple_func.nearest_pt_ind_le
{α : Type u_1}
[measurable_space α]
[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 α]
[emetric_space α]
[opens_measurable_space α]
(e : ℕ → α)
(x : α)
{k N : ℕ}
(hk : k ≤ N) :
edist (⇑(measure_theory.simple_func.nearest_pt e N) x) x ≤ edist (e k) x
theorem
measure_theory.simple_func.tendsto_nearest_pt
{α : Type u_1}
[measurable_space α]
[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 (𝓝 x)
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]
(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 α]
[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 : β) :
⇑(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 α]
[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 α]
[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 (𝓝 (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 : ℕ) :
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 β}
(hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure s)
(hi : 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 : ℕ) :
measure_theory.integrable ⇑(measure_theory.simple_func.approx_on f _ s y₀ h₀ n) μ
theorem
measure_theory.simple_func.tendsto_approx_on_univ_l1_edist
{β : Type u_2}
{E : Type u_4}
[measurable_space β]
[measurable_space E]
[normed_group E]
[opens_measurable_space E]
[topological_space.second_countable_topology E]
{f : β → E}
{μ : measure_theory.measure β}
(hf : measure_theory.integrable f μ) :
filter.tendsto (λ (n : ℕ), ∫⁻ (x : β), edist (⇑(measure_theory.simple_func.approx_on f _ set.univ 0 trivial n) x) (f x) ∂μ) filter.at_top (𝓝 0)
theorem
measure_theory.simple_func.integrable_approx_on_univ
{β : Type u_2}
{E : Type u_4}
[measurable_space β]
[measurable_space E]
[normed_group E]
[borel_space E]
[topological_space.second_countable_topology E]
{f : β → E}
{μ : measure_theory.measure β}
(hf : measure_theory.integrable f μ)
(n : ℕ) :
theorem
measure_theory.simple_func.tendsto_approx_on_univ_l1
{β : Type u_2}
{E : Type u_4}
[measurable_space β]
[measurable_space E]
[normed_group E]
[borel_space E]
[topological_space.second_countable_topology E]
{f : β → E}
{μ : measure_theory.measure β}
(hf : measure_theory.integrable f μ) :
filter.tendsto (λ (n : ℕ), measure_theory.l1.of_fun ⇑(measure_theory.simple_func.approx_on f _ set.univ 0 trivial n) _) filter.at_top (𝓝 (measure_theory.l1.of_fun f hf))