OAI/LinearAlgebra/MatrixFields/Arithmetic/ComplexArithmeticGrowth.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.LinearExpression.sumFin line 21
2. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.LinearExpression.eval_sumFin line 25
3. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.LinearExpression.cost_sumFin line 32
4. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.LinearExpression.linear line 40
5. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.LinearExpression.eval_linear line 46
6. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.LinearExpression.cost_linear line 52
7. structure OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family line 59
8. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.eval line 68
9. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.cost line 71
10. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.expressions line 73
11. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.eval_expressions line 77
12. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.cost_expressions line 82
13. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.compose line 86
14. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.eval_compose line 90
15. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.cost_compose line 95
16. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.mapInputs line 99
17. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.eval_mapInputs line 103
18. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.cost_mapInputs line 108
19. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.parallel line 112
20. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.eval_parallel line 123
21. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.cost_parallel line 135
22. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.copies line 145
23. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.eval_copies line 149
24. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.cost_copies line 154
25. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.ofMatrix line 158
26. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.cost_ofMatrix line 162
27. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.Family.eval_ofMatrix line 165
28. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.join line 184
29. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.rank_bilinear_identity line 186
30. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.leftBlock line 216
31. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.rightBlock line 221
32. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.block_identity line 226
33. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.inputExpressions line 249
34. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.inputFamily line 256
35. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.inputFamily_eval line 260
36. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.inputFamily_cost line 272
37. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.recursiveProducts line 283
38. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.recursiveProducts_eval line 287
39. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.recursiveProducts_cost line 296
40. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.outputExpressions line 302
41. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.outputFamily line 308
42. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.outputFamily_eval line 312
43. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.outputFamily_cost line 319
44. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.algorithm line 326
45. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.algorithm_correct line 331
46. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.algorithm_cost line 346
47. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.RecursiveBlock.rank_block_step line 353
48. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.exists_power_cover line 368
49. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.geometric_cost_recurrence_bound line 374
50. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.power_cost_padding_bound line 407
51. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.admissibleExponent_of_uniform_power_costs line 434
52. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.admissibleExponent_of_power_costs line 450
53. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.admissibleExponent_of_recursive_costs line 462
54. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.blockRecurrenceCost line 492
55. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.blockRecurrenceCost_zero line 496
56. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.blockRecurrenceCost_succ line 499
57. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.power_programs_of_block_step line 503
58. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.admissibleExponent_of_block_step_of_padding line 522
59. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.admissibleExponent_of_block_step line 553
60. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.admissibleExponent_of_rankAtMost line 563