OAI/LinearAlgebra/MatrixMultiplication/ComplexArithmetic/RecursiveBlockPrograms.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Complex arithmetic programs and asymptotic matrix multiplication costs.

  1. def OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.LinearExpression.sumFin line 21
  2. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.LinearExpression.eval_sumFin line 25
  3. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.LinearExpression.cost_sumFin line 32
  4. def OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.LinearExpression.linear line 40
  5. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.LinearExpression.eval_linear line 46
  6. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.LinearExpression.cost_linear line 52
  7. structure OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family line 59
  8. def OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.eval line 68
  9. def OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.cost line 71
  10. def OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.expressions line 73
  11. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.eval_expressions line 77
  12. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.cost_expressions line 82
  13. def OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.compose line 86
  14. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.eval_compose line 90
  15. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.cost_compose line 95
  16. def OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.mapInputs line 99
  17. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.eval_mapInputs line 103
  18. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.cost_mapInputs line 108
  19. def OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.parallel line 112
  20. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.eval_parallel line 123
  21. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.cost_parallel line 135
  22. def OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.copies line 145
  23. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.eval_copies line 149
  24. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.cost_copies line 154
  25. def OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.ofMatrix line 158
  26. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.cost_ofMatrix line 162
  27. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.eval_ofMatrix line 165
  28. def OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.join line 184
  29. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.rank_bilinear_identity line 186
  30. def OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.leftBlock line 216
  31. def OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.rightBlock line 221
  32. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.block_identity line 226
  33. def OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.inputExpressions line 251
  34. def OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.inputFamily line 258
  35. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.inputFamily_eval line 262
  36. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.inputFamily_cost line 274
  37. def OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.recursiveProducts line 285
  38. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.recursiveProducts_eval line 289
  39. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.recursiveProducts_cost line 298
  40. def OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.outputExpressions line 304
  41. def OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.outputFamily line 310
  42. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.outputFamily_eval line 314
  43. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.outputFamily_cost line 321
  44. def OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.algorithm line 328
  45. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.algorithm_correct line 333
  46. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.algorithm_cost line 348
  47. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.rank_block_step line 355