OAI/LinearAlgebra/MatrixMultiplication/Separation/ComplexModularSeparation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Finite type counts, hierarchy separation and tensor execution bounds.

  1. abbrev OAI.MatrixMultiplication.Foundation.Separation.AuxiliaryGroup line 13
  2. def OAI.MatrixMultiplication.Foundation.Separation.gridToGroup line 15
  3. def OAI.MatrixMultiplication.Foundation.Separation.gridToReal line 18
  4. theorem OAI.MatrixMultiplication.Foundation.Separation.gridToReal_injective line 21
  5. theorem OAI.MatrixMultiplication.Foundation.Separation.squaredNorm_gridToReal line 30
  6. theorem OAI.MatrixMultiplication.Foundation.Separation.dot_gridToReal line 34
  7. theorem OAI.MatrixMultiplication.Foundation.Separation.grid_group_collision_lift line 38
  8. theorem OAI.MatrixMultiplication.Foundation.Separation.grid_sphere_slice_collision line 59
  9. theorem OAI.MatrixMultiplication.Foundation.Separation.indexed_grid_collision line 83
  10. theorem OAI.MatrixMultiplication.Foundation.Separation.exists_modular_separation line 101
  11. theorem OAI.MatrixMultiplication.Foundation.Separation.card_auxiliaryGroup line 142