English
Rotation by an integer multiple n on the circle is ergodic when |n| > 1.
Русский
Поворот на окружности на кратное целое n(=n) эргодичен при |n| > 1.
LaTeX
$$$\text{ergodic\_zsmul}\ T\, n$ with n ≠ 0$$
Lean4
theorem ergodic_zsmul {n : ℤ} (hn : 1 < |n|) : Ergodic fun y : AddCircle T => n • y :=
{ measurePreserving_zsmul volume (abs_pos.mp <| lt_trans zero_lt_one hn) with
aeconst_set := fun s hs hs' =>
by
let u : ℕ → AddCircle T := fun j => ↑((↑1 : ℝ) / ↑(n.natAbs ^ j) * T)
replace hn : 1 < n.natAbs := by rwa [Int.abs_eq_natAbs, Nat.one_lt_cast] at hn
have hu₀ : ∀ j, addOrderOf (u j) = n.natAbs ^ j := fun j =>
by
convert addOrderOf_div_of_gcd_eq_one (p := T) (m := 1) (pow_pos (pos_of_gt hn) j) (gcd_one_left _)
norm_cast
have hnu : ∀ j, n ^ j • u j = 0 := fun j => by
rw [← addOrderOf_dvd_iff_zsmul_eq_zero, hu₀, Int.natCast_pow, Int.natCast_natAbs, ← abs_pow, abs_dvd]
have hu₁ : ∀ j, (u j +ᵥ s : Set _) =ᵐ[volume] s := fun j => by
rw [vadd_eq_self_of_preimage_zsmul_eq_self hs' (hnu j)]
have hu₂ : Tendsto (fun j => addOrderOf <| u j) atTop atTop := by simp_rw [hu₀];
exact Nat.tendsto_pow_atTop_atTop_of_one_lt hn
rw [eventuallyConst_set']
exact ae_empty_or_univ_of_forall_vadd_ae_eq_self hs.nullMeasurableSet hu₁ hu₂ }
