English
For a PreErgodic f on μ and invariant measurable s, either μ(s) = 0 or μ(s^c) = 0.
Русский
Для PreErgodic f на μ и инвариантного измеримого множества s либо μ(s)=0, либо μ(s^c)=0.
LaTeX
$$$\mu(s)=0 \lor \mu(s^{c})=0$.$$
Lean4
/-- Iteration of a conservative system is a conservative system. -/
protected theorem iterate (hf : Conservative f μ) (n : ℕ) : Conservative f^[n] μ := by
-- Discharge the trivial case `n = 0`
rcases n with - | n
· exact Conservative.id μ
refine ⟨hf.1.iterate _, fun s hs hs0 => ?_⟩
rcases (hf.frequently_ae_mem_and_frequently_image_mem hs.nullMeasurableSet hs0).exists with
⟨x, _, hx⟩
/- We take a point `x ∈ s` such that `f^[k] x ∈ s` for infinitely many values of `k`,
then we choose two of these values `k < l` such that `k ≡ l [MOD (n + 1)]`.
Then `f^[k] x ∈ s` and `f^[n + 1]^[(l - k) / (n + 1)] (f^[k] x) = f^[l] x ∈ s`. -/
rw [Nat.frequently_atTop_iff_infinite] at hx
rcases Nat.exists_lt_modEq_of_infinite hx n.succ_pos with ⟨k, hk, l, hl, hkl, hn⟩
set m := (l - k) / (n + 1)
have : (n + 1) * m = l - k := by
apply Nat.mul_div_cancel'
exact (Nat.modEq_iff_dvd' hkl.le).1 hn
refine ⟨f^[k] x, hk, m, ?_, ?_⟩
· intro hm
rw [hm, mul_zero, eq_comm, tsub_eq_zero_iff_le] at this
exact this.not_gt hkl
· rwa [← iterate_mul, this, ← iterate_add_apply, tsub_add_cancel_of_le]
exact hkl.le
