OAI/LinearAlgebra/MatrixMultiplication/ComplexArithmetic/ProgramComposition.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Complex arithmetic programs and asymptotic matrix multiplication costs.

  1. def OAI.MatrixMultiplication.Foundation.Arithmetic.Gate.mapInput line 15
  2. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.Gate.eval_mapInput line 22
  3. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.Gate.cost_mapInput line 27
  4. def OAI.MatrixMultiplication.Foundation.Arithmetic.Gate.mapSource line 31
  5. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.Gate.eval_mapSource line 40
  6. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.Gate.cost_mapSource line 51
  7. def OAI.MatrixMultiplication.Foundation.Arithmetic.Program.mapInput line 66
  8. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.Program.eval_mapInput line 70
  9. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.Program.cost_mapInput line 82
  10. def OAI.MatrixMultiplication.Foundation.Arithmetic.Program.mapSource line 88
  11. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.Program.eval_mapSource line 92
  12. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.Program.cost_mapSource line 105
  13. structure OAI.MatrixMultiplication.Foundation.Arithmetic.Program.Substituted line 111
  14. def OAI.MatrixMultiplication.Foundation.Arithmetic.Program.Substituted.step line 124
  15. def OAI.MatrixMultiplication.Foundation.Arithmetic.Program.substitute line 148