Theorems · Theorem · measure theory

MeasureTheory.Integrable.exists_boundedContinuous_lintegral_sub_le

∀ {α : Type u_1} [inst : TopologicalSpace α] [NormalSpace α] [inst_2 : MeasurableSpace α] [BorelSpace α] {E : Type u_2}
  [inst_4 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α} [NormedSpace ℝ E] [μ.WeaklyRegular] {f : α → E},
  MeasureTheory.Integrable f μ →
    ∀ {ε : ENNReal}, ε ≠ 0 → ∃ g, ∫⁻ (x : α), ‖f x - g x‖ₑ ∂μ ≤ ε ∧ MeasureTheory.Integrable (⇑g) μ

Any integrable function can be approximated by bounded continuous functions, version in terms of ∫⁻.

Defined in

Mathlib.MeasureTheory.Function.ContinuousMapDense

Cited by

0 results in Mathlib

Foundations

Depth 224 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceNormalSpaceMeasurableSpaceBorelSpaceNormedAddCommGroupNormedSpaceMeasureTheory.Measure.WeaklyRegular