OAI/NumberTheory/DukePrimeDegree/Dynamics/SingleBlockComponents.lean
1 declarations, 0 contain sorry, 0 declared as axioms
One actual root block and its canonical ergodic components
Ergodicity, diagonal velocity recurrence and the local block-preserving stabilizer conclusion now refer to the same full-subgroup conditional kernel. The selected root flow is ergodic on each component by Mautner; no ergodicity of a selected diagonal element is assumed.
- theorem
OAI.DukePrimeDegree.ae_singleBlock_component_ergodic_and_locally_block_preservingline 23