α : Type u_2
β : Type u_3
γ : Type ?u.935096
δ : Type u_1
m : MeasurableSpace α
μ ν✝ : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
ν : Measure δ
g : δ → β
f : α → δ
hf : MeasurePreserving f
hg : AEStronglyMeasurable g (Measure.map f μ)
⊢ Integrable (g ∘ f) ↔ Integrable g
α : Type u_2
β : Type u_3
γ : Type ?u.935096
δ : Type u_1
m : MeasurableSpace α
μ ν✝ : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
ν : Measure δ
g : δ → β
f : α → δ
hf : MeasurePreserving f
hg : AEStronglyMeasurable g ν
⊢ Integrable (g ∘ f) ↔ Integrable g
rw [← hf.map_eq] at hg ⊢
no goals
α : Type u_2
β : Type u_3
γ : Type ?u.935096
δ : Type u_1
m : MeasurableSpace α
μ ν✝ : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
ν : Measure δ
g : δ → β
f : α → δ
hf : MeasurePreserving f
hg : AEStronglyMeasurable g (Measure.map f μ)
⊢ Integrable (g ∘ f) ↔ Integrable g
exact (integrable_map_measure hg hf.measurable.aemeasurable).symm