OAI/Analysis/PlanarPacking/BasisIntervals.lean

GitHub source file

418 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpPlanar.IntegerBasis.phase12 line 8
2. lemma OAI.SharpPlanar.IntegerBasis.phase12_eq_pow line 9
3. lemma OAI.SharpPlanar.IntegerBasis.phase12_periodic line 14
4. lemma OAI.SharpPlanar.IntegerBasis.phase12_mod line 19
5. def OAI.SharpPlanar.IntegerBasis.phaseBase line 22
6. lemma OAI.SharpPlanar.IntegerBasis.phaseBase_contains line 23
7. def OAI.SharpPlanar.IntegerBasis.phaseBox line 33
8. lemma OAI.SharpPlanar.IntegerBasis.phaseBox_contains line 34
9. def OAI.SharpPlanar.IntegerBasis.coefficientBox line 39
10. lemma OAI.SharpPlanar.IntegerBasis.coefficientBox_contains line 48
11. def OAI.SharpPlanar.IntegerBasis.spectralCoefficient line 72
12. def OAI.SharpPlanar.IntegerBasis.spectralCoefficientBox line 74
13. lemma OAI.SharpPlanar.IntegerBasis.spectralCoefficientBox_contains line 75
14. def OAI.SharpPlanar.IntegerIntervals.zeroBox line 89
15. lemma OAI.SharpPlanar.IntegerIntervals.zeroBox_contains line 90
16. def OAI.SharpPlanar.IntegerIntervals.boxSum line 91
17. lemma OAI.SharpPlanar.IntegerIntervals.boxSum_contains line 94
18. def OAI.SharpPlanar.IntegerBasis.basisAlpha line 107
19. def OAI.SharpPlanar.IntegerBasis.basisBeta line 108
20. def OAI.SharpPlanar.IntegerBasis.alphaBox line 111
21. def OAI.SharpPlanar.IntegerBasis.betaBox line 113
22. lemma OAI.SharpPlanar.IntegerBasis.sum_seven_Icc line 115
23. lemma OAI.SharpPlanar.IntegerBasis.alphaBox_contains line 122
24. lemma OAI.SharpPlanar.IntegerBasis.betaBox_contains line 128
25. lemma OAI.SharpPlanar.IntegerBasis.u_factored line 137
26. lemma OAI.SharpPlanar.IntegerBasis.v_factored line 146
27. def OAI.SharpPlanar.IntegerIntervals.CBox.powFast line 155
28. lemma OAI.SharpPlanar.IntegerIntervals.CBox.contains_powFast line 162
29. lemma OAI.SharpPlanar.IntegerBasis.spectralCoefficient_eq_phase line 190
30. lemma OAI.SharpPlanar.IntegerBasis.spectralCoefficient_mod line 196
31. lemma OAI.SharpPlanar.IntegerBasis.basisAlpha_mod line 202
32. lemma OAI.SharpPlanar.IntegerBasis.basisBeta_mod line 205
33. def OAI.SharpPlanar.IntegerBasis.uBox line 209
34. def OAI.SharpPlanar.IntegerBasis.vBox line 212
35. lemma OAI.SharpPlanar.IntegerBasis.direct_power_contains line 214
36. lemma OAI.SharpPlanar.IntegerBasis.uBox_contains line 222
37. lemma OAI.SharpPlanar.IntegerBasis.vBox_contains line 234
38. lemma OAI.SharpPlanar.IntegerBasis.pointLambda_eq line 246
39. lemma OAI.SharpPlanar.IntegerBasis.pointZ_eq line 250
40. def OAI.SharpPlanar.IntegerBasis.kernel0Box line 255
41. lemma OAI.SharpPlanar.IntegerBasis.kernel0Box_contains line 256
42. def OAI.SharpPlanar.IntegerBasis.basisFunction line 269
43. def OAI.SharpPlanar.IntegerBasis.basisMoment line 271
44. def OAI.SharpPlanar.IntegerBasis.basisFunctionBox line 274
45. def OAI.SharpPlanar.IntegerBasis.basisMomentBox line 276
46. lemma OAI.SharpPlanar.IntegerBasis.basisFunctionBox_contains line 279
47. lemma OAI.SharpPlanar.IntegerBasis.basisMomentBox_contains line 286
48. def OAI.SharpPlanar.IntegerIntervals.finSum line 301
49. lemma OAI.SharpPlanar.IntegerIntervals.finSum_contains line 304
50. lemma OAI.SharpPlanar.IntegerBasis.sum_fin_square line 317
51. def OAI.SharpPlanar.IntegerBasis.momentRuleValue line 330
52. def OAI.SharpPlanar.IntegerBasis.momentRuleBox line 335
53. lemma OAI.SharpPlanar.IntegerBasis.momentRuleBox_contains line 341
54. def OAI.SharpPlanar.IntegerAlpha.a0_0 line 364
55. lemma OAI.SharpPlanar.IntegerAlpha.a0_0_contains line 365
56. def OAI.SharpPlanar.IntegerAlpha.b0_0 line 369
57. lemma OAI.SharpPlanar.IntegerAlpha.b0_0_contains line 370
58. def OAI.SharpPlanar.IntegerAlpha.a0_1 line 374
59. lemma OAI.SharpPlanar.IntegerAlpha.a0_1_contains line 375
60. def OAI.SharpPlanar.IntegerAlpha.b0_1 line 379
61. lemma OAI.SharpPlanar.IntegerAlpha.b0_1_contains line 380
62. def OAI.SharpPlanar.IntegerAlpha.a0_2 line 384
63. lemma OAI.SharpPlanar.IntegerAlpha.a0_2_contains line 385
64. def OAI.SharpPlanar.IntegerAlpha.b0_2 line 389
65. lemma OAI.SharpPlanar.IntegerAlpha.b0_2_contains line 390
66. def OAI.SharpPlanar.IntegerAlpha.a0_3 line 394
67. lemma OAI.SharpPlanar.IntegerAlpha.a0_3_contains line 395
68. def OAI.SharpPlanar.IntegerAlpha.b0_3 line 399
69. lemma OAI.SharpPlanar.IntegerAlpha.b0_3_contains line 400
70. def OAI.SharpPlanar.IntegerAlpha.a0_4 line 404
71. lemma OAI.SharpPlanar.IntegerAlpha.a0_4_contains line 405
72. def OAI.SharpPlanar.IntegerAlpha.b0_4 line 409
73. lemma OAI.SharpPlanar.IntegerAlpha.b0_4_contains line 410
74. def OAI.SharpPlanar.IntegerAlpha.a0_5 line 414
75. lemma OAI.SharpPlanar.IntegerAlpha.a0_5_contains line 415
76. def OAI.SharpPlanar.IntegerAlpha.b0_5 line 419
77. lemma OAI.SharpPlanar.IntegerAlpha.b0_5_contains line 420
78. def OAI.SharpPlanar.IntegerAlpha.aRow0 line 424
79. lemma OAI.SharpPlanar.IntegerAlpha.aRow0_contains line 425
80. def OAI.SharpPlanar.IntegerAlpha.bRow0 line 433
81. lemma OAI.SharpPlanar.IntegerAlpha.bRow0_contains line 434
82. def OAI.SharpPlanar.IntegerAlpha.a1_0 line 442
83. lemma OAI.SharpPlanar.IntegerAlpha.a1_0_contains line 443
84. def OAI.SharpPlanar.IntegerAlpha.b1_0 line 447
85. lemma OAI.SharpPlanar.IntegerAlpha.b1_0_contains line 448
86. def OAI.SharpPlanar.IntegerAlpha.a1_1 line 452
87. lemma OAI.SharpPlanar.IntegerAlpha.a1_1_contains line 453
88. def OAI.SharpPlanar.IntegerAlpha.b1_1 line 457
89. lemma OAI.SharpPlanar.IntegerAlpha.b1_1_contains line 458
90. def OAI.SharpPlanar.IntegerAlpha.a1_2 line 462
91. lemma OAI.SharpPlanar.IntegerAlpha.a1_2_contains line 463
92. def OAI.SharpPlanar.IntegerAlpha.b1_2 line 467
93. lemma OAI.SharpPlanar.IntegerAlpha.b1_2_contains line 468
94. def OAI.SharpPlanar.IntegerAlpha.a1_3 line 472
95. lemma OAI.SharpPlanar.IntegerAlpha.a1_3_contains line 473
96. def OAI.SharpPlanar.IntegerAlpha.b1_3 line 477
97. lemma OAI.SharpPlanar.IntegerAlpha.b1_3_contains line 478
98. def OAI.SharpPlanar.IntegerAlpha.a1_4 line 482
99. lemma OAI.SharpPlanar.IntegerAlpha.a1_4_contains line 483
100. def OAI.SharpPlanar.IntegerAlpha.b1_4 line 487
101. lemma OAI.SharpPlanar.IntegerAlpha.b1_4_contains line 488
102. def OAI.SharpPlanar.IntegerAlpha.a1_5 line 492
103. lemma OAI.SharpPlanar.IntegerAlpha.a1_5_contains line 493
104. def OAI.SharpPlanar.IntegerAlpha.b1_5 line 497
105. lemma OAI.SharpPlanar.IntegerAlpha.b1_5_contains line 498
106. def OAI.SharpPlanar.IntegerAlpha.aRow1 line 502
107. lemma OAI.SharpPlanar.IntegerAlpha.aRow1_contains line 503
108. def OAI.SharpPlanar.IntegerAlpha.bRow1 line 511
109. lemma OAI.SharpPlanar.IntegerAlpha.bRow1_contains line 512
110. def OAI.SharpPlanar.IntegerAlpha.a2_0 line 520
111. lemma OAI.SharpPlanar.IntegerAlpha.a2_0_contains line 521
112. def OAI.SharpPlanar.IntegerAlpha.b2_0 line 525
113. lemma OAI.SharpPlanar.IntegerAlpha.b2_0_contains line 526
114. def OAI.SharpPlanar.IntegerAlpha.a2_1 line 530
115. lemma OAI.SharpPlanar.IntegerAlpha.a2_1_contains line 531
116. def OAI.SharpPlanar.IntegerAlpha.b2_1 line 535
117. lemma OAI.SharpPlanar.IntegerAlpha.b2_1_contains line 536
118. def OAI.SharpPlanar.IntegerAlpha.a2_2 line 540
119. lemma OAI.SharpPlanar.IntegerAlpha.a2_2_contains line 541
120. def OAI.SharpPlanar.IntegerAlpha.b2_2 line 545
121. lemma OAI.SharpPlanar.IntegerAlpha.b2_2_contains line 546
122. def OAI.SharpPlanar.IntegerAlpha.a2_3 line 550
123. lemma OAI.SharpPlanar.IntegerAlpha.a2_3_contains line 551
124. def OAI.SharpPlanar.IntegerAlpha.b2_3 line 555
125. lemma OAI.SharpPlanar.IntegerAlpha.b2_3_contains line 556
126. def OAI.SharpPlanar.IntegerAlpha.a2_4 line 560
127. lemma OAI.SharpPlanar.IntegerAlpha.a2_4_contains line 561
128. def OAI.SharpPlanar.IntegerAlpha.b2_4 line 565
129. lemma OAI.SharpPlanar.IntegerAlpha.b2_4_contains line 566
130. def OAI.SharpPlanar.IntegerAlpha.a2_5 line 570
131. lemma OAI.SharpPlanar.IntegerAlpha.a2_5_contains line 571
132. def OAI.SharpPlanar.IntegerAlpha.b2_5 line 575
133. lemma OAI.SharpPlanar.IntegerAlpha.b2_5_contains line 576
134. def OAI.SharpPlanar.IntegerAlpha.aRow2 line 580
135. lemma OAI.SharpPlanar.IntegerAlpha.aRow2_contains line 581
136. def OAI.SharpPlanar.IntegerAlpha.bRow2 line 589
137. lemma OAI.SharpPlanar.IntegerAlpha.bRow2_contains line 590
138. def OAI.SharpPlanar.IntegerAlpha.a3_0 line 598
139. lemma OAI.SharpPlanar.IntegerAlpha.a3_0_contains line 599
140. def OAI.SharpPlanar.IntegerAlpha.b3_0 line 603
141. lemma OAI.SharpPlanar.IntegerAlpha.b3_0_contains line 604
142. def OAI.SharpPlanar.IntegerAlpha.a3_1 line 608
143. lemma OAI.SharpPlanar.IntegerAlpha.a3_1_contains line 609
144. def OAI.SharpPlanar.IntegerAlpha.b3_1 line 613
145. lemma OAI.SharpPlanar.IntegerAlpha.b3_1_contains line 614
146. def OAI.SharpPlanar.IntegerAlpha.a3_2 line 618
147. lemma OAI.SharpPlanar.IntegerAlpha.a3_2_contains line 619
148. def OAI.SharpPlanar.IntegerAlpha.b3_2 line 623
149. lemma OAI.SharpPlanar.IntegerAlpha.b3_2_contains line 624
150. def OAI.SharpPlanar.IntegerAlpha.a3_3 line 628
151. lemma OAI.SharpPlanar.IntegerAlpha.a3_3_contains line 629
152. def OAI.SharpPlanar.IntegerAlpha.b3_3 line 633
153. lemma OAI.SharpPlanar.IntegerAlpha.b3_3_contains line 634
154. def OAI.SharpPlanar.IntegerAlpha.a3_4 line 638
155. lemma OAI.SharpPlanar.IntegerAlpha.a3_4_contains line 639
156. def OAI.SharpPlanar.IntegerAlpha.b3_4 line 643
157. lemma OAI.SharpPlanar.IntegerAlpha.b3_4_contains line 644
158. def OAI.SharpPlanar.IntegerAlpha.a3_5 line 648
159. lemma OAI.SharpPlanar.IntegerAlpha.a3_5_contains line 649
160. def OAI.SharpPlanar.IntegerAlpha.b3_5 line 653
161. lemma OAI.SharpPlanar.IntegerAlpha.b3_5_contains line 654
162. def OAI.SharpPlanar.IntegerAlpha.aRow3 line 658
163. lemma OAI.SharpPlanar.IntegerAlpha.aRow3_contains line 659
164. def OAI.SharpPlanar.IntegerAlpha.bRow3 line 667
165. lemma OAI.SharpPlanar.IntegerAlpha.bRow3_contains line 668
166. def OAI.SharpPlanar.IntegerAlpha.a4_0 line 676
167. lemma OAI.SharpPlanar.IntegerAlpha.a4_0_contains line 677
168. def OAI.SharpPlanar.IntegerAlpha.b4_0 line 681
169. lemma OAI.SharpPlanar.IntegerAlpha.b4_0_contains line 682
170. def OAI.SharpPlanar.IntegerAlpha.a4_1 line 686
171. lemma OAI.SharpPlanar.IntegerAlpha.a4_1_contains line 687
172. def OAI.SharpPlanar.IntegerAlpha.b4_1 line 691
173. lemma OAI.SharpPlanar.IntegerAlpha.b4_1_contains line 692
174. def OAI.SharpPlanar.IntegerAlpha.a4_2 line 696
175. lemma OAI.SharpPlanar.IntegerAlpha.a4_2_contains line 697
176. def OAI.SharpPlanar.IntegerAlpha.b4_2 line 701
177. lemma OAI.SharpPlanar.IntegerAlpha.b4_2_contains line 702
178. def OAI.SharpPlanar.IntegerAlpha.a4_3 line 706
179. lemma OAI.SharpPlanar.IntegerAlpha.a4_3_contains line 707
180. def OAI.SharpPlanar.IntegerAlpha.b4_3 line 711
181. lemma OAI.SharpPlanar.IntegerAlpha.b4_3_contains line 712
182. def OAI.SharpPlanar.IntegerAlpha.a4_4 line 716
183. lemma OAI.SharpPlanar.IntegerAlpha.a4_4_contains line 717
184. def OAI.SharpPlanar.IntegerAlpha.b4_4 line 721
185. lemma OAI.SharpPlanar.IntegerAlpha.b4_4_contains line 722
186. def OAI.SharpPlanar.IntegerAlpha.a4_5 line 726
187. lemma OAI.SharpPlanar.IntegerAlpha.a4_5_contains line 727
188. def OAI.SharpPlanar.IntegerAlpha.b4_5 line 731
189. lemma OAI.SharpPlanar.IntegerAlpha.b4_5_contains line 732
190. def OAI.SharpPlanar.IntegerAlpha.aRow4 line 736
191. lemma OAI.SharpPlanar.IntegerAlpha.aRow4_contains line 737
192. def OAI.SharpPlanar.IntegerAlpha.bRow4 line 745
193. lemma OAI.SharpPlanar.IntegerAlpha.bRow4_contains line 746
194. def OAI.SharpPlanar.IntegerAlpha.a5_0 line 754
195. lemma OAI.SharpPlanar.IntegerAlpha.a5_0_contains line 755
196. def OAI.SharpPlanar.IntegerAlpha.b5_0 line 759
197. lemma OAI.SharpPlanar.IntegerAlpha.b5_0_contains line 760
198. def OAI.SharpPlanar.IntegerAlpha.a5_1 line 764
199. lemma OAI.SharpPlanar.IntegerAlpha.a5_1_contains line 765
200. def OAI.SharpPlanar.IntegerAlpha.b5_1 line 769
201. lemma OAI.SharpPlanar.IntegerAlpha.b5_1_contains line 770
202. def OAI.SharpPlanar.IntegerAlpha.a5_2 line 774
203. lemma OAI.SharpPlanar.IntegerAlpha.a5_2_contains line 775
204. def OAI.SharpPlanar.IntegerAlpha.b5_2 line 779
205. lemma OAI.SharpPlanar.IntegerAlpha.b5_2_contains line 780
206. def OAI.SharpPlanar.IntegerAlpha.a5_3 line 784
207. lemma OAI.SharpPlanar.IntegerAlpha.a5_3_contains line 785
208. def OAI.SharpPlanar.IntegerAlpha.b5_3 line 789
209. lemma OAI.SharpPlanar.IntegerAlpha.b5_3_contains line 790
210. def OAI.SharpPlanar.IntegerAlpha.a5_4 line 794
211. lemma OAI.SharpPlanar.IntegerAlpha.a5_4_contains line 795
212. def OAI.SharpPlanar.IntegerAlpha.b5_4 line 799
213. lemma OAI.SharpPlanar.IntegerAlpha.b5_4_contains line 800
214. def OAI.SharpPlanar.IntegerAlpha.a5_5 line 804
215. lemma OAI.SharpPlanar.IntegerAlpha.a5_5_contains line 805
216. def OAI.SharpPlanar.IntegerAlpha.b5_5 line 809
217. lemma OAI.SharpPlanar.IntegerAlpha.b5_5_contains line 810
218. def OAI.SharpPlanar.IntegerAlpha.aRow5 line 814
219. lemma OAI.SharpPlanar.IntegerAlpha.aRow5_contains line 815
220. def OAI.SharpPlanar.IntegerAlpha.bRow5 line 823
221. lemma OAI.SharpPlanar.IntegerAlpha.bRow5_contains line 824
222. def OAI.SharpPlanar.IntegerAlpha.a6_0 line 832
223. lemma OAI.SharpPlanar.IntegerAlpha.a6_0_contains line 833
224. def OAI.SharpPlanar.IntegerAlpha.b6_0 line 837
225. lemma OAI.SharpPlanar.IntegerAlpha.b6_0_contains line 838
226. def OAI.SharpPlanar.IntegerAlpha.a6_1 line 842
227. lemma OAI.SharpPlanar.IntegerAlpha.a6_1_contains line 843
228. def OAI.SharpPlanar.IntegerAlpha.b6_1 line 847
229. lemma OAI.SharpPlanar.IntegerAlpha.b6_1_contains line 848
230. def OAI.SharpPlanar.IntegerAlpha.a6_2 line 852
231. lemma OAI.SharpPlanar.IntegerAlpha.a6_2_contains line 853
232. def OAI.SharpPlanar.IntegerAlpha.b6_2 line 857
233. lemma OAI.SharpPlanar.IntegerAlpha.b6_2_contains line 858
234. def OAI.SharpPlanar.IntegerAlpha.a6_3 line 862
235. lemma OAI.SharpPlanar.IntegerAlpha.a6_3_contains line 863
236. def OAI.SharpPlanar.IntegerAlpha.b6_3 line 867
237. lemma OAI.SharpPlanar.IntegerAlpha.b6_3_contains line 868
238. def OAI.SharpPlanar.IntegerAlpha.a6_4 line 872
239. lemma OAI.SharpPlanar.IntegerAlpha.a6_4_contains line 873
240. def OAI.SharpPlanar.IntegerAlpha.b6_4 line 877
241. lemma OAI.SharpPlanar.IntegerAlpha.b6_4_contains line 878
242. def OAI.SharpPlanar.IntegerAlpha.a6_5 line 882
243. lemma OAI.SharpPlanar.IntegerAlpha.a6_5_contains line 883
244. def OAI.SharpPlanar.IntegerAlpha.b6_5 line 887
245. lemma OAI.SharpPlanar.IntegerAlpha.b6_5_contains line 888
246. def OAI.SharpPlanar.IntegerAlpha.aRow6 line 892
247. lemma OAI.SharpPlanar.IntegerAlpha.aRow6_contains line 893
248. def OAI.SharpPlanar.IntegerAlpha.bRow6 line 901
249. lemma OAI.SharpPlanar.IntegerAlpha.bRow6_contains line 902
250. def OAI.SharpPlanar.IntegerAlpha.a7_0 line 910
251. lemma OAI.SharpPlanar.IntegerAlpha.a7_0_contains line 911
252. def OAI.SharpPlanar.IntegerAlpha.b7_0 line 915
253. lemma OAI.SharpPlanar.IntegerAlpha.b7_0_contains line 916
254. def OAI.SharpPlanar.IntegerAlpha.a7_1 line 920
255. lemma OAI.SharpPlanar.IntegerAlpha.a7_1_contains line 921
256. def OAI.SharpPlanar.IntegerAlpha.b7_1 line 925
257. lemma OAI.SharpPlanar.IntegerAlpha.b7_1_contains line 926
258. def OAI.SharpPlanar.IntegerAlpha.a7_2 line 930
259. lemma OAI.SharpPlanar.IntegerAlpha.a7_2_contains line 931
260. def OAI.SharpPlanar.IntegerAlpha.b7_2 line 935
261. lemma OAI.SharpPlanar.IntegerAlpha.b7_2_contains line 936
262. def OAI.SharpPlanar.IntegerAlpha.a7_3 line 940
263. lemma OAI.SharpPlanar.IntegerAlpha.a7_3_contains line 941
264. def OAI.SharpPlanar.IntegerAlpha.b7_3 line 945
265. lemma OAI.SharpPlanar.IntegerAlpha.b7_3_contains line 946
266. def OAI.SharpPlanar.IntegerAlpha.a7_4 line 950
267. lemma OAI.SharpPlanar.IntegerAlpha.a7_4_contains line 951
268. def OAI.SharpPlanar.IntegerAlpha.b7_4 line 955
269. lemma OAI.SharpPlanar.IntegerAlpha.b7_4_contains line 956
270. def OAI.SharpPlanar.IntegerAlpha.a7_5 line 960
271. lemma OAI.SharpPlanar.IntegerAlpha.a7_5_contains line 961
272. def OAI.SharpPlanar.IntegerAlpha.b7_5 line 965
273. lemma OAI.SharpPlanar.IntegerAlpha.b7_5_contains line 966
274. def OAI.SharpPlanar.IntegerAlpha.aRow7 line 970
275. lemma OAI.SharpPlanar.IntegerAlpha.aRow7_contains line 971
276. def OAI.SharpPlanar.IntegerAlpha.bRow7 line 979
277. lemma OAI.SharpPlanar.IntegerAlpha.bRow7_contains line 980
278. def OAI.SharpPlanar.IntegerAlpha.a8_0 line 988
279. lemma OAI.SharpPlanar.IntegerAlpha.a8_0_contains line 989
280. def OAI.SharpPlanar.IntegerAlpha.b8_0 line 993
281. lemma OAI.SharpPlanar.IntegerAlpha.b8_0_contains line 994
282. def OAI.SharpPlanar.IntegerAlpha.a8_1 line 998
283. lemma OAI.SharpPlanar.IntegerAlpha.a8_1_contains line 999
284. def OAI.SharpPlanar.IntegerAlpha.b8_1 line 1003
285. lemma OAI.SharpPlanar.IntegerAlpha.b8_1_contains line 1004
286. def OAI.SharpPlanar.IntegerAlpha.a8_2 line 1008
287. lemma OAI.SharpPlanar.IntegerAlpha.a8_2_contains line 1009
288. def OAI.SharpPlanar.IntegerAlpha.b8_2 line 1013
289. lemma OAI.SharpPlanar.IntegerAlpha.b8_2_contains line 1014
290. def OAI.SharpPlanar.IntegerAlpha.a8_3 line 1018
291. lemma OAI.SharpPlanar.IntegerAlpha.a8_3_contains line 1019
292. def OAI.SharpPlanar.IntegerAlpha.b8_3 line 1023
293. lemma OAI.SharpPlanar.IntegerAlpha.b8_3_contains line 1024
294. def OAI.SharpPlanar.IntegerAlpha.a8_4 line 1028
295. lemma OAI.SharpPlanar.IntegerAlpha.a8_4_contains line 1029
296. def OAI.SharpPlanar.IntegerAlpha.b8_4 line 1033
297. lemma OAI.SharpPlanar.IntegerAlpha.b8_4_contains line 1034
298. def OAI.SharpPlanar.IntegerAlpha.a8_5 line 1038
299. lemma OAI.SharpPlanar.IntegerAlpha.a8_5_contains line 1039
300. def OAI.SharpPlanar.IntegerAlpha.b8_5 line 1043
301. lemma OAI.SharpPlanar.IntegerAlpha.b8_5_contains line 1044
302. def OAI.SharpPlanar.IntegerAlpha.aRow8 line 1048
303. lemma OAI.SharpPlanar.IntegerAlpha.aRow8_contains line 1049
304. def OAI.SharpPlanar.IntegerAlpha.bRow8 line 1057
305. lemma OAI.SharpPlanar.IntegerAlpha.bRow8_contains line 1058
306. def OAI.SharpPlanar.IntegerAlpha.a9_0 line 1066
307. lemma OAI.SharpPlanar.IntegerAlpha.a9_0_contains line 1067
308. def OAI.SharpPlanar.IntegerAlpha.b9_0 line 1071
309. lemma OAI.SharpPlanar.IntegerAlpha.b9_0_contains line 1072
310. def OAI.SharpPlanar.IntegerAlpha.a9_1 line 1076
311. lemma OAI.SharpPlanar.IntegerAlpha.a9_1_contains line 1077
312. def OAI.SharpPlanar.IntegerAlpha.b9_1 line 1081
313. lemma OAI.SharpPlanar.IntegerAlpha.b9_1_contains line 1082
314. def OAI.SharpPlanar.IntegerAlpha.a9_2 line 1086
315. lemma OAI.SharpPlanar.IntegerAlpha.a9_2_contains line 1087
316. def OAI.SharpPlanar.IntegerAlpha.b9_2 line 1091
317. lemma OAI.SharpPlanar.IntegerAlpha.b9_2_contains line 1092
318. def OAI.SharpPlanar.IntegerAlpha.a9_3 line 1096
319. lemma OAI.SharpPlanar.IntegerAlpha.a9_3_contains line 1097
320. def OAI.SharpPlanar.IntegerAlpha.b9_3 line 1101
321. lemma OAI.SharpPlanar.IntegerAlpha.b9_3_contains line 1102
322. def OAI.SharpPlanar.IntegerAlpha.a9_4 line 1106
323. lemma OAI.SharpPlanar.IntegerAlpha.a9_4_contains line 1107
324. def OAI.SharpPlanar.IntegerAlpha.b9_4 line 1111
325. lemma OAI.SharpPlanar.IntegerAlpha.b9_4_contains line 1112
326. def OAI.SharpPlanar.IntegerAlpha.a9_5 line 1116
327. lemma OAI.SharpPlanar.IntegerAlpha.a9_5_contains line 1117
328. def OAI.SharpPlanar.IntegerAlpha.b9_5 line 1121
329. lemma OAI.SharpPlanar.IntegerAlpha.b9_5_contains line 1122
330. def OAI.SharpPlanar.IntegerAlpha.aRow9 line 1126
331. lemma OAI.SharpPlanar.IntegerAlpha.aRow9_contains line 1127
332. def OAI.SharpPlanar.IntegerAlpha.bRow9 line 1135
333. lemma OAI.SharpPlanar.IntegerAlpha.bRow9_contains line 1136
334. def OAI.SharpPlanar.IntegerAlpha.a10_0 line 1144
335. lemma OAI.SharpPlanar.IntegerAlpha.a10_0_contains line 1145
336. def OAI.SharpPlanar.IntegerAlpha.b10_0 line 1149
337. lemma OAI.SharpPlanar.IntegerAlpha.b10_0_contains line 1150
338. def OAI.SharpPlanar.IntegerAlpha.a10_1 line 1154
339. lemma OAI.SharpPlanar.IntegerAlpha.a10_1_contains line 1155
340. def OAI.SharpPlanar.IntegerAlpha.b10_1 line 1159
341. lemma OAI.SharpPlanar.IntegerAlpha.b10_1_contains line 1160
342. def OAI.SharpPlanar.IntegerAlpha.a10_2 line 1164
343. lemma OAI.SharpPlanar.IntegerAlpha.a10_2_contains line 1165
344. def OAI.SharpPlanar.IntegerAlpha.b10_2 line 1169
345. lemma OAI.SharpPlanar.IntegerAlpha.b10_2_contains line 1170
346. def OAI.SharpPlanar.IntegerAlpha.a10_3 line 1174
347. lemma OAI.SharpPlanar.IntegerAlpha.a10_3_contains line 1175
348. def OAI.SharpPlanar.IntegerAlpha.b10_3 line 1179
349. lemma OAI.SharpPlanar.IntegerAlpha.b10_3_contains line 1180
350. def OAI.SharpPlanar.IntegerAlpha.a10_4 line 1184
351. lemma OAI.SharpPlanar.IntegerAlpha.a10_4_contains line 1185
352. def OAI.SharpPlanar.IntegerAlpha.b10_4 line 1189
353. lemma OAI.SharpPlanar.IntegerAlpha.b10_4_contains line 1190
354. def OAI.SharpPlanar.IntegerAlpha.a10_5 line 1194
355. lemma OAI.SharpPlanar.IntegerAlpha.a10_5_contains line 1195
356. def OAI.SharpPlanar.IntegerAlpha.b10_5 line 1199
357. lemma OAI.SharpPlanar.IntegerAlpha.b10_5_contains line 1200
358. def OAI.SharpPlanar.IntegerAlpha.aRow10 line 1204
359. lemma OAI.SharpPlanar.IntegerAlpha.aRow10_contains line 1205
360. def OAI.SharpPlanar.IntegerAlpha.bRow10 line 1213
361. lemma OAI.SharpPlanar.IntegerAlpha.bRow10_contains line 1214
362. def OAI.SharpPlanar.IntegerAlpha.a11_0 line 1222
363. lemma OAI.SharpPlanar.IntegerAlpha.a11_0_contains line 1223
364. def OAI.SharpPlanar.IntegerAlpha.b11_0 line 1227
365. lemma OAI.SharpPlanar.IntegerAlpha.b11_0_contains line 1228
366. def OAI.SharpPlanar.IntegerAlpha.a11_1 line 1232
367. lemma OAI.SharpPlanar.IntegerAlpha.a11_1_contains line 1233
368. def OAI.SharpPlanar.IntegerAlpha.b11_1 line 1237
369. lemma OAI.SharpPlanar.IntegerAlpha.b11_1_contains line 1238
370. def OAI.SharpPlanar.IntegerAlpha.a11_2 line 1242
371. lemma OAI.SharpPlanar.IntegerAlpha.a11_2_contains line 1243
372. def OAI.SharpPlanar.IntegerAlpha.b11_2 line 1247
373. lemma OAI.SharpPlanar.IntegerAlpha.b11_2_contains line 1248
374. def OAI.SharpPlanar.IntegerAlpha.a11_3 line 1252
375. lemma OAI.SharpPlanar.IntegerAlpha.a11_3_contains line 1253
376. def OAI.SharpPlanar.IntegerAlpha.b11_3 line 1257
377. lemma OAI.SharpPlanar.IntegerAlpha.b11_3_contains line 1258
378. def OAI.SharpPlanar.IntegerAlpha.a11_4 line 1262
379. lemma OAI.SharpPlanar.IntegerAlpha.a11_4_contains line 1263
380. def OAI.SharpPlanar.IntegerAlpha.b11_4 line 1267
381. lemma OAI.SharpPlanar.IntegerAlpha.b11_4_contains line 1268
382. def OAI.SharpPlanar.IntegerAlpha.a11_5 line 1272
383. lemma OAI.SharpPlanar.IntegerAlpha.a11_5_contains line 1273
384. def OAI.SharpPlanar.IntegerAlpha.b11_5 line 1277
385. lemma OAI.SharpPlanar.IntegerAlpha.b11_5_contains line 1278
386. def OAI.SharpPlanar.IntegerAlpha.aRow11 line 1282
387. lemma OAI.SharpPlanar.IntegerAlpha.aRow11_contains line 1283
388. def OAI.SharpPlanar.IntegerAlpha.bRow11 line 1291
389. lemma OAI.SharpPlanar.IntegerAlpha.bRow11_contains line 1292
390. def OAI.SharpPlanar.IntegerAlpha.aTable line 1300
391. lemma OAI.SharpPlanar.IntegerAlpha.aTable_contains line 1301
392. def OAI.SharpPlanar.IntegerAlpha.aLookup line 1315
393. lemma OAI.SharpPlanar.IntegerAlpha.aLookup_contains line 1316
394. def OAI.SharpPlanar.IntegerAlpha.bTable line 1318
395. lemma OAI.SharpPlanar.IntegerAlpha.bTable_contains line 1319
396. def OAI.SharpPlanar.IntegerAlpha.bLookup line 1333
397. lemma OAI.SharpPlanar.IntegerAlpha.bLookup_contains line 1334
398. def OAI.SharpPlanar.IntegerBasis.weightedColumnBox line 1341
399. def OAI.SharpPlanar.IntegerBasis.momentKernelBox line 1343
400. def OAI.SharpPlanar.IntegerBasis.cachedMomentRuleBox line 1346
401. lemma OAI.SharpPlanar.IntegerBasis.weightedColumnBox_contains line 1349
402. lemma OAI.SharpPlanar.IntegerBasis.momentKernelBox_contains line 1354
403. lemma OAI.SharpPlanar.IntegerBasis.cachedMomentRuleBox_contains line 1363
404. lemma OAI.SharpPlanar.complexU_ofReal line 1385
405. lemma OAI.SharpPlanar.complexV_ofReal line 1386
406. lemma OAI.SharpPlanar.complexLambda_ofReal line 1387
407. lemma OAI.SharpPlanar.complexZ_ofReal line 1388
408. lemma OAI.SharpPlanar.complexBasisMoment_ofReal line 1389
409. lemma OAI.SharpPlanar.IntegerBasis.exp_direct_step line 1401
410. lemma OAI.SharpPlanar.IntegerBasis.exp_transformed_step line 1410
411. def OAI.SharpPlanar.IntegerBasis.transformedStepBox line 1420
412. lemma OAI.SharpPlanar.IntegerBasis.transformedStepBox_contains line 1421
413. def OAI.SharpPlanar.IntegerBasis.waveAmplitude line 1432
414. def OAI.SharpPlanar.IntegerBasis.waveAmplitudeBox line 1435
415. lemma OAI.SharpPlanar.IntegerBasis.waveAmplitude_mod line 1439
416. lemma OAI.SharpPlanar.IntegerBasis.basisFunction_wave line 1442
417. lemma OAI.SharpPlanar.IntegerBasis.waveAmplitudeBox_contains line 1447
418. lemma OAI.SharpPlanar.IntegerBasis.cached_weighted_wave line 1460