English
Let e be a measure-preserving equivalence of α with itself, and let k be an integer. If the image of a measurable set s under e is almost-equal to s, then the image under e^k is also almost-equal to s.
Русский
Пусть e — эквивалент измеримости на α; если образ множества s под e равен почти s, то образ под e^k равен почти s.
LaTeX
$$$\forall k \in \mathbb{Z}, \; e(s) =_{ae}^{\mu} s \Rightarrow e^{k}(s) =_{ae}^{\mu} s$$$
Lean4
theorem image_zpow_ae_eq {s : Set α} {e : α ≃ α} (he : QuasiMeasurePreserving e μ μ)
(he' : QuasiMeasurePreserving e.symm μ μ) (k : ℤ) (hs : e '' s =ᵐ[μ] s) : (⇑(e ^ k)) '' s =ᵐ[μ] s :=
by
rw [Equiv.image_eq_preimage]
obtain ⟨k, rfl | rfl⟩ := k.eq_nat_or_neg
· replace hs : (⇑e⁻¹) ⁻¹' s =ᵐ[μ] s := by rwa [Equiv.image_eq_preimage] at hs
replace he' : (⇑e⁻¹)^[k] ⁻¹' s =ᵐ[μ] s := he'.preimage_iterate_ae_eq k hs
rwa [Equiv.Perm.iterate_eq_pow e⁻¹ k, inv_pow e k] at he'
· rw [zpow_neg, zpow_natCast]
replace hs : e ⁻¹' s =ᵐ[μ] s := by
convert he.preimage_ae_eq hs.symm
rw [Equiv.preimage_image]
replace he : (⇑e)^[k] ⁻¹' s =ᵐ[μ] s := he.preimage_iterate_ae_eq k hs
rwa [Equiv.Perm.iterate_eq_pow e k] at he
