α : 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
ε : ℝ
hε : 0 < ε
hf : Memℒp f (ENNReal.ofReal 1)
⊢ ∃ g, HasCompactSupport g ∧ (∫ (x : α), ‖f x - g x‖ ∂μ) ≤ ε ∧ Continuous g ∧ Memℒp g (ENNReal.ofReal 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
ε : ℝ
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, ← ENNReal.ofReal_one]
  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
ε : ℝ
hε : 0 < ε
hf : Memℒp f (ENNReal.ofReal 1)
⊢ ∃ g, HasCompactSupport g ∧ (∫ (x : α), ‖f x - g x‖ ∂μ) ≤ ε ∧ Continuous g ∧ Memℒp g (ENNReal.ofReal 1)
simpa using hf.exists_hasCompactSupport_integral_rpow_sub_le zero_lt_one hε