measure_symmDiff_preimage_iterate_le

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]

Похожие утверждения