α : Type u_1
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : BorelSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝² : NormedSpace ℝ E
inst✝¹ : LocallyCompactSpace α
inst✝ : Measure.Regular μ
f : α → E
ε : ℝ≥0∞
hε : ε ≠ 0
hf : Memℒp f 1
⊢ ∃ g, HasCompactSupport g ∧ snorm (fun x => f x - g x) 1 μ ≤ ε ∧ Continuous g ∧ Memℒp g 1
α : Type u_1
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : BorelSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝² : NormedSpace ℝ E
inst✝¹ : LocallyCompactSpace α
inst✝ : Measure.Regular μ
f : α → E
hf : Integrable f
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ g, HasCompactSupport g ∧ (∫⁻ (x : α), ↑‖f x - g x‖₊ ∂μ) ≤ ε ∧ Continuous g ∧ Integrable g
simp only [← memℒp_one_iff_integrable, ← snorm_one_eq_lintegral_nnnorm] at hf ⊢
no goals
α : Type u_1
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : BorelSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝² : NormedSpace ℝ E
inst✝¹ : LocallyCompactSpace α
inst✝ : Measure.Regular μ
f : α → E
ε : ℝ≥0∞
hε : ε ≠ 0
hf : Memℒp f 1
⊢ ∃ g, HasCompactSupport g ∧ snorm (fun x => f x - g x) 1 μ ≤ ε ∧ Continuous g ∧ Memℒp g 1
exact hf.exists_hasCompactSupport_snorm_sub_le ENNReal.one_ne_top hε