case pos
α : Type u_2
E : Type u_3
F : Type ?u.1387726
𝕜 : Type ?u.1387729
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g✝ : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1390420
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν : Measure α
β : Type u_1
x✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
g : β → E
hgm : AEStronglyMeasurable g (Measure.map f μ)
⊢ (∫ (y : β), g y ∂Measure.map f μ) = ∫ (x : α), g (f x) ∂μ

case neg
α : Type u_2
E : Type u_3
F : Type ?u.1387726
𝕜 : Type ?u.1387729
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g✝ : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1390420
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν : Measure α
β : Type u_1
x✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
g : β → E
hgm : ¬AEStronglyMeasurable g (Measure.map f μ)
⊢ (∫ (y : β), g y ∂Measure.map f μ) = ∫ (x : α), g (f x) ∂μ
α : Type u_2
E : Type u_3
F : Type ?u.1387726
𝕜 : Type ?u.1387729
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g✝ : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1390420
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν : Measure α
β : Type u_1
x✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
g : β → E
⊢ (∫ (y : β), g y ∂Measure.map f μ) = ∫ (x : α), g (f x) ∂μ
by_cases hgm : AEStronglyMeasurable g (Measure.map f μ)
no goals
case pos
α : Type u_2
E : Type u_3
F : Type ?u.1387726
𝕜 : Type ?u.1387729
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g✝ : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1390420
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν : Measure α
β : Type u_1
x✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
g : β → E
hgm : AEStronglyMeasurable g (Measure.map f μ)
⊢ (∫ (y : β), g y ∂Measure.map f μ) = ∫ (x : α), g (f x) ∂μ
exact MeasureTheory.integral_map hf.measurable.aemeasurable hgm
case neg
α : Type u_2
E : Type u_3
F : Type ?u.1387726
𝕜 : Type ?u.1387729
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g✝ : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1390420
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν : Measure α
β : Type u_1
x✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
g : β → E
hgm : ¬AEStronglyMeasurable g (Measure.map f μ)
⊢ ¬AEStronglyMeasurable (fun x => g (f x)) μ
case neg
α : Type u_2
E : Type u_3
F : Type ?u.1387726
𝕜 : Type ?u.1387729
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g✝ : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1390420
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν : Measure α
β : Type u_1
x✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
g : β → E
hgm : ¬AEStronglyMeasurable g (Measure.map f μ)
⊢ (∫ (y : β), g y ∂Measure.map f μ) = ∫ (x : α), g (f x) ∂μ
rw [integral_non_aestronglyMeasurable hgm, integral_non_aestronglyMeasurable]
no goals
case neg
α : Type u_2
E : Type u_3
F : Type ?u.1387726
𝕜 : Type ?u.1387729
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace F
f✝ g✝ : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1390420
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
ν : Measure α
β : Type u_1
x✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
g : β → E
hgm : ¬AEStronglyMeasurable g (Measure.map f μ)
⊢ ¬AEStronglyMeasurable (fun x => g (f x)) μ
refine' fun hgf => hgm (hf.aestronglyMeasurable_map_iff.2 hgf)