OAI/LinearAlgebra/MatrixMultiplication/Arithmetic/RecursiveBlockPrograms.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

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

  1. def OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.LinearExpression.sumFin line 25
  2. theorem OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.LinearExpression.eval_sumFin line 29
  3. theorem OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.LinearExpression.cost_sumFin line 36
  4. def OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.LinearExpression.linear line 44
  5. theorem OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.LinearExpression.eval_linear line 50
  6. theorem OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.LinearExpression.cost_linear line 56
  7. structure OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.Family line 63
  8. def OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.eval line 72
  9. def OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.cost line 75
  10. def OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.expressions line 77
  11. theorem OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.eval_expressions line 81
  12. theorem OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.cost_expressions line 86
  13. def OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.compose line 90
  14. theorem OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.eval_compose line 94
  15. theorem OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.cost_compose line 99
  16. def OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.mapInputs line 103
  17. theorem OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.eval_mapInputs line 107
  18. theorem OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.cost_mapInputs line 113
  19. def OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.parallel line 117
  20. theorem OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.eval_parallel line 128
  21. theorem OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.cost_parallel line 141
  22. def OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.copies line 151
  23. theorem OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.eval_copies line 155
  24. theorem OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.cost_copies line 161
  25. def OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.ofMatrix line 165
  26. theorem OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.cost_ofMatrix line 170
  27. theorem OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.eval_ofMatrix line 173
  28. def OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.join line 192
  29. theorem OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.rank_bilinear_identity line 194
  30. def OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.leftBlock line 225
  31. def OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.rightBlock line 230
  32. theorem OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.block_identity line 235
  33. def OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.inputExpressions line 263
  34. def OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.inputFamily line 272
  35. theorem OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.inputFamily_eval line 278
  36. theorem OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.inputFamily_cost line 293
  37. def OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.recursiveProducts line 303
  38. theorem OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.recursiveProducts_eval line 309
  39. theorem OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.recursiveProducts_cost line 321
  40. def OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.outputExpressions line 328
  41. def OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.outputFamily line 334
  42. theorem OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.outputFamily_eval line 338
  43. theorem OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.outputFamily_cost line 346
  44. def OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.algorithm line 353
  45. theorem OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.algorithm_correct line 360
  46. theorem OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.algorithm_cost line 376
  47. theorem OAI.MatrixMultiplication.Arithmetic.RecursiveBlock.rank_block_step line 385