OAI/LinearAlgebra/MatrixFields/Arithmetic/ComplexArithmeticLowerBound.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Gate line 18
2. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Gate.eval line 29
3. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Gate.cost line 36
4. inductive OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Program line 45
5. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Program.eval line 53
6. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Program.cost line 58
7. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Program.eval_step_zero line 62
8. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Program.eval_step_succ line 66
9. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Program.cost_step line 70
10. abbrev OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.MatrixInput line 75
11. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.matrixInputs line 77
12. structure OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.MatrixAlgorithm line 81
13. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.MatrixAlgorithm.eval line 88
14. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.MatrixAlgorithm.Correct line 92
15. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.MatrixAlgorithm.cost line 95
16. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.MatrixAlgorithm.correct_iff_entries line 97
17. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.scalarAlgorithm line 109
18. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.scalarAlgorithm_correct line 115
19. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.scalarAlgorithm_cost line 125
20. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.AdmissibleExponent line 127
21. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.omega line 132
22. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.matrixMultiplication line 138
23. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.matrixMultiplication_matching line 142
24. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Gate.mapRegister line 160
25. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Gate.eval_mapRegister line 167
26. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Gate.cost_mapRegister line 172
27. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Program.oldIndex line 182
28. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Program.newIndex line 184
29. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Program.oldIndex_zero line 186
30. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Program.oldIndex_succ line 190
31. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Program.newIndex_zero line 196
32. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Program.newIndex_succ line 200
33. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Program.append line 205
34. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Program.eval_append_new line 209
35. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Program.eval_append_old line 221
36. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Program.cost_append line 230
37. inductive OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Expression line 238
38. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Expression.eval line 249
39. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Expression.cost line 256
40. structure OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Expression.Compiled line 263
41. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Expression.compile line 270
42. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Gate.mapInput line 329
43. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Gate.eval_mapInput line 336
44. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Gate.cost_mapInput line 341
45. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Gate.mapSource line 345
46. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Gate.eval_mapSource line 354
47. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Gate.cost_mapSource line 365
48. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Program.mapInput line 380
49. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Program.eval_mapInput line 384
50. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Program.cost_mapInput line 396
51. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Program.mapSource line 402
52. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Program.eval_mapSource line 406
53. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Program.cost_mapSource line 419
54. structure OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Program.Substituted line 425
55. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Program.Substituted.step line 438
56. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Program.substitute line 462
57. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.zeroPadMatrix line 508
58. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.zeroPadMatrix_castLE line 514
59. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.sum_fin_castLE_of_zero line 519
60. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.zeroPadMatrix_mul line 530
61. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.padSource line 547
62. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.padSource_eval line 555
63. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.MatrixAlgorithm.pad line 566
64. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.MatrixAlgorithm.pad_correct line 571
65. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.MatrixAlgorithm.pad_cost_eq line 582
66. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.MatrixAlgorithm.exists_restrict line 586
67. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.Program.eval_eq_constant_or_input_of_cost_eq_zero line 602
68. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.MatrixAlgorithm.one_le_cost line 629
69. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.admissibleExponent_nonneg line 662
70. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.admissibleExponent_bddBelow line 684