English
If a finite invariant map on a finite measure cannot keep mass away, there exists a point in s and some iterate m such that f^m(x) ∈ s.
Русский
Если консервативная система не может держать массу вне s навсегда, то существует точка x ∈ s и некоторая итерация m такая, что f^m(x) ∈ s.
LaTeX
$$$\exists x\in s,\exists m\in(0,n), f^{[m]}(x)\in s$ under suitable measure inequalities$$
Lean4
/-- If `μ univ < n * μ s` and `f` is a map preserving measure `μ`,
then for some `x ∈ s` and `0 < m < n`, `f^[m] x ∈ s`. -/
theorem exists_mem_iterate_mem_of_measure_univ_lt_mul_measure (hf : MeasurePreserving f μ μ)
(hs : NullMeasurableSet s μ) {n : ℕ} (hvol : μ (Set.univ : Set α) < n * μ s) :
∃ x ∈ s, ∃ m ∈ Set.Ioo 0 n, f^[m] x ∈ s :=
by
have A : ∀ m, NullMeasurableSet (f^[m] ⁻¹' s) μ := fun m ↦ hs.preimage (hf.iterate m).quasiMeasurePreserving
have B : ∀ m, μ (f^[m] ⁻¹' s) = μ s := fun m ↦ (hf.iterate m).measure_preimage hs
have : μ (univ : Set α) < ∑ m ∈ Finset.range n, μ (f^[m] ⁻¹' s) := by simpa [B]
obtain ⟨i, hi, j, hj, hij, x, hxi : f^[i] x ∈ s, hxj : f^[j] x ∈ s⟩ :
∃ i < n, ∃ j < n, i ≠ j ∧ (f^[i] ⁻¹' s ∩ f^[j] ⁻¹' s).Nonempty := by
simpa using exists_nonempty_inter_of_measure_univ_lt_sum_measure μ (fun m _ ↦ A m) this
wlog hlt : i < j generalizing i j
· exact this j hj i hi hij.symm hxj hxi (hij.lt_or_gt.resolve_left hlt)
refine ⟨f^[i] x, hxi, j - i, ⟨tsub_pos_of_lt hlt, lt_of_le_of_lt (j.sub_le i) hj⟩, ?_⟩
rwa [← iterate_add_apply, tsub_add_cancel_of_le hlt.le]
