α : Type u_1
β : Type ?u.1131588
γ : Type ?u.1131591
δ : Type ?u.1131594
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
𝕜 : Type u_2
inst✝ : IsROrC 𝕜
f : α → 𝕜
⊢ Memℒp (fun x => ↑IsROrC.re (f x)) 1 ∧ Memℒp (fun x => ↑IsROrC.im (f x)) 1 ↔ Memℒp f 1
α : Type u_1
β : Type ?u.1131588
γ : Type ?u.1131591
δ : Type ?u.1131594
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
𝕜 : Type u_2
inst✝ : IsROrC 𝕜
f : α → 𝕜
⊢ ((Integrable fun x => ↑IsROrC.re (f x)) ∧ Integrable fun x => ↑IsROrC.im (f x)) ↔ Integrable f
simp_rw [← memℒp_one_iff_integrable]
no goals
α : Type u_1
β : Type ?u.1131588
γ : Type ?u.1131591
δ : Type ?u.1131594
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
𝕜 : Type u_2
inst✝ : IsROrC 𝕜
f : α → 𝕜
⊢ Memℒp (fun x => ↑IsROrC.re (f x)) 1 ∧ Memℒp (fun x => ↑IsROrC.im (f x)) 1 ↔ Memℒp f 1
exact memℒp_re_im_iff