OAI/LinearAlgebra/MatrixMultiplication/ComplexArithmetic/Programs.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Complex arithmetic programs and asymptotic matrix multiplication costs.

  1. def OAI.MatrixMultiplication.Foundation.Arithmetic.Gate.mapRegister line 16
  2. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.Gate.eval_mapRegister line 23
  3. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.Gate.cost_mapRegister line 28
  4. def OAI.MatrixMultiplication.Foundation.Arithmetic.Program.oldIndex line 38
  5. def OAI.MatrixMultiplication.Foundation.Arithmetic.Program.newIndex line 40
  6. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.Program.oldIndex_zero line 42
  7. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.Program.oldIndex_succ line 46
  8. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.Program.newIndex_zero line 52
  9. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.Program.newIndex_succ line 56
  10. def OAI.MatrixMultiplication.Foundation.Arithmetic.Program.append line 61
  11. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.Program.eval_append_new line 65
  12. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.Program.eval_append_old line 77
  13. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.Program.cost_append line 86
  14. inductive OAI.MatrixMultiplication.Foundation.Arithmetic.Expression line 94
  15. def OAI.MatrixMultiplication.Foundation.Arithmetic.Expression.eval line 105
  16. def OAI.MatrixMultiplication.Foundation.Arithmetic.Expression.cost line 112
  17. structure OAI.MatrixMultiplication.Foundation.Arithmetic.Expression.Compiled line 119
  18. def OAI.MatrixMultiplication.Foundation.Arithmetic.Expression.compile line 126