OAI/LinearAlgebra/MatrixMultiplication/Separation/ComplexBalancedSeparation.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Finite type counts, hierarchy separation and tensor execution bounds.

  1. def OAI.MatrixMultiplication.Foundation.BalancedSeparation.singlePairingX line 18
  2. def OAI.MatrixMultiplication.Foundation.BalancedSeparation.singlePairingY line 24
  3. def OAI.MatrixMultiplication.Foundation.BalancedSeparation.singlePairingZ line 30
  4. theorem OAI.MatrixMultiplication.Foundation.BalancedSeparation.singlePairing_matrix line 36
  5. theorem OAI.MatrixMultiplication.Foundation.BalancedSeparation.singlePairingXZ_matrix line 47
  6. theorem OAI.MatrixMultiplication.Foundation.BalancedSeparation.singlePairingYZ_matrix line 58
  7. theorem OAI.MatrixMultiplication.Foundation.BalancedSeparation.singlePairing_budget line 69
  8. def OAI.MatrixMultiplication.Foundation.BalancedSeparation.piPairEquiv line 80
  9. theorem OAI.MatrixMultiplication.Foundation.BalancedSeparation.matrixBank_identity line 88
  10. def OAI.MatrixMultiplication.Foundation.BalancedSeparation.factorDimension line 103
  11. def OAI.MatrixMultiplication.Foundation.BalancedSeparation.bankDimension line 106
  12. abbrev OAI.MatrixMultiplication.Foundation.BalancedSeparation.BankIndex line 109
  13. theorem OAI.MatrixMultiplication.Foundation.BalancedSeparation.card_BankIndex line 112
  14. def OAI.MatrixMultiplication.Foundation.BalancedSeparation.bankIndexFinEquiv line 116
  15. theorem OAI.MatrixMultiplication.Foundation.BalancedSeparation.bank_volume line 121
  16. theorem OAI.MatrixMultiplication.Foundation.BalancedSeparation.bankDimension_pos line 132
  17. theorem OAI.MatrixMultiplication.Foundation.BalancedSeparation.bank_volume_le_auxiliary line 142
  18. def OAI.MatrixMultiplication.Foundation.BalancedSeparation.bankMatrixCoordinate line 148
  19. def OAI.MatrixMultiplication.Foundation.BalancedSeparation.matrixBank line 154
  20. theorem OAI.MatrixMultiplication.Foundation.BalancedSeparation.matrixBank_numeric line 159
  21. def OAI.MatrixMultiplication.Foundation.BalancedSeparation.orientedPairingBank line 177
  22. def OAI.MatrixMultiplication.Foundation.BalancedSeparation.pairingBankX line 182
  23. def OAI.MatrixMultiplication.Foundation.BalancedSeparation.pairingBankY line 187
  24. def OAI.MatrixMultiplication.Foundation.BalancedSeparation.pairingBankZ line 192
  25. theorem OAI.MatrixMultiplication.Foundation.BalancedSeparation.orientedPairingBank_numeric line 197
  26. theorem OAI.MatrixMultiplication.Foundation.BalancedSeparation.orientedPairingBank_directSum_rank line 215
  27. theorem OAI.MatrixMultiplication.Foundation.BalancedSeparation.orientedPairingBank_directSum_borderRank line 225
  28. def OAI.MatrixMultiplication.Foundation.BalancedSeparation.physicalPairingSlot line 246
  29. theorem OAI.MatrixMultiplication.Foundation.BalancedSeparation.physicalPairingSlot_fiber_card line 249
  30. theorem OAI.MatrixMultiplication.Foundation.BalancedSeparation.physicalPairingSlot_product line 253
  31. def OAI.MatrixMultiplication.Foundation.BalancedSeparation.sixSlot line 262
  32. theorem OAI.MatrixMultiplication.Foundation.BalancedSeparation.six_bankDimension line 266
  33. theorem OAI.MatrixMultiplication.Foundation.BalancedSeparation.six_bank_volume line 284
  34. theorem OAI.MatrixMultiplication.Foundation.BalancedSeparation.six_bank_budget line 293
  35. theorem OAI.MatrixMultiplication.Foundation.BalancedSeparation.six_auxiliary_product line 299
  36. def OAI.MatrixMultiplication.Foundation.BalancedSeparation.orientationBankEquiv line 305
  37. theorem OAI.MatrixMultiplication.Foundation.BalancedSeparation.orientationBankEquiv_site line 313
  38. def OAI.MatrixMultiplication.Foundation.BalancedSeparation.orientationCoordinateEquiv line 316
  39. theorem OAI.MatrixMultiplication.Foundation.BalancedSeparation.orientationCoordinateEquiv_tensor line 328
  40. theorem OAI.MatrixMultiplication.Foundation.BalancedSeparation.orientationBankEquiv_grade_card line 338