English
For a measurable f, SMulInvariantMeasure (IterateMulAct f) α μ holds if and only if f is measure-preserving with respect to μ.
Русский
Для измеримого f имеется эквивалентность: SMulInvariantMeasure (IterateMulAct f) μ ⇔ MeasurePreserving f μ μ.
LaTeX
$$$\\text{smulInvariantMeasure}_{IterateMulAct(f)}(\\mu) \\iff \\text{MeasurePreserving}(f,\\mu,\\mu)$, при условии, что $f$ измерим.$$
Lean4
@[to_additive]
theorem smulInvariantMeasure_iterateMulAct {f : α → α} {_ : MeasurableSpace α} {μ : Measure α} (hf : Measurable f) :
SMulInvariantMeasure (IterateMulAct f) α μ ↔ MeasurePreserving f μ μ :=
⟨fun _ ↦
have := hf.measurableSMul₂_iterateMulAct
measurePreserving_smul (IterateMulAct.mk (f := f) 1) μ,
MeasurePreserving.smulInvariantMeasure_iterateMulAct⟩