OAI/LinearAlgebra/MatrixMultiplication/ComplexArithmetic/NaiveAlgorithm.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Complex arithmetic programs and asymptotic matrix multiplication costs.

  1. def OAI.MatrixMultiplication.Foundation.Arithmetic.Expression.sumFin line 18
  2. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.Expression.sumFin_eval line 22
  3. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.Expression.sumFin_cost line 28
  4. def OAI.MatrixMultiplication.Foundation.Arithmetic.naiveEntry line 38
  5. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.naiveEntry_eval line 42
  6. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.naiveEntry_cost line 47
  7. def OAI.MatrixMultiplication.Foundation.Arithmetic.naiveAlgorithm line 51
  8. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.naiveAlgorithm_correct line 57
  9. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.naiveAlgorithm_cost line 65
  10. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.naiveAlgorithm_cost_le line 73
  11. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.admissibleExponent_three line 76
  12. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.admissibleExponent_nonempty line 94