α : Type u_2
β : Type u_1
γ : Type ?u.1093696
δ : Type ?u.1093699
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_3
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → β
φ : α → 𝕜
hf : Memℒp f 1
hφ : Memℒp φ ⊤
⊢ Memℒp (φ • f) 1
α : Type u_2
β : Type u_1
γ : Type ?u.1093696
δ : Type ?u.1093699
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_3
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → β
φ : α → 𝕜
hf : Integrable f
hφ : Memℒp φ ⊤
⊢ Integrable (φ • f)
rw [← memℒp_one_iff_integrable] at hf ⊢
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.1093696
δ : Type ?u.1093699
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_3
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → β
φ : α → 𝕜
hf : Memℒp f 1
hφ : Memℒp φ ⊤
⊢ Memℒp (φ • f) 1
exact Memℒp.smul_of_top_right hf hφ