OAI/LinearAlgebra/MatrixFields/Arithmetic/RecursiveBlockPrograms.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.Gate.mapInput line 22
  2. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.Gate.eval_mapInput line 29
  3. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.Gate.cost_mapInput line 35
  4. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.Gate.mapSource line 39
  5. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.Gate.eval_mapSource line 48
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.Gate.cost_mapSource line 60
  7. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.Program.mapInput line 75
  8. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.Program.eval_mapInput line 79
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.Program.cost_mapInput line 92
  10. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.Program.mapSource line 98
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.Program.eval_mapSource line 102
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.Program.cost_mapSource line 116
  13. structure OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.Program.Substituted line 122
  14. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.Program.Substituted.step line 135
  15. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.Program.substitute line 159
  16. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.zeroPadMatrix line 214
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.zeroPadMatrix_castLE line 220
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.sum_fin_castLE_of_zero line 225
  19. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.zeroPadMatrix_mul line 236
  20. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.padSource line 254
  21. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.padSource_eval line 262
  22. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.MatrixAlgorithm.pad line 275
  23. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.MatrixAlgorithm.pad_correct line 281
  24. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.MatrixAlgorithm.pad_cost_eq line 292
  25. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.MatrixAlgorithm.exists_restrict line 296
  26. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RectangularAdmissibleExponent.mono_aspect line 303
  27. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.LinearExpression.sumFin line 333
  28. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.LinearExpression.eval_sumFin line 337
  29. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.LinearExpression.cost_sumFin line 344
  30. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.LinearExpression.linear line 352
  31. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.LinearExpression.eval_linear line 358
  32. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.LinearExpression.cost_linear line 364
  33. structure OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family line 371
  34. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.eval line 380
  35. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.cost line 383
  36. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.expressions line 385
  37. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.eval_expressions line 389
  38. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.cost_expressions line 394
  39. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.compose line 398
  40. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.eval_compose line 402
  41. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.cost_compose line 407
  42. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.mapInputs line 411
  43. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.eval_mapInputs line 415
  44. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.cost_mapInputs line 421
  45. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.parallel line 425
  46. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.eval_parallel line 436
  47. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.cost_parallel line 449
  48. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.copies line 459
  49. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.eval_copies line 463
  50. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.cost_copies line 469
  51. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.ofMatrix line 473
  52. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.cost_ofMatrix line 478
  53. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.Family.eval_ofMatrix line 481
  54. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.join line 500
  55. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.rank_bilinear_identity line 502
  56. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.leftBlock line 533
  57. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.rightBlock line 538
  58. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.block_identity line 543
  59. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.inputExpressions line 571
  60. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.inputFamily line 580
  61. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.inputFamily_eval line 586
  62. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.inputFamily_cost line 601
  63. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.recursiveProducts line 611
  64. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.recursiveProducts_eval line 617
  65. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.recursiveProducts_cost line 629
  66. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.outputExpressions line 636
  67. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.outputFamily line 642
  68. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.outputFamily_eval line 646
  69. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.outputFamily_cost line 654
  70. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.algorithm line 661
  71. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.algorithm_correct line 668
  72. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.algorithm_cost line 684
  73. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RecursiveBlock.rank_block_step line 693