α : Type u_1
β : Type ?u.660001
m : MeasurableSpace α
μ✝ ν : Measure α
c✝ c : ComplexMeasure α
μ : Measure α
⊢ Memℒp (fun x => ↑IsROrC.re (rnDeriv c μ x)) 1 ∧ Memℒp (fun x => ↑IsROrC.im (rnDeriv c μ x)) 1
α : Type u_1
β : Type ?u.660001
m : MeasurableSpace α
μ✝ ν : Measure α
c✝ c : ComplexMeasure α
μ : Measure α
⊢ Integrable (rnDeriv c μ)
rw [← memℒp_one_iff_integrable, ← memℒp_re_im_iff]
no goals
α : Type u_1
β : Type ?u.660001
m : MeasurableSpace α
μ✝ ν : Measure α
c✝ c : ComplexMeasure α
μ : Measure α
⊢ Memℒp (fun x => ↑IsROrC.re (rnDeriv c μ x)) 1 ∧ Memℒp (fun x => ↑IsROrC.im (rnDeriv c μ x)) 1
exact
  ⟨memℒp_one_iff_integrable.2 (SignedMeasure.integrable_rnDeriv _ _),
    memℒp_one_iff_integrable.2 (SignedMeasure.integrable_rnDeriv _ _)⟩