OAI/LinearAlgebra/MatrixMultiplication/Arithmetic/LowerBound.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Division-free arithmetic programs over a field and their operation counts.

  1. def OAI.MatrixMultiplication.Arithmetic.Program.registerCost line 20
  2. theorem OAI.MatrixMultiplication.Arithmetic.Program.sum_registerCost line 24
  3. theorem OAI.MatrixMultiplication.Arithmetic.Program.eval_eq_constant_or_input_of_registerCost_eq_zero line 30
  4. def OAI.MatrixMultiplication.Arithmetic.elementaryLeft line 58
  5. def OAI.MatrixMultiplication.Arithmetic.elementaryRight line 61
  6. theorem OAI.MatrixMultiplication.Arithmetic.elementaryProduct line 64
  7. theorem OAI.MatrixMultiplication.Arithmetic.MatrixAlgorithm.output_injective line 76
  8. theorem OAI.MatrixMultiplication.Arithmetic.MatrixAlgorithm.one_le_output_registerCost line 96
  9. theorem OAI.MatrixMultiplication.Arithmetic.MatrixAlgorithm.output_size_le_cost line 124
  10. theorem OAI.MatrixMultiplication.Arithmetic.rectangularAdmissibleExponent_two_le line 144
  11. theorem OAI.MatrixMultiplication.Arithmetic.rectangularAdmissibleExponent_bddBelow line 174
  12. theorem OAI.MatrixMultiplication.Arithmetic.rectangularOmega_le_of_admissibleExponent line 178
  13. theorem OAI.MatrixMultiplication.Arithmetic.admissibleExponent_iff_rectangular_one line 182
  14. theorem OAI.MatrixMultiplication.Arithmetic.admissibleExponent_two_le line 199
  15. theorem OAI.MatrixMultiplication.Arithmetic.admissibleExponent_bddBelow line 203
  16. theorem OAI.MatrixMultiplication.Arithmetic.omega_le_of_admissibleExponent line 207
  17. theorem OAI.MatrixMultiplication.Arithmetic.rectangularOmega_one line 211