OAI/NumberTheory/DukePrimeDegree/Dynamics/NormalizerErgodicComponents.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual ergodic components covariant under a normalizer

The countable dense subgroup is chosen closed under all conjugates by one specified normalizer. The resulting conditional kernel consists of ergodic components for the full subgroup, and transforms covariantly under that normalizer. Individual components are not assumed fixed.

  1. theorem OAI.DukePrimeDegree.lattice_subgroup_normalizer_ergodic_decomposition line 22