OAI/GroupTheory/PolycyclicRecognition/Analysis/CompactErgodicDecomposition.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Ergodic decomposition on compact metrizable action spaces

Conditioning on the invariant sigma algebra gives ergodic components almost everywhere. Repairing the null exceptional set on the factor preserves exact orbit invariance of the component map.

  1. theorem OAI.PolycyclicRecognition.ergodicDecompositionInput_of_compactMetric line 25