OAI/LinearAlgebra/MatrixMultiplication/Rectangular/Growth.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Rectangular matrix multiplication algorithms and their asymptotic exponents.

  1. theorem OAI.MatrixMultiplication.Arithmetic.rectangular_power_cost_padding_bound line 15
  2. theorem OAI.MatrixMultiplication.Arithmetic.rectangularAdmissibleExponent_of_power_costs line 43
  3. def OAI.MatrixMultiplication.Arithmetic.rectangularBlockCost line 54
  4. theorem OAI.MatrixMultiplication.Arithmetic.rectangularBlockCost_zero line 58
  5. theorem OAI.MatrixMultiplication.Arithmetic.rectangularBlockCost_succ line 61
  6. theorem OAI.MatrixMultiplication.Arithmetic.rectangularBlockCost_bound line 65
  7. theorem OAI.MatrixMultiplication.Arithmetic.rectangular_power_programs_of_block_step line 97
  8. theorem OAI.MatrixMultiplication.Arithmetic.rectangularAdmissibleExponent_of_block_step line 118