α : 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✝ : Measure.WeaklyRegular μ
f : α → E
ε : ℝ
hε : 0 < ε
hf : Memℒp f (ENNReal.ofReal 1)
⊢ ∃ g, (∫ (x : α), ‖f x - ↑g x‖ ∂μ) ≤ ε ∧ 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✝ : Measure.WeaklyRegular μ
f : α → E
hf : Integrable f
ε : ℝ
hε : 0 < ε
⊢ ∃ g, (∫ (x : α), ‖f x - ↑g x‖ ∂μ) ≤ ε ∧ 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✝ : Measure.WeaklyRegular μ
f : α → E
ε : ℝ
hε : 0 < ε
hf : Memℒp f (ENNReal.ofReal 1)
⊢ ∃ g, (∫ (x : α), ‖f x - ↑g x‖ ∂μ) ≤ ε ∧ Memℒp (↑g) (ENNReal.ofReal 1)
simpa using hf.exists_boundedContinuous_integral_rpow_sub_le zero_lt_one hε