English
If a map f on a measure space (α, m) is PreErgodic with respect to a measure μ, then for any scalar c, f is PreErgodic with respect to the scaled measure c · μ.
Русский
Пусть отображение f на измеримом пространстве (α, m) является предергодичным относительно меры μ. Тогда для любого скаляра c отображение f является предергодичным относительно масштабированной меры c · μ.
LaTeX
$$$\mathrm{PreErgodic}(f, \mu) \Rightarrow \forall c \; \mathrm{PreErgodic}(f, c \cdot \mu)$$$
Lean4
theorem smul_measure {R : Type*} [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] (hf : PreErgodic f μ) (c : R) :
PreErgodic f (c • μ) where aeconst_set _s hs hfs := (hf.aeconst_set hs hfs).anti <| ae_smul_measure_le _
