OAI/LinearAlgebra/MatrixMultiplication/ComplexArithmetic/Complexity.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Complex arithmetic programs and asymptotic matrix multiplication costs.

  1. inductive OAI.MatrixMultiplication.Foundation.Arithmetic.Gate line 17
  2. def OAI.MatrixMultiplication.Foundation.Arithmetic.Gate.eval line 28
  3. def OAI.MatrixMultiplication.Foundation.Arithmetic.Gate.cost line 35
  4. inductive OAI.MatrixMultiplication.Foundation.Arithmetic.Program line 44
  5. def OAI.MatrixMultiplication.Foundation.Arithmetic.Program.eval line 52
  6. def OAI.MatrixMultiplication.Foundation.Arithmetic.Program.cost line 57
  7. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.Program.eval_step_zero line 61
  8. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.Program.eval_step_succ line 65
  9. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.Program.cost_step line 69
  10. abbrev OAI.MatrixMultiplication.Foundation.Arithmetic.MatrixInput line 74
  11. def OAI.MatrixMultiplication.Foundation.Arithmetic.matrixInputs line 76
  12. structure OAI.MatrixMultiplication.Foundation.Arithmetic.MatrixAlgorithm line 80
  13. def OAI.MatrixMultiplication.Foundation.Arithmetic.MatrixAlgorithm.eval line 87
  14. def OAI.MatrixMultiplication.Foundation.Arithmetic.MatrixAlgorithm.Correct line 91
  15. def OAI.MatrixMultiplication.Foundation.Arithmetic.MatrixAlgorithm.cost line 94
  16. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.MatrixAlgorithm.correct_iff_entries line 96
  17. def OAI.MatrixMultiplication.Foundation.Arithmetic.scalarAlgorithm line 108
  18. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.scalarAlgorithm_correct line 114
  19. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.scalarAlgorithm_cost line 124
  20. def OAI.MatrixMultiplication.Foundation.Arithmetic.AdmissibleExponent line 126
  21. def OAI.MatrixMultiplication.Foundation.Arithmetic.omega line 131
  22. def OAI.MatrixMultiplication.Foundation.Tensor.matrixMultiplication line 137
  23. theorem OAI.MatrixMultiplication.Foundation.Tensor.matrixMultiplication_matching line 141