OAI/Analysis/IrrationalRotation/Product/ProductFieldDiagonals.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Invariant233.ProductModel.S line 9
2. theorem OAI.Invariant233.ProductModel.rotationIterate_one_eq line 12
3. theorem OAI.Invariant233.ProductModel.IsCovariantFieldRepresentation.covariance_all line 18
4. theorem OAI.Invariant233.ProductModel.IsCovariantFieldRepresentation.matrix_covariance line 61
5. theorem OAI.Invariant233.ProductModel.signedShift_mem_factor line 86
6. def OAI.Invariant233.ProductModel.fieldCoefficient line 109
7. theorem OAI.Invariant233.ProductModel.IsCovariantFieldRepresentation.measurable_fieldCoefficient line 113
8. theorem OAI.Invariant233.ProductModel.IsCovariantFieldRepresentation.norm_fieldCoefficient_le line 121
9. theorem OAI.Invariant233.ProductModel.IsCovariantFieldRepresentation.diagonal_coefficient line 134
10. theorem OAI.Invariant233.ProductModel.IsCovariantFieldRepresentation.diagonalOperator_mem_factor line 145
11. theorem OAI.Invariant233.ProductModel.IsCovariantFieldRepresentation.diagonalOperator_ae line 157
12. theorem OAI.Invariant233.ProductModel.IsCovariantFieldRepresentation.diagonalOperator_basis line 173