OAI/LinearAlgebra/MatrixMultiplication/FieldConstruction/FinishedWitness.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Tensor extraction over arbitrary fields and its asymptotic rate.

  1. def OAI.MatrixMultiplication.AllFieldFinishedWitness.localMapWithFintypes line 21
  2. def OAI.MatrixMultiplication.AllFieldFinishedWitness.matrixProductMap line 32
  3. def OAI.MatrixMultiplication.AllFieldFinishedWitness.combineMatrixMaps line 46
  4. abbrev OAI.MatrixMultiplication.AllFieldFinishedWitness.ZeroRows line 59
  5. abbrev OAI.MatrixMultiplication.AllFieldFinishedWitness.ZeroMiddles line 60
  6. abbrev OAI.MatrixMultiplication.AllFieldFinishedWitness.ZeroColumns line 61
  7. abbrev OAI.MatrixMultiplication.AllFieldFinishedWitness.Rows line 63
  8. abbrev OAI.MatrixMultiplication.AllFieldFinishedWitness.Middles line 66
  9. abbrev OAI.MatrixMultiplication.AllFieldFinishedWitness.Columns line 69
  10. theorem OAI.MatrixMultiplication.AllFieldFinishedWitness.zero_volume line 142
  11. theorem OAI.MatrixMultiplication.AllFieldFinishedWitness.volume_eq line 150
  12. theorem OAI.MatrixMultiplication.AllFieldFinishedWitness.dimensions_pos line 168
  13. def OAI.MatrixMultiplication.AllFieldFinishedWitness.zeroMap line 178
  14. def OAI.MatrixMultiplication.AllFieldFinishedWitness.terminalMap line 197
  15. def OAI.MatrixMultiplication.AllFieldFinishedWitness.execution line 223
  16. def OAI.MatrixMultiplication.AllFieldFinishedWitness.witness line 236
  17. theorem OAI.MatrixMultiplication.AllFieldFinishedWitness.witness_volume line 245
  18. theorem OAI.MatrixMultiplication.AllFieldFinishedWitness.witness_multiplicity line 253
  19. theorem OAI.MatrixMultiplication.AllFieldFinishedWitness.witness_rankBound line 260