OAI/LinearAlgebra/MatrixMultiplication/Arithmetic/Exponent.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

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

  1. theorem OAI.MatrixMultiplication.Arithmetic.AdmissibleExponent.mono line 15
  2. theorem OAI.MatrixMultiplication.Arithmetic.omega_two_le line 27
  3. theorem OAI.MatrixMultiplication.Arithmetic.omega_nonneg line 30
  4. theorem OAI.MatrixMultiplication.Arithmetic.omega_le_three line 32
  5. theorem OAI.MatrixMultiplication.Arithmetic.omega_admissibleExponent line 35
  6. theorem OAI.MatrixMultiplication.Arithmetic.admissibleExponent_iff_omega_le line 49
  7. theorem OAI.MatrixMultiplication.Arithmetic.RectangularAdmissibleExponent.mono line 53
  8. theorem OAI.MatrixMultiplication.Arithmetic.rectangularAdmissibleExponent_of_uniform_costs line 66
  9. theorem OAI.MatrixMultiplication.Arithmetic.rectangularAdmissibleExponent_naive line 79
  10. theorem OAI.MatrixMultiplication.Arithmetic.rectangularAdmissibleExponent_nonempty line 100
  11. theorem OAI.MatrixMultiplication.Arithmetic.rectangularOmega_two_le line 104
  12. theorem OAI.MatrixMultiplication.Arithmetic.rectangularOmega_admissibleExponent line 108
  13. theorem OAI.MatrixMultiplication.Arithmetic.rectangularAdmissibleExponent_iff_omega_le line 123
  14. theorem OAI.MatrixMultiplication.Arithmetic.rectangularOmega_mono line 127
  15. theorem OAI.MatrixMultiplication.Arithmetic.rectangularOmega_zero line 132
  16. theorem OAI.MatrixMultiplication.Arithmetic.complexAlpha_set_nonempty line 137
  17. theorem OAI.MatrixMultiplication.Arithmetic.complexAlpha_set_bddAbove line 141
  18. theorem OAI.MatrixMultiplication.Arithmetic.le_complexAlpha line 145
  19. theorem OAI.MatrixMultiplication.Arithmetic.complexAlpha_le_one line 149
  20. theorem OAI.MatrixMultiplication.Arithmetic.complexAlpha_nonneg line 152