OAI/LinearAlgebra/MatrixFields/Construction/OrderedLimits.lean

GitHub source file

126 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialChoice.Choice line 25
2. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialChoice.initial_count_eq line 33
3. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialChoice.eventually_nonempty line 50
4. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialChoice.Tags line 64
5. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialChoice.card_tags line 69
6. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialChoice.execution line 76
7. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialChoice.execution_copies line 85
8. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminal.terminalProductMap line 114
9. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminal.terminalExecution line 122
10. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminal.terminalExecution_copies line 131
11. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminal.finish line 135
12. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminal.finish_multiplicity line 141
13. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminal.finish_volume line 147
14. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminal.finish_rankBound line 157
15. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialZeroFinish.Index line 186
16. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialZeroFinish.shape_total line 190
17. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialZeroFinish.has_zero line 193
18. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialZeroFinish.canonical_axes_ne line 196
19. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialZeroFinish.zero line 201
20. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialZeroFinish.selected line 202
21. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialZeroFinish.axes_ne line 204
22. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialZeroFinish.weights_sum line 207
23. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialZeroFinish.physical_shape_eq line 211
24. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialZeroFinish.embed line 222
25. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialZeroFinish.coefficient line 226
26. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialZeroFinish.RowIndex line 239
27. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialZeroFinish.MiddleIndex line 240
28. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialZeroFinish.ColumnIndex line 241
29. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialZeroFinish.factorMap line 243
30. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialZeroFinish.factor_volume line 252
31. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialZeroFinish.RawWords line 259
32. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialZeroFinish.Rows line 261
33. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialZeroFinish.Middles line 262
34. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialZeroFinish.Columns line 263
35. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialZeroFinish.source line 265
36. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialZeroFinish.finishMap line 271
37. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialZeroFinish.volume_eq line 284
38. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialZeroFinish.volume_pos line 296
39. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialZeroFinish.rows_pos line 303
40. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialZeroFinish.middles_pos line 306
41. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialZeroFinish.columns_pos line 309
42. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCRegroup.Positions line 336
43. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCRegroup.PairedWords line 339
44. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCRegroup.SplitWords line 342
45. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCRegroup.unpair line 345
46. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCRegroup.pair line 352
47. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCRegroup.pair_unpair line 357
48. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCRegroup.unpair_pair line 363
49. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCRegroup.unpairEquiv line 369
50. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCRegroup.splitTensor line 379
51. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCRegroup.pairedTensor line 384
52. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCRegroup.prod_fin_cast line 389
53. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCRegroup.pullback_unpair line 394
54. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCFinish.localMapWithFintypes_inline_MatrixMultiplication_AllFieldStageCFinish line 443
55. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCFinish.pairLocalMap line 454
56. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCFinish.shapeFactorMap line 471
57. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCFinish.shapeHistoryMap line 478
58. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCFinish.row_nonempty line 505
59. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCFinish.middle_nonempty line 509
60. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCFinish.column_nonempty line 513
61. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCFinish.Index line 519
62. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCFinish.RawWords line 521
63. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCFinish.source line 524
64. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCFinish.counts line 530
65. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCFinish.counts_half line 533
66. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCFinish.counts_false line 537
67. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCFinish.SingleWord line 540
68. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCFinish.leaf line 542
69. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCFinish.GroupedWords line 546
70. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCFinish.PairedWords line 549
71. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCFinish.groupedSource line 552
72. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCFinish.pairedSource line 555
73. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCFinish.indexEquiv line 562
74. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCFinish.toRaw line 568
75. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCFinish.regroup_coefficient line 571
76. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCFinish.regroupMap line 585
77. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCFinish.leaf_pair line 596
78. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCFinish.pairedSource_eq line 603
79. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCFinish.pairMap line 617
80. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCFinish.Rows line 634
81. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCFinish.Middles line 635
82. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCFinish.Columns line 636
83. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCFinish.terminalMap line 638
84. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCFinish.finishMap line 647
85. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCFinish.volume_eq_populationVolume line 654
86. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCFinish.rows_pos line 662
87. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCFinish.middles_pos line 666
88. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCFinish.columns_pos line 670
89. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinishedWitness.localMapWithFintypes_inline_MatrixMultiplication_AllFieldFinishedWitness line 695
90. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinishedWitness.matrixProductMap line 706
91. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinishedWitness.combineMatrixMaps line 720
92. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinishedWitness.ZeroRows line 733
93. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinishedWitness.ZeroMiddles line 734
94. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinishedWitness.ZeroColumns line 735
95. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinishedWitness.Rows line 737
96. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinishedWitness.Middles line 740
97. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinishedWitness.Columns line 743
98. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinishedWitness.zero_volume line 816
99. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinishedWitness.volume_eq line 824
100. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinishedWitness.dimensions_pos line 842
101. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinishedWitness.zeroMap line 852
102. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinishedWitness.terminalMap line 871
103. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinishedWitness.execution line 897
104. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinishedWitness.witness line 910
105. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinishedWitness.witness_volume line 919
106. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinishedWitness.witness_multiplicity line 927
107. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinishedWitness.witness_rankBound line 934
108. structure OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionData.Data line 964
109. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionData.Tags line 973
110. instance OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionData.tagsFintype line 977
111. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionData.execution line 980
112. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionData.card_tags line 989
113. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionData.execution_copies line 1002
114. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionData.tags_pos line 1012
115. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionData.witness line 1023
116. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionData.witness_volume line 1033
117. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionData.witness_multiplicity line 1043
118. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionData.witness_rankBound line 1055
119. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionFamily.exists_width_eventually_data line 1095
120. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionFamily.yieldRate line 1129
121. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionFamily.exists_family line 1134
122. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionFamily.fixed_prescription_constraint line 1176
123. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldConstructionFamily.fixed_allocation_constraint line 1185
124. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldOrderedLimits.fixed_lot_constraint line 1219
125. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldOrderedLimits.native_rank_constraint line 1248
126. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldOrderedLimits.omega_le_native_ratio line 1263