OAI/Analysis/IrrationalRotation/Product/ProductErgodicity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.InvariantProjection.ProductRotation.integer_affine_independent line 15
2. theorem OAI.InvariantProjection.ProductRotation.measurePreserving_product_translation line 22
3. theorem OAI.InvariantProjection.ProductRotation.product_rotation_integer_ergodic line 37
4. theorem OAI.InvariantProjection.ProductRotation.product_rotation_ergodic line 55
5. theorem OAI.InvariantProjection.ProductRotation.product_rotation_totalErgodic line 62