α : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_1
𝕜 : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : α → E
c : E
hf : Memℒp f 1
⊢ Memℒp (fun x => inner c (f x)) 1
α : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_1
𝕜 : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : α → E
c : E
hf : Integrable f
⊢ Integrable fun x => inner c (f x)
rw [← memℒp_one_iff_integrable] at hf ⊢
no goals
α : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_1
𝕜 : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : α → E
c : E
hf : Memℒp f 1
⊢ Memℒp (fun x => inner c (f x)) 1
exact hf.const_inner c