English
On the circle, ergodicity persists under translation by a fixed x when applying z-smul and addition.
Русский
На окружности эргодичность сохраняется при добавлении константы x и умножении на z.
LaTeX
$$$\text{ergodic\_zsmul\_add}\ x\ n\ y$$$
Lean4
theorem ergodic_zsmul_add (x : AddCircle T) {n : ℤ} (h : 1 < |n|) : Ergodic fun y => n • y + x :=
by
set f : AddCircle T → AddCircle T := fun y => n • y + x
let e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x <| n - 1)
have he : MeasurePreserving e volume volume := measurePreserving_add_left volume (DivisibleBy.div x <| n - 1)
suffices e ∘ f ∘ e.symm = fun y => n • y by rw [← he.ergodic_conjugate_iff, this]; exact ergodic_zsmul h
replace h : n - 1 ≠ 0 := by rw [← abs_one] at h; rw [sub_ne_zero]; exact ne_of_apply_ne _ (ne_of_gt h)
have hnx : n • DivisibleBy.div x (n - 1) = x + DivisibleBy.div x (n - 1) :=
by
conv_rhs => congr; rw [← DivisibleBy.div_cancel x h]
rw [sub_smul, one_smul, sub_add_cancel]
ext y
simp only [f, e, hnx, MeasurableEquiv.coe_addLeft, MeasurableEquiv.symm_addLeft, comp_apply, smul_add, zsmul_neg',
neg_smul, neg_add_rev]
abel
