OAI/LinearAlgebra/MatrixFields/Certificates/Four1_7_0.lean

GitHub source file

99 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0Raw line 15
2. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0Raw_sound_0 line 54
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0Raw_sound_1 line 81
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0Raw_sound_2 line 108
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0Raw_sound_3 line 135
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0Raw_sound_4 line 162
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0Raw_sound_5 line 189
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0Raw_sound line 216
9. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0Den line 221
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0Den_sound line 222
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0Den_pos line 227
12. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0Probs line 228
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0Contains line 233
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0Zero line 237
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0Probs_sound line 240
16. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0Half line 250
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0Half_sound line 254
18. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0Value line 264
19. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0E_4_5LogWitness line 265
20. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0E_4_5Log line 266
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0E_4_5Log_sound line 267
22. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0E_4_5 line 271
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0E_4_5_sound line 272
24. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0E_5_4LogWitness line 274
25. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0E_5_4Log line 275
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0E_5_4Log_sound line 276
27. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0E_5_4 line 280
28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0E_5_4_sound line 281
29. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0Terms line 283
30. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0Terms_sound line 288
31. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0Entropy line 299
32. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0Entropy_sound line 300
33. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0Labels line 302
34. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0Labels_sound line 303
35. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0Four line 308
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0Four_sound line 309
37. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H0Value line 311
38. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H0E_1_0LogWitness line 312
39. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H0E_1_0Log line 313
40. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H0E_1_0Log_sound line 314
41. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H0E_1_0 line 318
42. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H0E_1_0_sound line 319
43. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H0E_0_1LogWitness line 321
44. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H0E_0_1Log line 322
45. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H0E_0_1Log_sound line 323
46. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H0E_0_1 line 327
47. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H0E_0_1_sound line 328
48. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H0Terms line 330
49. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H0Terms_sound line 335
50. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H0Entropy line 346
51. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H0Entropy_sound line 347
52. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H0Mass line 349
53. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H0Mass_sound line 350
54. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H0MassTermLog line 352
55. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H0MassTermLog_sound line 353
56. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H0MassTerm line 355
57. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H0MassTerm_sound line 356
58. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H0H line 358
59. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H0H_sound line 359
60. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H1Value line 361
61. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H1E_4_5LogWitness line 362
62. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H1E_4_5Log line 363
63. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H1E_4_5Log_sound line 364
64. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H1E_4_5 line 368
65. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H1E_4_5_sound line 369
66. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H1E_5_4LogWitness line 371
67. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H1E_5_4Log line 372
68. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H1E_5_4Log_sound line 373
69. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H1E_5_4 line 377
70. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H1E_5_4_sound line 378
71. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H1Terms line 380
72. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H1Terms_sound line 385
73. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H1Entropy line 396
74. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H1Entropy_sound line 397
75. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H1Mass line 399
76. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H1Mass_sound line 400
77. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H1MassTermLog line 402
78. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H1MassTermLog_sound line 403
79. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H1MassTerm line 405
80. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H1MassTerm_sound line 406
81. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H1H line 408
82. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H1H_sound line 409
83. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H2Value line 411
84. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H2E_0_0Log line 412
85. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H2E_0_0Log_sound line 413
86. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H2E_0_0 line 415
87. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H2E_0_0_sound line 416
88. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H2Terms line 418
89. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H2Terms_sound line 422
90. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H2Entropy line 433
91. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H2Entropy_sound line 434
92. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H2Mass line 436
93. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H2Mass_sound line 437
94. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H2MassTermLog line 439
95. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H2MassTermLog_sound line 440
96. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H2MassTerm line 442
97. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H2MassTerm_sound line 443
98. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H2H line 445
99. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z1_7_0H2H_sound line 446