OAI/LinearAlgebra/MatrixFields/Certificates/NativeInterior.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1_below line 53
2. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Raw line 58
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Raw_2_1_1 line 65
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Raw_3_0_1 line 69
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Raw_3_1_0 line 73
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Raw_4_0_0 line 77
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Raw_sound line 81
8. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Den line 90
9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Den_sound line 91
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Den_positive line 93
11. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Table line 94
12. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Law line 101
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Law_check_2_1_1 line 102
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Law_check_3_0_1 line 103
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Law_check_3_1_0 line 104
16. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Law_check_4_0_0 line 105
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Law_check line 106
18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Law_sound line 115
19. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Binary line 142
20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Binary_eq line 146
21. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1LittleRat line 166
22. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Little line 171
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Little_sound line 175
24. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Half line 183
25. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Half_check_0_0 line 195
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Half_check_0_1 line 199
27. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Half_check_0_2 line 203
28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Half_check_0_3 line 207
29. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Half_check_0_4 line 211
30. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Half_check_0_5 line 215
31. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Half_check_1_0 line 219
32. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Half_check_1_1 line 223
33. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Half_check_1_2 line 227
34. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Half_check_1_3 line 231
35. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Half_check_1_4 line 235
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Half_check_1_5 line 239
37. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Half_check_2_0 line 243
38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Half_check_2_1 line 247
39. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Half_check_2_2 line 251
40. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Half_check_2_3 line 255
41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Half_check_2_4 line 259
42. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Half_check_2_5 line 263
43. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Half_sound line 267
44. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1U2_1_1D line 302
45. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1U2_1_1D_sound line 303
46. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1U2_1_1OneD line 306
47. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1U2_1_1OneD_sound line 307
48. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1U2_1_1EDLogWitness line 311
49. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1U2_1_1EDLog line 312
50. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1U2_1_1EDLog_sound line 313
51. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1U2_1_1ED line 317
52. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1U2_1_1ED_sound line 318
53. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1U2_1_1EOneDLogWitness line 320
54. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1U2_1_1EOneDLog line 321
55. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1U2_1_1EOneDLog_sound line 322
56. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1U2_1_1EOneD line 326
57. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1U2_1_1EOneD_sound line 327
58. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1U2_1_1BinaryEntropy line 329
59. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1U2_1_1BinaryEntropy_sound line 330
60. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1U2_1_1Leaf line 334
61. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1U2_1_1Leaf_sound line 335
62. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1U2_1_1Mass line 346
63. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1U2_1_1Mass_sound line 347
64. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1U3_0_1Leaf line 352
65. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1U3_0_1Leaf_sound line 353
66. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1U3_0_1Mass line 357
67. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1U3_0_1Mass_sound line 358
68. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1U3_1_0Leaf line 363
69. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1U3_1_0Leaf_sound line 364
70. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1U3_1_0Mass line 368
71. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1U3_1_0Mass_sound line 369
72. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1U4_0_0Leaf line 374
73. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1U4_0_0Leaf_sound line 375
74. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1U4_0_0Mass line 379
75. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1U4_0_0Mass_sound line 380
76. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Leaves line 385
77. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Leaves_sound line 392
78. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Masses line 401
79. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Masses_sound line 408
80. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Binaries line 417
81. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Binaries_sound line 421
82. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1S2 line 428
83. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1S2_sound line 429
84. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.fourRateBalls line 453
85. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.fourRateBalls_sound line 480
86. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.nativeS1Ball line 509
87. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.nativeS1Ball_sound line 510
88. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.s2ParentBalls line 515
89. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.s2ParentBalls_sound line 539
90. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.nativeS2Ball line 566
91. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.nativeS2Ball_sound line 567
92. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.nativeSBall line 570
93. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.nativeSBall_sound line 571
94. theorem OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.native_volume_positive line 575
95. theorem OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.nativeS1_strict_bounds line 580
96. theorem OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.nativeS2_strict_bounds line 585
97. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.interior_fold line 608
98. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_1_6Ttotal line 619
99. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_1_6Ttotal_sound line 620
100. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_1_6Btotal line 624
101. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_1_6Btotal_sound line 625
102. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Ttotal line 632
103. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Ttotal_sound line 633
104. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Btotal line 637
105. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Btotal_sound line 638
106. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4Ttotal line 645
107. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4Ttotal_sound line 646
108. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4Btotal line 650
109. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4Btotal_sound line 651
110. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3Ttotal line 658
111. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3Ttotal_sound line 659
112. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3Btotal line 663
113. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_4_3Btotal_sound line 664
114. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2Ttotal line 671
115. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2Ttotal_sound line 672
116. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2Btotal line 676
117. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_5_2Btotal_sound line 677
118. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Ttotal line 684
119. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Ttotal_sound line 685
120. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Btotal line 689
121. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Btotal_sound line 690
122. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Ttotal line 697
123. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Ttotal_sound line 698
124. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Btotal line 702
125. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Btotal_sound line 703
126. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Ttotal line 710
127. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Ttotal_sound line 711
128. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Btotal line 715
129. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_2_4Btotal_sound line 716
130. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3Ttotal line 723
131. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3Ttotal_sound line 724
132. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3Btotal line 728
133. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_3_3Btotal_sound line 729
134. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Ttotal line 736
135. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Ttotal_sound line 737
136. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Btotal line 741
137. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_4_2Btotal_sound line 742
138. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1Ttotal line 749
139. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1Ttotal_sound line 750
140. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1Btotal line 754
141. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_5_1Btotal_sound line 755
142. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Ttotal line 762
143. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Ttotal_sound line 763
144. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Btotal line 767
145. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Btotal_sound line 768
146. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3Ttotal line 775
147. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3Ttotal_sound line 776
148. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3Btotal line 780
149. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3Btotal_sound line 781
150. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_3_2Ttotal line 788
151. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_3_2Ttotal_sound line 789
152. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_3_2Btotal line 793
153. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_3_2Btotal_sound line 794
154. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Ttotal line 801
155. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Ttotal_sound line 802
156. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Btotal line 806
157. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Btotal_sound line 807
158. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Ttotal line 814
159. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Ttotal_sound line 815
160. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Btotal line 819
161. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Btotal_sound line 820
162. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Ttotal line 827
163. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Ttotal_sound line 828
164. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Btotal line 832
165. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_2_2Btotal_sound line 833
166. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Ttotal line 840
167. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Ttotal_sound line 841
168. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Btotal line 845
169. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Btotal_sound line 846
170. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2Ttotal line 853
171. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2Ttotal_sound line 854
172. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2Btotal line 858
173. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2Btotal_sound line 859
174. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Ttotal line 866
175. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Ttotal_sound line 867
176. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Btotal line 871
177. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Btotal_sound line 872
178. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Ttotal line 879
179. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Ttotal_sound line 880
180. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Btotal line 884
181. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B6_1_1Btotal_sound line 885
182. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.TParentBalls line 892
183. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.TParentBalls_sound line 916
184. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.BParentBalls line 943
185. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.BParentBalls_sound line 967
186. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.nativeTBall line 994
187. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.nativeTBall_sound line 995
188. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.nativeBBall line 999
189. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.nativeBBall_sound line 1000
190. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.nativeHighBall line 1009
191. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.nativeHighBall_sound line 1010
192. theorem OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.native_denominator_gap line 1013