Theorems · Theorem · measure theory

MeasureTheory.Integrable.exists_hasCompactSupport_integral_sub_le

∀ {α : Type u_1} [inst : TopologicalSpace α] [NormalSpace α] [inst_2 : MeasurableSpace α] [BorelSpace α] {E : Type u_2}
  [inst_4 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α} [NormedSpace ℝ E] [R1Space α]
  [WeaklyLocallyCompactSpace α] [μ.Regular] {f : α → E},
  MeasureTheory.Integrable f μ →
    ∀ {ε : ℝ},
      0 < ε → ∃ g, HasCompactSupport g ∧ ∫ (x : α), ‖f x - g x‖ ∂μ ≤ ε ∧ Continuous g ∧ MeasureTheory.Integrable g μ

In a locally compact space, any integrable function can be approximated by compactly supported continuous functions, version in terms of ∫.

Defined in

Mathlib.MeasureTheory.Function.ContinuousMapDense

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceNormalSpaceMeasurableSpaceBorelSpaceNormedAddCommGroupNormedSpaceR1SpaceWeaklyLocallyCompactSpaceMeasureTheory.Measure.Regular