α : 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
ε : ℝ≥0∞
hε : ε ≠ 0
hf : Memℒp f 1
⊢ ∃ g, snorm (fun x => f x - ↑g x) 1 μ ≤ ε ∧ 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✝ : Measure.WeaklyRegular μ
f : α → E
hf : Integrable f
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ g, (∫⁻ (x : α), ↑‖f x - ↑g x‖₊ ∂μ) ≤ ε ∧ 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✝ : Measure.WeaklyRegular μ
f : α → E
ε : ℝ≥0∞
hε : ε ≠ 0
hf : Memℒp f 1
⊢ ∃ g, snorm (fun x => f x - ↑g x) 1 μ ≤ ε ∧ Memℒp (↑g) 1
exact hf.exists_boundedContinuous_snorm_sub_le ENNReal.one_ne_top hε