smulInvariantMeasure_iterateMulAct

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⟩

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