English
If f is conservative on μ and s is null-measurable with positive measure, there exist x ∈ s and m ≠ 0 such that f^m x ∈ s.
Русский
Если f консервативно действует на μ, и s—нулеизмеримо множество с μ(s) > 0, то найдётся x ∈ s и m ≠ 0 такое, что f^m(x) ∈ s.
LaTeX
$$$\exists x \in s, \exists m\neq 0, f^{[m]}(x) \in s$ under hf, hs and μ(s) ≠ 0.$$
Lean4
/-- If `f` is a conservative self-map and `s` is a null measurable set of nonzero measure,
then there exists a point `x ∈ s` that returns to `s` under a non-zero iteration of `f`. -/
theorem exists_mem_iterate_mem (hf : Conservative f μ) (hsm : NullMeasurableSet s μ) (hs₀ : μ s ≠ 0) :
∃ x ∈ s, ∃ m ≠ 0, f^[m] x ∈ s :=
by
rcases hsm.exists_measurable_subset_ae_eq with ⟨t, hsub, htm, hts⟩
rcases hf.exists_mem_iterate_mem' htm (by rwa [measure_congr hts]) with ⟨x, hxt, m, hm₀, hmt⟩
exact ⟨x, hsub hxt, m, hm₀, hsub hmt⟩
