α : Type u_3
β : Type u_2
γ : Type ?u.857469
δ : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → δ
g : δ → β
hg : AEStronglyMeasurable g (Measure.map f μ)
hf : AEMeasurable f
⊢ Memℒp g 1 ↔ Memℒp (g ∘ f) 1
α : Type u_3
β : Type u_2
γ : Type ?u.857469
δ : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → δ
g : δ → β
hg : AEStronglyMeasurable g (Measure.map f μ)
hf : AEMeasurable f
⊢ Integrable g ↔ Integrable (g ∘ f)
simp_rw [← memℒp_one_iff_integrable]
no goals
α : Type u_3
β : Type u_2
γ : Type ?u.857469
δ : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → δ
g : δ → β
hg : AEStronglyMeasurable g (Measure.map f μ)
hf : AEMeasurable f
⊢ Memℒp g 1 ↔ Memℒp (g ∘ f) 1
exact memℒp_map_measure_iff hg hf