OAI/GroupTheory/PolycyclicRecognition/Analysis/OrbitAverageErgodicity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A countable convex-averaging criterion for ergodicity

If indicators in a determining family admit finite orbit averages converging almost everywhere to constants, restriction to any invariant set is a scalar multiple of the original probability. Evaluating on its complement gives the zero-one law.

  1. theorem OAI.PolycyclicRecognition.ergodicSMul_of_orbitAverages line 26