𝕜 : Type ?u.84709
M : Type ?u.84712
α : Type u_1
G : Type u_2
E : Type u_3
F : Type ?u.84724
inst✝⁹ : MeasurableSpace G
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NormedAddCommGroup F
μ✝ : Measure G
f✝ : G → E
g✝ : G
inst✝⁴ : Group G
inst✝³ : MeasurableSpace α
inst✝² : MulAction G α
inst✝¹ : MeasurableSMul G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
f : α → E
g : G
h : MeasurableEmbedding fun x => g • x
⊢ (∫ (x : α), f (g • x) ∂μ) = ∫ (x : α), f x ∂μ
𝕜 : Type ?u.84709
M : Type ?u.84712
α : Type u_1
G : Type u_2
E : Type u_3
F : Type ?u.84724
inst✝⁹ : MeasurableSpace G
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NormedAddCommGroup F
μ✝ : Measure G
f✝ : G → E
g✝ : G
inst✝⁴ : Group G
inst✝³ : MeasurableSpace α
inst✝² : MulAction G α
inst✝¹ : MeasurableSMul G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
f : α → E
g : G
⊢ (∫ (x : α), f (g • x) ∂μ) = ∫ (x : α), f x ∂μ
have h : MeasurableEmbedding fun x : α => g • x := (MeasurableEquiv.smul g).measurableEmbedding
no goals
𝕜 : Type ?u.84709
M : Type ?u.84712
α : Type u_1
G : Type u_2
E : Type u_3
F : Type ?u.84724
inst✝⁹ : MeasurableSpace G
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NormedAddCommGroup F
μ✝ : Measure G
f✝ : G → E
g✝ : G
inst✝⁴ : Group G
inst✝³ : MeasurableSpace α
inst✝² : MulAction G α
inst✝¹ : MeasurableSMul G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
f : α → E
g : G
h : MeasurableEmbedding fun x => g • x
⊢ (∫ (x : α), f (g • x) ∂μ) = ∫ (x : α), f x ∂μ
rw [← h.integral_map, map_smul]