OAI/Analysis/IrrationalRotation/Rotation/Rotation.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.Rotation.action_zero line 15
  2. theorem OAI.Invariant233.Rotation.action_add line 18
  3. theorem OAI.Invariant233.Rotation.action_continuous line 23
  4. theorem OAI.Invariant233.Rotation.action_measurePreserving line 26
  5. theorem OAI.Invariant233.Rotation.orbitWeight_apply line 31
  6. theorem OAI.Invariant233.Rotation.orbitWeight_norm_le line 34
  7. theorem OAI.Invariant233.Rotation.representation_ae line 38
  8. theorem OAI.Invariant233.Rotation.representation_coordinates_ae line 45
  9. theorem OAI.Invariant233.Rotation.U_ae line 53
  10. theorem OAI.Invariant233.Rotation.U_coordinates_ae line 57
  11. theorem OAI.Invariant233.Rotation.weighted_coordinates_ae line 64
  12. theorem OAI.Invariant233.Rotation.action_one_ergodic line 72
  13. theorem OAI.Invariant233.Rotation.character_add line 82
  14. theorem OAI.Invariant233.Rotation.character_norm line 86
  15. theorem OAI.Invariant233.Rotation.character_angle line 89
  16. theorem OAI.Invariant233.Rotation.character_action_step line 93
  17. theorem OAI.Invariant233.Rotation.V_mul_U line 101
  18. theorem OAI.Invariant233.Rotation.V_mul_U_exp line 122
  19. theorem OAI.Invariant233.Rotation.operator_ext_of_coordinates line 126
  20. theorem OAI.Invariant233.Rotation.representation_one line 134
  21. theorem OAI.Invariant233.Rotation.representation_mul line 141
  22. theorem OAI.Invariant233.Rotation.representation_add line 154
  23. theorem OAI.Invariant233.Rotation.representation_smul line 170
  24. theorem OAI.Invariant233.Rotation.representation_norm_le line 184
  25. theorem OAI.Invariant233.Rotation.representation_star line 189
  26. theorem OAI.Invariant233.Rotation.representation_zero line 195
  27. def OAI.Invariant233.Rotation.representationStarAlgHom line 207
  28. theorem OAI.Invariant233.Rotation.representation_continuous line 217
  29. theorem OAI.Invariant233.Rotation.U_mem_unitary line 225
  30. theorem OAI.Invariant233.Rotation.V_mem_unitary line 228