OAI/LinearAlgebra/MatrixFields/Certificates/SparseContraction.lean

GitHub source file

303 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.exponentialCoefficients line 17
2. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.exponential_polynomial_cast line 20
3. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weight_enclosed_of_trace line 29
4. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightTrace0 line 53
5. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare0_1 line 71
6. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare0_2 line 72
7. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare0_3 line 73
8. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare0_4 line 74
9. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare0_5 line 75
10. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare0_6 line 76
11. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weight_enclosed_0 line 77
12. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightTrace1 line 81
13. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare1_1 line 99
14. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare1_2 line 100
15. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare1_3 line 101
16. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare1_4 line 102
17. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare1_5 line 103
18. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare1_6 line 104
19. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weight_enclosed_1 line 105
20. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightTrace2 line 109
21. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare2_1 line 127
22. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare2_2 line 128
23. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare2_3 line 129
24. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare2_4 line 130
25. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare2_5 line 131
26. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare2_6 line 132
27. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weight_enclosed_2 line 133
28. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightTrace3 line 137
29. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare3_1 line 155
30. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare3_2 line 156
31. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare3_3 line 157
32. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare3_4 line 158
33. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare3_5 line 159
34. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare3_6 line 160
35. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weight_enclosed_3 line 161
36. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightTrace4 line 165
37. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare4_1 line 183
38. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare4_2 line 184
39. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare4_3 line 185
40. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare4_4 line 186
41. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare4_5 line 187
42. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare4_6 line 188
43. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weight_enclosed_4 line 189
44. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightTrace5 line 193
45. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare5_1 line 211
46. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare5_2 line 212
47. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare5_3 line 213
48. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare5_4 line 214
49. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare5_5 line 215
50. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare5_6 line 216
51. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weight_enclosed_5 line 217
52. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightTrace6 line 221
53. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare6_1 line 239
54. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare6_2 line 240
55. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare6_3 line 241
56. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare6_4 line 242
57. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare6_5 line 243
58. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare6_6 line 244
59. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weight_enclosed_6 line 245
60. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightTrace7 line 249
61. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare7_1 line 267
62. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare7_2 line 268
63. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare7_3 line 269
64. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare7_4 line 270
65. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare7_5 line 271
66. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare7_6 line 272
67. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weight_enclosed_7 line 273
68. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightTrace8 line 277
69. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare8_1 line 295
70. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare8_2 line 296
71. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare8_3 line 297
72. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare8_4 line 298
73. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare8_5 line 299
74. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare8_6 line 300
75. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weight_enclosed_8 line 301
76. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightTrace9 line 305
77. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare9_1 line 323
78. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare9_2 line 324
79. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare9_3 line 325
80. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare9_4 line 326
81. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare9_5 line 327
82. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare9_6 line 328
83. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weight_enclosed_9 line 329
84. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightTrace10 line 333
85. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare10_1 line 351
86. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare10_2 line 352
87. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare10_3 line 353
88. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare10_4 line 354
89. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare10_5 line 355
90. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare10_6 line 356
91. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weight_enclosed_10 line 357
92. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightTrace11 line 361
93. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare11_1 line 379
94. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare11_2 line 380
95. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare11_3 line 381
96. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare11_4 line 382
97. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare11_5 line 383
98. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare11_6 line 384
99. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weight_enclosed_11 line 385
100. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightTrace12 line 389
101. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare12_1 line 407
102. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare12_2 line 408
103. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare12_3 line 409
104. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare12_4 line 410
105. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare12_5 line 411
106. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare12_6 line 412
107. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weight_enclosed_12 line 413
108. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightTrace13 line 417
109. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare13_1 line 435
110. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare13_2 line 436
111. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare13_3 line 437
112. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare13_4 line 438
113. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare13_5 line 439
114. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare13_6 line 440
115. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weight_enclosed_13 line 441
116. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightTrace14 line 445
117. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare14_1 line 463
118. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare14_2 line 464
119. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare14_3 line 465
120. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare14_4 line 466
121. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare14_5 line 467
122. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare14_6 line 468
123. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weight_enclosed_14 line 469
124. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightTrace15 line 473
125. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare15_1 line 491
126. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare15_2 line 492
127. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare15_3 line 493
128. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare15_4 line 494
129. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare15_5 line 495
130. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare15_6 line 496
131. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weight_enclosed_15 line 497
132. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightTrace16 line 501
133. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare16_1 line 519
134. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare16_2 line 520
135. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare16_3 line 521
136. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare16_4 line 522
137. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare16_5 line 523
138. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightSquare16_6 line 524
139. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weight_enclosed_16 line 525
140. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightBall line 529
141. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.weightBall_sound line 531
142. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.sourceWeightBall line 552
143. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.sourceWeightBall_sound line 554
144. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.listSumBall line 558
145. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.listSumBall_sound line 561
146. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.finSumBall line 570
147. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.finSumBall_sound line 574
148. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.initialRawBall line 583
149. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.initial_shape_bound line 588
150. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.initialRawBall_sound line 591
151. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.initialDenominatorBall line 601
152. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.initialDenominatorBall_sound line 603
153. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.initialDenominatorBall_positive line 610
154. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.initialLawBall line 613
155. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.initialLawBall_sound line 616
156. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.initialMarginalBall line 623
157. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.initialMarginalBall_sound line 628
158. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.roundedMarginal line 638
159. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.marginal_containment_0 line 640
160. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.marginal_containment_1 line 643
161. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.marginal_containment_2 line 646
162. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.marginal_containment_3 line 649
163. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.marginal_containment_4 line 652
164. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.marginal_containment_5 line 655
165. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.marginal_containment_6 line 658
166. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.marginal_containment_7 line 661
167. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.marginal_containment_8 line 664
168. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.marginal_containment_9 line 667
169. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.marginal_containment_10 line 670
170. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.marginal_containment_11 line 673
171. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.marginal_containment_12 line 676
172. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.marginal_containment_13 line 679
173. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.marginal_containment_14 line 682
174. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.marginal_containment_15 line 685
175. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.marginal_containment_16 line 688
176. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.roundedMarginal_sound line 691
177. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.logTwoTrace line 713
178. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.logTwoBall line 738
179. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.logTwoBall_sound line 739
180. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.marginalLogWitness line 743
181. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.marginalLogBall line 744
182. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.marginalLogBall_sound line 745
183. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.totalMarginalBall line 750
184. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.totalMarginalBall_sound line 751
185. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.totalLogWitness line 756
186. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.totalLogBall line 757
187. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.totalLogBall_sound line 758
188. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.entropySumBall line 763
189. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.entropySumBall_sound line 766
190. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.initialEntropyRawBall line 777
191. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.initialEntropyRawBall_sound line 780
192. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.initialEntropyBall line 784
193. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.nativeH0_enclosed line 785
194. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialEntropyCertificate.nativeH0_strict_bounds line 787
195. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.zeroLeafShape line 813
196. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.zeroLeafCoefficient line 814
197. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.zeroLeafShape_mem line 817
198. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.initialZeroShapes line 821
199. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.nativeS0_eq_sum line 825
200. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.leafLogWitness0 line 830
201. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.leafRateBall0 line 831
202. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.leafRateBall0_sound line 832
203. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.leafLogWitness1 line 841
204. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.leafRateBall1 line 842
205. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.leafRateBall1_sound line 843
206. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.leafLogWitness2 line 852
207. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.leafRateBall2 line 853
208. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.leafRateBall2_sound line 854
209. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.leafLogWitness3 line 863
210. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.leafRateBall3 line 864
211. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.leafRateBall3_sound line 865
212. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.leafLogWitness4 line 874
213. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.leafRateBall4 line 875
214. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.leafRateBall4_sound line 876
215. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.leafLogWitness5 line 885
216. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.leafRateBall5 line 886
217. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.leafRateBall5_sound line 887
218. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.leafLogWitness6 line 896
219. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.leafRateBall6 line 897
220. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.leafRateBall6_sound line 898
221. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.leafLogWitness7 line 907
222. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.leafRateBall7 line 908
223. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.leafRateBall7_sound line 909
224. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.leafLogWitness8 line 918
225. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.leafRateBall8 line 919
226. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.leafRateBall8_sound line 920
227. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.leafRateBall line 929
228. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.leafRateBall_sound line 930
229. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.initialVolumeRawBall line 942
230. lemma OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.initialVolumeRawBall_sound line 945
231. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.initialVolumeBall line 951
232. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.nativeS0_enclosed line 952
233. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldVolumeCertificate.nativeS0_strict_bounds line 954
234. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.splitWeight_three_enclosed line 977
235. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.list_cast_enclosed line 987
236. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.product_fin6_enclosed line 993
237. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.entropyTerm_ball line 999
238. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.entropyTerm_zero_ball line 1004
239. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.log_exact_one_ball line 1011
240. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.forall_fin6 line 1036
241. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.forall_fin3 line 1041
242. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.exact_rat_enclosed line 1045
243. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.pairSumBall line 1049
244. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.pairSumBall_sound line 1052
245. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.doublePairSumBall line 1057
246. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.doublePairSumBall_sound line 1060
247. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.entropyFin_enclosed line 1066
248. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.entropyPair_enclosed line 1071
249. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.entropyDoublePair_enclosed line 1076
250. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.homogeneous_enclosed line 1082
251. instance OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.designatedDecidable line 1089
252. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.marginalBall line 1094
253. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.marginalBall_sound line 1097
254. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.pairLawBall line 1106
255. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.pairLawBall_sound line 1110
256. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.pairLawBall_sound_on line 1119
257. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.residualBall line 1130
258. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.residualBall_sound line 1137
259. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.residualBall_sound_on line 1150
260. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.singletonBall line 1163
261. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.singletonBall_sound line 1168
262. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.logN1 line 1199
263. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.logN1_sound line 1200
264. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.logN2Witness line 1202
265. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.logN2 line 1203
266. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.logN2_sound line 1204
267. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.logN4Witness line 1208
268. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.logN4 line 1209
269. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.logN4_sound line 1210
270. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.logN5Witness line 1214
271. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.logN5 line 1215
272. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.logN5_sound line 1216
273. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.logN7Witness line 1220
274. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.logN7 line 1221
275. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.logN7_sound line 1222
276. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.logN10Witness line 1226
277. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.logN10 line 1227
278. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.logN10_sound line 1228
279. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.logN20Witness line 1232
280. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.logN20 line 1233
281. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.logN20_sound line 1234
282. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.logN25Witness line 1238
283. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.logN25 line 1239
284. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.logN25_sound line 1240
285. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.logN50Witness line 1244
286. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.logN50 line 1245
287. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.logN50_sound line 1246
288. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.logN100Witness line 1250
289. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.logN100 line 1251
290. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.logN100_sound line 1252
291. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.logN250Witness line 1256
292. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.logN250 line 1257
293. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.logN250_sound line 1258
294. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.logN625Witness line 1262
295. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.logN625 line 1263
296. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.logN625_sound line 1264
297. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.multLogs line 1268
298. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.multLogs_sound line 1307
299. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.sparseTripleBall line 1481
300. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.sparseTripleBall_eq line 1484
301. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.sparsePairLawBall line 1499
302. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.sparsePairLawBall_eq line 1503
303. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.sparsePairLawBall_sound_on line 1508