OAI/GroupTheory/PolycyclicRecognition/Analysis/CountableErgodicComponents.lean

Ergodicity of conditioning on the invariant sigma algebra

For a countable action, choose convergent finite convex orbit averages for each member of a countable determining family. Their invariant limits are constant on almost every conditional measure. The averaging zero-one criterion then proves that these conditional measures are ergodic.