OAI/Analysis/FiniteFactor/CrossedProduct/RotationErgodic.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sourceTorusRepresentative_rotationStep line 9
2. theorem OAI.FiniteFactor.coordinateRotate_ergodic line 21

   Source documentation

   Ergodicity for the exact real-coordinate model used by the original algebra.

   theorem coordinateRotate_ergodic (θ : SourceCoordinate → ℝ)
       (hr : SourceRationalIndependent θ) :
       Ergodic (coordinateRotate θ 1) sourceSamplingHaar :=
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceRationalIndependent, OAI.FiniteFactor.coordinateRotate, OAI.FiniteFactor.sourceSamplingHaar

3. theorem OAI.FiniteFactor.sourceRotation_invariant_constant line 28