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.
theorem
measure_theory.simple_func_sequence_tendsto
{α : Type u}
{β : Type v}
[measurable_space α]
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
{f : α → β} :
measurable f → (∃ (F : ℕ → measure_theory.simple_func α β), ∀ (x : α), filter.tendsto (λ (n : ℕ), ⇑(F n) x) filter.at_top (nhds (f x)) ∧ ∀ (n : ℕ), ∥⇑(F n) x∥ ≤ ∥f x∥ + ∥f x∥)
theorem
measure_theory.simple_func_sequence_tendsto'
{α : Type u}
{β : Type v}
[measurable_space α]
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
{μ : measure_theory.measure α}
{f : α → β} :
measurable f → measure_theory.integrable f μ → (∃ (F : ℕ → measure_theory.simple_func α β), (∀ (n : ℕ), measure_theory.integrable ⇑(F n) μ) ∧ filter.tendsto (λ (n : ℕ), ∫⁻ (x : α), ↑(nndist (⇑(F n) x) (f x)) ∂μ) filter.at_top (nhds 0))