English
If f preserves μ and s is measurable, then the measure of the symmetric difference between s and its preimage under f relates to measure of s.
Русский
Если f сохраняет μ, то мера симметрической разности между s и её предобразом по f связана с мерой s.
LaTeX
$$$\text{MeasurePreserving } f\, μ\, μ \rightarrow \forall s, μ(f^{-1}(s) \triangle s) \le ?$$$
Lean4
theorem measure_symmDiff_preimage_iterate_le (hf : MeasurePreserving f μ μ) (hs : NullMeasurableSet s μ) (n : ℕ) :
μ (s ∆ (f^[n] ⁻¹' s)) ≤ n • μ (s ∆ (f ⁻¹' s)) := by
induction n with
| zero => simp
| succ n ih =>
simp only [add_smul, one_smul]
grw [← ih, measure_symmDiff_le s (f^[n] ⁻¹' s) (f^[n + 1] ⁻¹' s)]
replace hs : NullMeasurableSet (s ∆ (f ⁻¹' s)) μ := hs.symmDiff <| hs.preimage hf.quasiMeasurePreserving
rw [iterate_succ', preimage_comp, ← preimage_symmDiff, (hf.iterate n).measure_preimage hs]