English
A self-map preserving μ a on α and mapped to comap by subtype retains measure-preserving property when restricted to a measurable subset.
Русский
Самое отображение сохраняющее μ на α сохраняет свойство сохранения меры при ограничении к измеримому подмножеству.
LaTeX
$$$\text{MeasurePreserving} (\text{Subtype.val}: s\to α) (μ_a\;\text{comap } \text{Subtype.val}) (μ_a\restriction s)$$$
Lean4
/-- A self-map preserving a finite measure is conservative: if `μ s ≠ 0`, then at least one point
`x ∈ s` comes back to `s` under iterations of `f`. Actually, a.e. point of `s` comes back to `s`
infinitely many times, see `MeasureTheory.MeasurePreserving.conservative` and theorems about
`MeasureTheory.Conservative`. -/
theorem exists_mem_iterate_mem [IsFiniteMeasure μ] (hf : MeasurePreserving f μ μ) (hs : NullMeasurableSet s μ)
(hs' : μ s ≠ 0) : ∃ x ∈ s, ∃ m ≠ 0, f^[m] x ∈ s :=
by
rcases ENNReal.exists_nat_mul_gt hs' (measure_ne_top μ (Set.univ : Set α)) with ⟨N, hN⟩
rcases hf.exists_mem_iterate_mem_of_measure_univ_lt_mul_measure hs hN with ⟨x, hx, m, hm, hmx⟩
exact ⟨x, hx, m, hm.1.ne', hmx⟩
