OAI/LinearAlgebra/MatrixFields/Certificates/Four0_5_3.lean

GitHub source file

161 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3Raw line 16
2. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3Raw_sound_0 line 55
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3Raw_sound_1 line 82
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3Raw_sound_2 line 109
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3Raw_sound_3 line 136
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3Raw_sound_4 line 163
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3Raw_sound_5 line 190
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3Raw_sound line 217
9. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3Den line 222
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3Den_sound line 223
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3Den_pos line 228
12. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3Probs line 229
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3Contains line 238
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3Zero line 242
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3Probs_sound line 245
16. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3Half line 255
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3Half_sound line 259
18. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3Value line 286
19. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3E_1_5LogWitness line 287
20. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3E_1_5Log line 288
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3E_1_5Log_sound line 289
22. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3E_1_5 line 293
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3E_1_5_sound line 294
24. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3E_2_4LogWitness line 296
25. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3E_2_4Log line 297
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3E_2_4Log_sound line 298
27. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3E_2_4 line 302
28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3E_2_4_sound line 303
29. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3E_3_4LogWitness line 305
30. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3E_3_4Log line 306
31. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3E_3_4Log_sound line 307
32. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3E_3_4 line 311
33. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3E_3_4_sound line 312
34. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3E_4_2LogWitness line 314
35. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3E_4_2Log line 315
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3E_4_2Log_sound line 316
37. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3E_4_2 line 320
38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3E_4_2_sound line 321
39. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3E_4_3LogWitness line 323
40. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3E_4_3Log line 324
41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3E_4_3Log_sound line 325
42. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3E_4_3 line 329
43. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3E_4_3_sound line 330
44. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3E_5_1LogWitness line 332
45. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3E_5_1Log line 333
46. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3E_5_1Log_sound line 334
47. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3E_5_1 line 338
48. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3E_5_1_sound line 339
49. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3Terms line 341
50. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3Terms_sound line 350
51. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3Entropy line 361
52. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3Entropy_sound line 362
53. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3Labels line 364
54. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3Labels_sound line 365
55. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3Four line 370
56. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3Four_sound line 371
57. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H0Value line 373
58. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H0E_0_0Log line 374
59. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H0E_0_0Log_sound line 375
60. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H0E_0_0 line 377
61. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H0E_0_0_sound line 378
62. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H0Terms line 380
63. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H0Terms_sound line 384
64. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H0Entropy line 395
65. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H0Entropy_sound line 396
66. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H0Mass line 398
67. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H0Mass_sound line 399
68. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H0MassTermLog line 401
69. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H0MassTermLog_sound line 402
70. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H0MassTerm line 404
71. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H0MassTerm_sound line 405
72. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H0H line 407
73. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H0H_sound line 408
74. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1Value line 410
75. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1E_1_5LogWitness line 411
76. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1E_1_5Log line 412
77. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1E_1_5Log_sound line 413
78. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1E_1_5 line 417
79. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1E_1_5_sound line 418
80. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1E_2_4LogWitness line 420
81. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1E_2_4Log line 421
82. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1E_2_4Log_sound line 422
83. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1E_2_4 line 426
84. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1E_2_4_sound line 427
85. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1E_3_4LogWitness line 429
86. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1E_3_4Log line 430
87. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1E_3_4Log_sound line 431
88. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1E_3_4 line 435
89. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1E_3_4_sound line 436
90. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1E_4_2LogWitness line 438
91. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1E_4_2Log line 439
92. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1E_4_2Log_sound line 440
93. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1E_4_2 line 444
94. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1E_4_2_sound line 445
95. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1E_4_3LogWitness line 447
96. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1E_4_3Log line 448
97. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1E_4_3Log_sound line 449
98. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1E_4_3 line 453
99. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1E_4_3_sound line 454
100. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1E_5_1LogWitness line 456
101. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1E_5_1Log line 457
102. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1E_5_1Log_sound line 458
103. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1E_5_1 line 462
104. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1E_5_1_sound line 463
105. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1Terms line 465
106. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1Terms_sound line 474
107. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1Entropy line 485
108. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1Entropy_sound line 486
109. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1Mass line 488
110. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1Mass_sound line 489
111. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1MassTermLogWitness line 491
112. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1MassTermLog line 492
113. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1MassTermLog_sound line 493
114. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1MassTerm line 497
115. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1MassTerm_sound line 498
116. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1H line 500
117. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H1H_sound line 501
118. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2Value line 503
119. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2E_4_0LogWitness line 504
120. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2E_4_0Log line 505
121. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2E_4_0Log_sound line 506
122. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2E_4_0 line 510
123. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2E_4_0_sound line 511
124. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2E_2_1LogWitness line 513
125. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2E_2_1Log line 514
126. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2E_2_1Log_sound line 515
127. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2E_2_1 line 519
128. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2E_2_1_sound line 520
129. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2E_3_1LogWitness line 522
130. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2E_3_1Log line 523
131. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2E_3_1Log_sound line 524
132. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2E_3_1 line 528
133. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2E_3_1_sound line 529
134. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2E_1_2LogWitness line 531
135. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2E_1_2Log line 532
136. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2E_1_2Log_sound line 533
137. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2E_1_2 line 537
138. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2E_1_2_sound line 538
139. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2E_1_3LogWitness line 540
140. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2E_1_3Log line 541
141. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2E_1_3Log_sound line 542
142. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2E_1_3 line 546
143. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2E_1_3_sound line 547
144. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2E_0_4LogWitness line 549
145. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2E_0_4Log line 550
146. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2E_0_4Log_sound line 551
147. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2E_0_4 line 555
148. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2E_0_4_sound line 556
149. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2Terms line 558
150. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2Terms_sound line 567
151. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2Entropy line 578
152. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2Entropy_sound line 579
153. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2Mass line 581
154. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2Mass_sound line 582
155. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2MassTermLogWitness line 584
156. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2MassTermLog line 585
157. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2MassTermLog_sound line 586
158. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2MassTerm line 590
159. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2MassTerm_sound line 591
160. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2H line 593
161. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z0_5_3H2H_sound line 594