smulInvariantMeasure_iterateMulAct

English

If f is measure-preserving, then the action generated by iterates of f preserves μ; i.e., μ is invariant under the action of IterateMulAct f.

Русский

Если f сохраняет меру μ, тогда действие, порождаемое повторениями f, сохраняет μ; то есть μ инвариантна относительно действия IterateMulAct f.

LaTeX

$$$\\forall n \\in \\mathbb{N}, \\forall S\\subseteq \\alpha\\ (\\text{Measurable}(S) \\Rightarrow \\mu((f^n)^{-1}(S)) = \\mu(S))$$$

Lean4

@[to_additive]
theorem smulInvariantMeasure_iterateMulAct {f : α → α} {_ : MeasurableSpace α} {μ : Measure α}
    (hf : MeasurePreserving f μ μ) : SMulInvariantMeasure (IterateMulAct f) α μ :=
  ⟨fun n _s hs ↦ (hf.iterate n.val).measure_preimage hs.nullMeasurableSet⟩

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