OAI/GroupTheory/PolycyclicRecognition/Analysis/ErgodicMap.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Pushforward of an ergodic measure by an equivariant map

  1. theorem OAI.PolycyclicRecognition.ergodicSMul_map line 16

    Source documentation

    An equivariant measurable factor of an ergodic action is ergodic.

    theorem ergodicSMul_map (μ : Measure X) [ErgodicSMul G X μ]
    (f : X → Y) (hf : Measurable f) (heq : ∀ (g : G) x, f (g • x) = g • f x) :
    ErgodicSMul G Y (μ.map f) := by
…