OAI/Analysis/IrrationalRotation/Product/ProductCovariance.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.ProductModel.rotationIterate_zero line 13
2. theorem OAI.Invariant233.ProductModel.rotationIterate_add line 16
3. theorem OAI.Invariant233.ProductModel.rotationIterate_measurePreserving line 20
4. theorem OAI.Invariant233.ProductModel.shiftedPullback_mem_unitary line 24
5. theorem OAI.Invariant233.ProductModel.multiplier_commutes_shiftedPullback line 41
6. theorem OAI.Invariant233.ProductModel.commute_shiftedPullback_of_mem_factor line 58
7. theorem OAI.Invariant233.ProductModel.field_matrix_covariance line 72
8. theorem OAI.Invariant233.ProductModel.field_covariance line 93
9. theorem OAI.Invariant233.ProductModel.field_conjugacy line 109