case intro
G : Type u_2
M : Type ?u.82889
α : Type u_1
s : Set α
m : MeasurableSpace α
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
c : G
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x : G
hs : x • s =ᶠ[ae μ] s
k : ℤ
hy : x ^ k ∈ Subgroup.zpowers x
⊢ x ^ k • s =ᶠ[ae μ] s
G : Type u_2
M : Type ?u.82889
α : Type u_1
s : Set α
m : MeasurableSpace α
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
c : G
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x y : G
hs : x • s =ᶠ[ae μ] s
hy : y ∈ Subgroup.zpowers x
⊢ y • s =ᶠ[ae μ] s
obtain ⟨k, rfl⟩ := Subgroup.mem_zpowers_iff.mp hy
case intro
G : Type u_2
M : Type ?u.82889
α : Type u_1
s : Set α
m : MeasurableSpace α
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
c : G
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x : G
hs : x • s =ᶠ[ae μ] s
k : ℤ
hy : x ^ k ∈ Subgroup.zpowers x
e : α ≃ α := ↑(MulAction.toPermHom G α) x
⊢ x ^ k • s =ᶠ[ae μ] s
case intro
G : Type u_2
M : Type ?u.82889
α : Type u_1
s : Set α
m : MeasurableSpace α
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
c : G
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x : G
hs : x • s =ᶠ[ae μ] s
k : ℤ
hy : x ^ k ∈ Subgroup.zpowers x
⊢ x ^ k • s =ᶠ[ae μ] s
let e : α ≃ α := MulAction.toPermHom G α x
case intro
G : Type u_2
M : Type ?u.82889
α : Type u_1
s : Set α
m : MeasurableSpace α
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
c : G
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x : G
hs : x • s =ᶠ[ae μ] s
k : ℤ
hy : x ^ k ∈ Subgroup.zpowers x
e : α ≃ α := ↑(MulAction.toPermHom G α) x
he : QuasiMeasurePreserving ↑e
⊢ x ^ k • s =ᶠ[ae μ] s
case intro
G : Type u_2
M : Type ?u.82889
α : Type u_1
s : Set α
m : MeasurableSpace α
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
c : G
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x : G
hs : x • s =ᶠ[ae μ] s
k : ℤ
hy : x ^ k ∈ Subgroup.zpowers x
e : α ≃ α := ↑(MulAction.toPermHom G α) x
⊢ x ^ k • s =ᶠ[ae μ] s
have he : QuasiMeasurePreserving e μ μ := (measurePreserving_smul x μ).quasiMeasurePreserving
case intro
G : Type u_2
M : Type ?u.82889
α : Type u_1
s : Set α
m : MeasurableSpace α
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
c : G
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x : G
hs : x • s =ᶠ[ae μ] s
k : ℤ
hy : x ^ k ∈ Subgroup.zpowers x
e : α ≃ α := ↑(MulAction.toPermHom G α) x
he : QuasiMeasurePreserving ↑e
he' : QuasiMeasurePreserving ↑e.symm
⊢ x ^ k • s =ᶠ[ae μ] s
case intro
G : Type u_2
M : Type ?u.82889
α : Type u_1
s : Set α
m : MeasurableSpace α
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
c : G
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x : G
hs : x • s =ᶠ[ae μ] s
k : ℤ
hy : x ^ k ∈ Subgroup.zpowers x
e : α ≃ α := ↑(MulAction.toPermHom G α) x
he : QuasiMeasurePreserving ↑e
⊢ x ^ k • s =ᶠ[ae μ] s
have he' : QuasiMeasurePreserving e.symm μ μ :=
  (measurePreserving_smul x⁻¹ μ).quasiMeasurePreserving
case intro
G : Type u_2
M : Type ?u.82889
α : Type u_1
s : Set α
m : MeasurableSpace α
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
c : G
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x : G
hs : x • s =ᶠ[ae μ] s
k : ℤ
hy : x ^ k ∈ Subgroup.zpowers x
e : α ≃ α := ↑(MulAction.toPermHom G α) x
he : QuasiMeasurePreserving ↑e
he' : QuasiMeasurePreserving ↑e.symm
h : ↑(e ^ k) '' s =ᶠ[ae μ] s
⊢ x ^ k • s =ᶠ[ae μ] s
case intro
G : Type u_2
M : Type ?u.82889
α : Type u_1
s : Set α
m : MeasurableSpace α
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
c : G
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x : G
hs : x • s =ᶠ[ae μ] s
k : ℤ
hy : x ^ k ∈ Subgroup.zpowers x
e : α ≃ α := ↑(MulAction.toPermHom G α) x
he : QuasiMeasurePreserving ↑e
he' : QuasiMeasurePreserving ↑e.symm
⊢ x ^ k • s =ᶠ[ae μ] s
have h := he.image_zpow_ae_eq he' k hs
case intro
G : Type u_2
M : Type ?u.82889
α : Type u_1
s : Set α
m : MeasurableSpace α
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
c : G
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x : G
hs : x • s =ᶠ[ae μ] s
k : ℤ
hy : x ^ k ∈ Subgroup.zpowers x
e : α ≃ α := ↑(MulAction.toPermHom G α) x
he : QuasiMeasurePreserving ↑e
he' : QuasiMeasurePreserving ↑e.symm
h : (fun a => ↑(↑(MulAction.toPermHom G α) (x ^ k)) a) '' s =ᶠ[ae μ] s
⊢ x ^ k • s =ᶠ[ae μ] s
case intro
G : Type u_2
M : Type ?u.82889
α : Type u_1
s : Set α
m : MeasurableSpace α
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
c : G
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x : G
hs : x • s =ᶠ[ae μ] s
k : ℤ
hy : x ^ k ∈ Subgroup.zpowers x
e : α ≃ α := ↑(MulAction.toPermHom G α) x
he : QuasiMeasurePreserving ↑e
he' : QuasiMeasurePreserving ↑e.symm
h : ↑(e ^ k) '' s =ᶠ[ae μ] s
⊢ x ^ k • s =ᶠ[ae μ] s
simp only [← MonoidHom.map_zpow] at h
no goals
case intro
G : Type u_2
M : Type ?u.82889
α : Type u_1
s : Set α
m : MeasurableSpace α
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
c : G
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x : G
hs : x • s =ᶠ[ae μ] s
k : ℤ
hy : x ^ k ∈ Subgroup.zpowers x
e : α ≃ α := ↑(MulAction.toPermHom G α) x
he : QuasiMeasurePreserving ↑e
he' : QuasiMeasurePreserving ↑e.symm
h : (fun a => ↑(↑(MulAction.toPermHom G α) (x ^ k)) a) '' s =ᶠ[ae μ] s
⊢ x ^ k • s =ᶠ[ae μ] s
simpa only [MulAction.toPermHom_apply, MulAction.toPerm_apply, image_smul] using h