English
In a locally compact space, every integrable function can be approximated in the lintegral norm by a function with compact support that is continuous and integrable; i.e., there exists a g with compact support such that ∫⁻ ‖f−g‖ ≤ ε and g is integrable and continuous.
Русский
В локально компактном пространстве любая интегрируемая функция может быть аппроксимирована функцией с компактной опорой, непрерывной и интегрируемой, в линегральной норме.
LaTeX
$$MeasureTheory.Integrable exists_hasCompactSupport_lintegral_sub_le: ∃ g, HasCompactSupport g ∧ ∫⁻ x, ‖f x − g x‖ₑ ∂μ ≤ ε ∧ Continuous g ∧ Integrable g μ$$
Lean4
/-- In a locally compact space, any integrable function can be approximated by compactly supported
continuous functions, version in terms of `∫⁻`. -/
theorem exists_hasCompactSupport_lintegral_sub_le [R1Space α] [WeaklyLocallyCompactSpace α] [μ.Regular] {f : α → E}
(hf : Integrable f μ) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
∃ g : α → E, HasCompactSupport g ∧ ∫⁻ x, ‖f x - g x‖ₑ ∂μ ≤ ε ∧ Continuous g ∧ Integrable g μ :=
by
simp only [← memLp_one_iff_integrable, ← eLpNorm_one_eq_lintegral_enorm] at hf ⊢
exact hf.exists_hasCompactSupport_eLpNorm_sub_le ENNReal.one_ne_top hε
