English
In a conservative system, for a measurable s with μ(s) ≠ 0, there are infinitely many m with μ(s ∩ f^(-m)(s)) > 0.
Русский
В консервативной системе для измеримого множества s с μ(s) ≠ 0 существует бесконечно много m с μ( s ∩ f^{-m}(s) ) > 0.
LaTeX
$$$\exists^{\infty} m\in\mathbb{N},\ μ(s\cap f^{-m}(s)) \neq 0.$$$
Lean4
/-- If `f` is a conservative map and `s` is a measurable set of nonzero measure, then
for infinitely many values of `m` a positive measure of points `x ∈ s` returns back to `s`
after `m` iterations of `f`. -/
theorem frequently_measure_inter_ne_zero (hf : Conservative f μ) (hs : NullMeasurableSet s μ) (h0 : μ s ≠ 0) :
∃ᶠ m in atTop, μ (s ∩ f^[m] ⁻¹' s) ≠ 0 :=
by
set t : ℕ → Set α := fun n ↦ s ∩ f^[n] ⁻¹' s
by_contra H
obtain ⟨N, hN, hmax⟩ : ∃ N, μ (t N) ≠ 0 ∧ ∀ n > N, μ (t n) = 0 :=
by
rw [Nat.frequently_atTop_iff_infinite, not_infinite] at H
convert exists_max_image _ (·) H ⟨0, by simpa⟩ using 4
rw [gt_iff_lt, ← not_le, not_imp_comm, mem_setOf]
have htm {n : ℕ} : NullMeasurableSet (t n) μ := hs.inter <| hs.preimage <| hf.toQuasiMeasurePreserving.iterate n
set T := t N \ ⋃ n > N, t n with hT
have hμT : μ T ≠ 0 := by
rwa [hT, measure_diff_null]
exact (measure_biUnion_null_iff {n | N < n}.to_countable).2 hmax
have hTm : NullMeasurableSet T μ := htm.diff <| .biUnion {n | N < n}.to_countable fun _ _ ↦ htm
rcases hf.exists_mem_iterate_mem hTm hμT with
⟨x, hxt, m, hm₀, hmt⟩
-- Then `N + m > N`, `x ∈ s`, and `f^[N + m] x = f^[N] (f^[m] x) ∈ s`.
-- This contradicts `x ∈ T ⊆ (⋃ n > N, t n)ᶜ`.
refine hxt.2 <| mem_iUnion₂.2 ⟨N + m, ?_, hxt.1.1, ?_⟩
· simpa [pos_iff_ne_zero]
· simpa only [iterate_add] using hmt.1.2
