prob_eq_zero_or_one — Mathlib

English

If f^[n] is PreErgodic with μ, then f is PreErgodic with μ.

Русский

Если f^n является преэргодичным относительно μ, то и f является преэргодичным относительно μ.

LaTeX

$$$\text{PreErgodic}(f^{[n]},\mu)\Rightarrow \text{PreErgodic}(f,\mu).$$$

Lean4

/-- On a probability space, the (pre)ergodicity condition is a zero one law. -/
theorem prob_eq_zero_or_one [IsProbabilityMeasure μ] (hf : PreErgodic f μ) (hs : MeasurableSet s) (hs' : f ⁻¹' s = s) :
    μ s = 0 ∨ μ s = 1 := by simpa [hs] using hf.measure_self_or_compl_eq_zero hs hs'

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