OAI/Analysis/Triangular/Certificate/WaveIntervals.lean

GitHub source file

669 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AtomicTriangular.Construction.TailNodes line 10
2. def OAI.AtomicTriangular.Construction.rootProduct line 12
3. theorem OAI.AtomicTriangular.Construction.P_eq_square line 14
4. theorem OAI.AtomicTriangular.Construction.differentiable_rootProduct line 17
5. theorem OAI.AtomicTriangular.Construction.differentiable_P line 21
6. theorem OAI.AtomicTriangular.Construction.node_residue line 25
7. theorem OAI.AtomicTriangular.Construction.rootProduct_node line 35
8. theorem OAI.AtomicTriangular.Construction.P_node line 58
9. theorem OAI.AtomicTriangular.Construction.hasDerivAt_P_node line 62
10. theorem OAI.AtomicTriangular.Construction.deriv_P_node line 67
11. theorem OAI.AtomicTriangular.Construction.differentiable_dBasis line 69
12. theorem OAI.AtomicTriangular.Construction.differentiable_cBasis line 74
13. theorem OAI.AtomicTriangular.Construction.dBasis_node line 79
14. theorem OAI.AtomicTriangular.Construction.dBasis_eq line 82
15. theorem OAI.AtomicTriangular.Construction.cBasis_eq line 86
16. theorem OAI.AtomicTriangular.Construction.differentiable_finiteC line 91
17. theorem OAI.AtomicTriangular.Construction.differentiable_finiteD line 95
18. theorem OAI.AtomicTriangular.Construction.P_factor line 99
19. theorem OAI.AtomicTriangular.Construction.finiteC_eq line 103
20. theorem OAI.AtomicTriangular.Construction.finiteD_eq line 112
21. theorem OAI.AtomicTriangular.Construction.phase_add line 121
22. theorem OAI.AtomicTriangular.Construction.phase_zero line 127
23. theorem OAI.AtomicTriangular.Construction.phase_neg_mul line 129
24. theorem OAI.AtomicTriangular.Construction.sineFactor_sq line 132
25. theorem OAI.AtomicTriangular.Construction.eval_atomFactor line 155
26. theorem OAI.AtomicTriangular.Construction.P_spectral line 170
27. theorem OAI.AtomicTriangular.Construction.finiteC_spectral line 182
28. theorem OAI.AtomicTriangular.Construction.finiteD_factor line 197
29. theorem OAI.AtomicTriangular.Construction.rest_spectral line 219
30. theorem OAI.AtomicTriangular.Construction.finiteD_spectral line 229
31. theorem OAI.AtomicTriangular.Construction.atomFactor_degree line 251
32. theorem OAI.AtomicTriangular.Construction.atomPolynomial_degree line 255
33. lemma OAI.AtomicTriangular.Construction.phase_nat_mul line 270
34. lemma OAI.AtomicTriangular.Construction.phase_offset line 276
35. lemma OAI.AtomicTriangular.Construction.P_fourier line 285
36. lemma OAI.AtomicTriangular.Construction.phase_int_mod line 294
37. lemma OAI.AtomicTriangular.Construction.wave_phase_integer line 307
38. lemma OAI.AtomicTriangular.Construction.waveDerivative_zero line 314
39. lemma OAI.AtomicTriangular.Construction.hasDerivAt_waveDerivative line 318
40. lemma OAI.AtomicTriangular.Construction.waveDerivative_eq_iterated line 328
41. lemma OAI.AtomicTriangular.Construction.hasDerivAt_P line 335
42. lemma OAI.AtomicTriangular.Construction.fourier_node_cancel line 338
43. lemma OAI.AtomicTriangular.Construction.fourier_node_deriv_cancel line 341
44. def OAI.AtomicTriangular.Interval.scale line 348
45. lemma OAI.AtomicTriangular.Interval.scale_pos line 349
46. lemma OAI.AtomicTriangular.Interval.scale_int_pos line 350
47. structure OAI.AtomicTriangular.Interval.RI line 352
48. def OAI.AtomicTriangular.Interval.RI.Mem line 357
49. def OAI.AtomicTriangular.Interval.RI.point line 359
50. def OAI.AtomicTriangular.Interval.RI.add line 360
51. def OAI.AtomicTriangular.Interval.RI.neg line 361
52. def OAI.AtomicTriangular.Interval.RI.sub line 362
53. def OAI.AtomicTriangular.Interval.imin4 line 364
54. def OAI.AtomicTriangular.Interval.imax4 line 365
55. def OAI.AtomicTriangular.Interval.RI.mul line 366
56. def OAI.AtomicTriangular.Interval.RI.divNat line 370
57. def OAI.AtomicTriangular.Interval.RI.widen line 371
58. def OAI.AtomicTriangular.Interval.RI.pow line 373
59. lemma OAI.AtomicTriangular.Interval.RI.mem_point line 377
60. lemma OAI.AtomicTriangular.Interval.RI.mem_add line 380
61. lemma OAI.AtomicTriangular.Interval.RI.mem_neg line 385
62. lemma OAI.AtomicTriangular.Interval.RI.mem_sub line 389
63. lemma OAI.AtomicTriangular.Interval.mul_bounds line 392
64. lemma OAI.AtomicTriangular.Interval.four_bounds line 400
65. lemma OAI.AtomicTriangular.Interval.div_floor_bounds line 413
66. lemma OAI.AtomicTriangular.Interval.RI.mem_mul line 419
67. lemma OAI.AtomicTriangular.Interval.RI.mem_divNat line 433
68. lemma OAI.AtomicTriangular.Interval.RI.mem_pow line 446
69. lemma OAI.AtomicTriangular.Interval.RI.mem_widen line 451
70. def OAI.AtomicTriangular.Interval.RI.invPos line 459
71. lemma OAI.AtomicTriangular.Interval.RI.mem_invPos line 461
72. structure OAI.AtomicTriangular.Interval.CI line 480
73. def OAI.AtomicTriangular.Interval.CI.Mem line 485
74. def OAI.AtomicTriangular.Interval.CI.ofReal line 487
75. def OAI.AtomicTriangular.Interval.CI.point line 488
76. def OAI.AtomicTriangular.Interval.CI.imag line 489
77. def OAI.AtomicTriangular.Interval.CI.add line 490
78. def OAI.AtomicTriangular.Interval.CI.neg line 491
79. def OAI.AtomicTriangular.Interval.CI.sub line 492
80. def OAI.AtomicTriangular.Interval.CI.mul line 494
81. def OAI.AtomicTriangular.Interval.CI.conj line 496
82. def OAI.AtomicTriangular.Interval.CI.divNat line 497
83. def OAI.AtomicTriangular.Interval.CI.widen line 498
84. def OAI.AtomicTriangular.Interval.CI.normSq line 499
85. def OAI.AtomicTriangular.Interval.CI.inv line 500
86. def OAI.AtomicTriangular.Interval.CI.pow line 502
87. lemma OAI.AtomicTriangular.Interval.CI.mem_ofReal line 506
88. lemma OAI.AtomicTriangular.Interval.CI.mem_point line 508
89. lemma OAI.AtomicTriangular.Interval.CI.mem_imag line 510
90. lemma OAI.AtomicTriangular.Interval.CI.mem_add line 512
91. lemma OAI.AtomicTriangular.Interval.CI.mem_neg line 514
92. lemma OAI.AtomicTriangular.Interval.CI.mem_sub line 516
93. lemma OAI.AtomicTriangular.Interval.CI.mem_mul line 518
94. lemma OAI.AtomicTriangular.Interval.CI.mem_divNat line 522
95. lemma OAI.AtomicTriangular.Interval.CI.mem_conj line 526
96. lemma OAI.AtomicTriangular.Interval.CI.mem_normSq line 528
97. lemma OAI.AtomicTriangular.Interval.CI.mem_inv line 530
98. lemma OAI.AtomicTriangular.Interval.CI.mem_pow line 534
99. lemma OAI.AtomicTriangular.Interval.CI.mem_widen line 542
100. def OAI.AtomicTriangular.Interval.CI.taylor line 550
101. lemma OAI.AtomicTriangular.Interval.CI.mem_taylor line 557
102. lemma OAI.AtomicTriangular.Interval.small_taylor_error line 573
103. def OAI.AtomicTriangular.Interval.CI.square line 582
104. lemma OAI.AtomicTriangular.Interval.CI.mem_square line 586
105. def OAI.AtomicTriangular.Interval.CI.exp line 594
106. lemma OAI.AtomicTriangular.Interval.CI.mem_exp line 597
107. lemma OAI.AtomicTriangular.Interval.RI.mem_of_subset line 609
108. lemma OAI.AtomicTriangular.Interval.CI.mem_of_subset line 615
109. lemma OAI.AtomicTriangular.Interval.CI.norm_le_of_mem line 620
110. lemma OAI.AtomicTriangular.Interval.CI.mem_exp_checked line 630
111. def OAI.AtomicTriangular.Interval.RI.abs line 634
112. def OAI.AtomicTriangular.Interval.RI.imax line 635
113. def OAI.AtomicTriangular.Interval.RI.imin line 636
114. def OAI.AtomicTriangular.Interval.RI.inv line 637
115. lemma OAI.AtomicTriangular.Interval.RI.mem_abs line 639
116. lemma OAI.AtomicTriangular.Interval.RI.mem_max line 649
117. lemma OAI.AtomicTriangular.Interval.RI.mem_min line 657
118. lemma OAI.AtomicTriangular.Interval.RI.mem_inv line 665
119. lemma OAI.AtomicTriangular.Interval.RI.mem_sqrt line 673
120. lemma OAI.AtomicTriangular.Interval.CI.mem_norm line 690
121. def OAI.AtomicTriangular.Interval.RI.sum line 704
122. lemma OAI.AtomicTriangular.Interval.RI.mem_sum line 707
123. def OAI.AtomicTriangular.Interval.CI.sum line 715
124. lemma OAI.AtomicTriangular.Interval.CI.mem_sum line 718
125. def OAI.AtomicTriangular.Constants.eps line 733
126. def OAI.AtomicTriangular.Constants.pStar line 734
127. def OAI.AtomicTriangular.Constants.bStar line 735
128. def OAI.AtomicTriangular.Constants.arctanPoly line 737
129. lemma OAI.AtomicTriangular.Constants.arctan_bracket line 740
130. lemma OAI.AtomicTriangular.Constants.bStar_bracket line 757
131. lemma OAI.AtomicTriangular.Constants.arctanPoly_inv5 line 766
132. lemma OAI.AtomicTriangular.Constants.arctanPoly_inv239 line 770
133. theorem OAI.AtomicTriangular.Constants.pStar_bracket line 774
134. def OAI.AtomicTriangular.FiniteCertificate.piBox line 797
135. lemma OAI.AtomicTriangular.FiniteCertificate.piBox_mem line 801
136. lemma OAI.AtomicTriangular.FiniteCertificate.phase_conj line 813
137. def OAI.AtomicTriangular.FiniteCertificate.partialPolynomial line 820
138. lemma OAI.AtomicTriangular.FiniteCertificate.partialPolynomial_zero line 823
139. lemma OAI.AtomicTriangular.FiniteCertificate.partialPolynomial_fifteen line 824
140. lemma OAI.AtomicTriangular.FiniteCertificate.partialPolynomial_succ line 825
141. lemma OAI.AtomicTriangular.FiniteCertificate.coeff_X_mul' line 837
142. lemma OAI.AtomicTriangular.FiniteCertificate.coeff_X_sq_mul line 843
143. lemma OAI.AtomicTriangular.FiniteCertificate.coeff_atom_mul line 853
144. def OAI.AtomicTriangular.FiniteCertificate.coeffStep line 864
145. lemma OAI.AtomicTriangular.FiniteCertificate.coeffStep_mem line 869
146. def OAI.AtomicTriangular.FiniteCertificate.phaseInputBox line 887
147. lemma OAI.AtomicTriangular.FiniteCertificate.phaseInputBox_mem line 890
148. def OAI.AtomicTriangular.FiniteCertificate.phaseBox0 line 904
149. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox0_calc line 905
150. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox0_mem line 906
151. def OAI.AtomicTriangular.FiniteCertificate.phaseBox1 line 909
152. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox1_calc line 910
153. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox1_mem line 911
154. def OAI.AtomicTriangular.FiniteCertificate.phaseBox2 line 914
155. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox2_calc line 915
156. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox2_mem line 916
157. def OAI.AtomicTriangular.FiniteCertificate.phaseBox3 line 919
158. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox3_calc line 920
159. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox3_mem line 921
160. def OAI.AtomicTriangular.FiniteCertificate.phaseBox4 line 924
161. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox4_calc line 925
162. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox4_mem line 926
163. def OAI.AtomicTriangular.FiniteCertificate.phaseBox5 line 929
164. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox5_calc line 930
165. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox5_mem line 931
166. def OAI.AtomicTriangular.FiniteCertificate.phaseBox6 line 934
167. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox6_calc line 935
168. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox6_mem line 936
169. def OAI.AtomicTriangular.FiniteCertificate.phaseBox7 line 939
170. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox7_calc line 940
171. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox7_mem line 941
172. def OAI.AtomicTriangular.FiniteCertificate.phaseBox8 line 944
173. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox8_calc line 945
174. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox8_mem line 946
175. def OAI.AtomicTriangular.FiniteCertificate.phaseBox9 line 949
176. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox9_calc line 950
177. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox9_mem line 951
178. def OAI.AtomicTriangular.FiniteCertificate.phaseBox10 line 954
179. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox10_calc line 955
180. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox10_mem line 956
181. def OAI.AtomicTriangular.FiniteCertificate.phaseBox11 line 959
182. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox11_calc line 960
183. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox11_mem line 961
184. def OAI.AtomicTriangular.FiniteCertificate.phaseBox12 line 964
185. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox12_calc line 965
186. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox12_mem line 966
187. def OAI.AtomicTriangular.FiniteCertificate.phaseBox13 line 969
188. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox13_calc line 970
189. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox13_mem line 971
190. def OAI.AtomicTriangular.FiniteCertificate.phaseBox14 line 974
191. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox14_calc line 975
192. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox14_mem line 976
193. def OAI.AtomicTriangular.FiniteCertificate.phaseBox15 line 979
194. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox15_calc line 980
195. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox15_mem line 981
196. def OAI.AtomicTriangular.FiniteCertificate.phaseBox16 line 984
197. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox16_calc line 985
198. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox16_mem line 986
199. def OAI.AtomicTriangular.FiniteCertificate.phaseBox17 line 989
200. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox17_calc line 990
201. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox17_mem line 991
202. def OAI.AtomicTriangular.FiniteCertificate.phaseBox18 line 994
203. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox18_calc line 995
204. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox18_mem line 996
205. def OAI.AtomicTriangular.FiniteCertificate.phaseBox19 line 999
206. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox19_calc line 1000
207. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox19_mem line 1001
208. def OAI.AtomicTriangular.FiniteCertificate.phaseBox20 line 1004
209. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox20_calc line 1005
210. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox20_mem line 1006
211. def OAI.AtomicTriangular.FiniteCertificate.phaseBox21 line 1009
212. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox21_calc line 1010
213. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox21_mem line 1011
214. def OAI.AtomicTriangular.FiniteCertificate.phaseBox22 line 1014
215. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox22_calc line 1015
216. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox22_mem line 1016
217. def OAI.AtomicTriangular.FiniteCertificate.phaseBox23 line 1019
218. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox23_calc line 1020
219. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox23_mem line 1021
220. def OAI.AtomicTriangular.FiniteCertificate.phaseBox24 line 1024
221. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox24_calc line 1025
222. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox24_mem line 1026
223. def OAI.AtomicTriangular.FiniteCertificate.phaseBox25 line 1029
224. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox25_calc line 1030
225. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox25_mem line 1031
226. def OAI.AtomicTriangular.FiniteCertificate.phaseBox26 line 1034
227. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox26_calc line 1035
228. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox26_mem line 1036
229. def OAI.AtomicTriangular.FiniteCertificate.phaseBox27 line 1039
230. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox27_calc line 1040
231. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox27_mem line 1041
232. def OAI.AtomicTriangular.FiniteCertificate.phaseBox28 line 1044
233. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox28_calc line 1045
234. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox28_mem line 1046
235. def OAI.AtomicTriangular.FiniteCertificate.phaseBox29 line 1049
236. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox29_calc line 1050
237. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox29_mem line 1051
238. def OAI.AtomicTriangular.FiniteCertificate.phaseBox30 line 1054
239. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox30_calc line 1055
240. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox30_mem line 1056
241. def OAI.AtomicTriangular.FiniteCertificate.phaseBox31 line 1059
242. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox31_calc line 1060
243. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox31_mem line 1061
244. def OAI.AtomicTriangular.FiniteCertificate.phaseBox32 line 1064
245. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox32_calc line 1065
246. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox32_mem line 1066
247. def OAI.AtomicTriangular.FiniteCertificate.phaseBox33 line 1069
248. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox33_calc line 1070
249. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox33_mem line 1071
250. def OAI.AtomicTriangular.FiniteCertificate.phaseBox34 line 1074
251. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox34_calc line 1075
252. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox34_mem line 1076
253. def OAI.AtomicTriangular.FiniteCertificate.phaseBox35 line 1079
254. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox35_calc line 1080
255. lemma OAI.AtomicTriangular.FiniteCertificate.phaseBox35_mem line 1081
256. def OAI.AtomicTriangular.FiniteCertificate.coeffBox0 line 1084
257. lemma OAI.AtomicTriangular.FiniteCertificate.coeffBox0_mem line 1085
258. def OAI.AtomicTriangular.FiniteCertificate.coeffBox1 line 1092
259. lemma OAI.AtomicTriangular.FiniteCertificate.coeffBox1_calc line 1124
260. lemma OAI.AtomicTriangular.FiniteCertificate.coeffBox1_mem line 1127
261. def OAI.AtomicTriangular.FiniteCertificate.coeffBox2 line 1134
262. lemma OAI.AtomicTriangular.FiniteCertificate.coeffBox2_calc line 1166
263. lemma OAI.AtomicTriangular.FiniteCertificate.coeffBox2_mem line 1169
264. def OAI.AtomicTriangular.FiniteCertificate.coeffBox3 line 1176
265. lemma OAI.AtomicTriangular.FiniteCertificate.coeffBox3_calc line 1208
266. lemma OAI.AtomicTriangular.FiniteCertificate.coeffBox3_mem line 1211
267. def OAI.AtomicTriangular.FiniteCertificate.coeffBox4 line 1218
268. lemma OAI.AtomicTriangular.FiniteCertificate.coeffBox4_calc line 1250
269. lemma OAI.AtomicTriangular.FiniteCertificate.coeffBox4_mem line 1253
270. def OAI.AtomicTriangular.FiniteCertificate.coeffBox5 line 1260
271. lemma OAI.AtomicTriangular.FiniteCertificate.coeffBox5_calc line 1292
272. lemma OAI.AtomicTriangular.FiniteCertificate.coeffBox5_mem line 1295
273. def OAI.AtomicTriangular.FiniteCertificate.coeffBox6 line 1302
274. lemma OAI.AtomicTriangular.FiniteCertificate.coeffBox6_calc line 1334
275. lemma OAI.AtomicTriangular.FiniteCertificate.coeffBox6_mem line 1337
276. def OAI.AtomicTriangular.FiniteCertificate.coeffBox7 line 1344
277. lemma OAI.AtomicTriangular.FiniteCertificate.coeffBox7_calc line 1376
278. lemma OAI.AtomicTriangular.FiniteCertificate.coeffBox7_mem line 1379
279. def OAI.AtomicTriangular.FiniteCertificate.coeffBox8 line 1386
280. lemma OAI.AtomicTriangular.FiniteCertificate.coeffBox8_calc line 1418
281. lemma OAI.AtomicTriangular.FiniteCertificate.coeffBox8_mem line 1421
282. def OAI.AtomicTriangular.FiniteCertificate.coeffBox9 line 1428
283. lemma OAI.AtomicTriangular.FiniteCertificate.coeffBox9_calc line 1460
284. lemma OAI.AtomicTriangular.FiniteCertificate.coeffBox9_mem line 1463
285. def OAI.AtomicTriangular.FiniteCertificate.coeffBox10 line 1470
286. lemma OAI.AtomicTriangular.FiniteCertificate.coeffBox10_calc line 1502
287. lemma OAI.AtomicTriangular.FiniteCertificate.coeffBox10_mem line 1505
288. def OAI.AtomicTriangular.FiniteCertificate.coeffBox11 line 1512
289. lemma OAI.AtomicTriangular.FiniteCertificate.coeffBox11_calc line 1544
290. lemma OAI.AtomicTriangular.FiniteCertificate.coeffBox11_mem line 1547
291. def OAI.AtomicTriangular.FiniteCertificate.coeffBox12 line 1554
292. lemma OAI.AtomicTriangular.FiniteCertificate.coeffBox12_calc line 1586
293. lemma OAI.AtomicTriangular.FiniteCertificate.coeffBox12_mem line 1589
294. def OAI.AtomicTriangular.FiniteCertificate.coeffBox13 line 1596
295. lemma OAI.AtomicTriangular.FiniteCertificate.coeffBox13_calc line 1628
296. lemma OAI.AtomicTriangular.FiniteCertificate.coeffBox13_mem line 1631
297. def OAI.AtomicTriangular.FiniteCertificate.coeffBox14 line 1638
298. lemma OAI.AtomicTriangular.FiniteCertificate.coeffBox14_calc line 1670
299. lemma OAI.AtomicTriangular.FiniteCertificate.coeffBox14_mem line 1673
300. def OAI.AtomicTriangular.FiniteCertificate.coeffBox15 line 1680
301. lemma OAI.AtomicTriangular.FiniteCertificate.coeffBox15_calc line 1712
302. lemma OAI.AtomicTriangular.FiniteCertificate.coeffBox15_mem line 1715
303. lemma OAI.AtomicTriangular.FiniteCertificate.atomPolynomial_coeff_mem line 1722
304. def OAI.AtomicTriangular.FiniteCertificate.phaseTable line 1730
305. lemma OAI.AtomicTriangular.FiniteCertificate.phaseTable_mem line 1731
306. def OAI.AtomicTriangular.FiniteCertificate.phaseModBox line 1769
307. lemma OAI.AtomicTriangular.FiniteCertificate.phaseModBox_mem line 1770
308. def OAI.AtomicTriangular.FiniteCertificate.frequencyBox line 1775
309. lemma OAI.AtomicTriangular.FiniteCertificate.frequencyBox_mem line 1777
310. def OAI.AtomicTriangular.FiniteCertificate.waveDerivativeBox line 1788
311. lemma OAI.AtomicTriangular.FiniteCertificate.waveDerivativeBox_mem line 1790
312. def OAI.AtomicTriangular.FiniteCertificate.jetBox2_0 line 1798
313. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox2_0_calc line 1799
314. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox2_0_mem line 1800
315. def OAI.AtomicTriangular.FiniteCertificate.jetBox3_0 line 1803
316. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox3_0_calc line 1804
317. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox3_0_mem line 1805
318. def OAI.AtomicTriangular.FiniteCertificate.QBox0 line 1808
319. lemma OAI.AtomicTriangular.FiniteCertificate.QBox0_calc line 1809
320. lemma OAI.AtomicTriangular.FiniteCertificate.QBox0_mem line 1810
321. def OAI.AtomicTriangular.FiniteCertificate.DBox0 line 1813
322. lemma OAI.AtomicTriangular.FiniteCertificate.DBox0_calc line 1814
323. lemma OAI.AtomicTriangular.FiniteCertificate.DBox0_mem line 1815
324. lemma OAI.AtomicTriangular.FiniteCertificate.Q_0_bounds line 1823
325. lemma OAI.AtomicTriangular.FiniteCertificate.D_0_bound line 1827
326. def OAI.AtomicTriangular.FiniteCertificate.jetBox2_1 line 1832
327. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox2_1_calc line 1833
328. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox2_1_mem line 1834
329. def OAI.AtomicTriangular.FiniteCertificate.jetBox3_1 line 1837
330. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox3_1_calc line 1838
331. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox3_1_mem line 1839
332. def OAI.AtomicTriangular.FiniteCertificate.QBox1 line 1842
333. lemma OAI.AtomicTriangular.FiniteCertificate.QBox1_calc line 1843
334. lemma OAI.AtomicTriangular.FiniteCertificate.QBox1_mem line 1844
335. def OAI.AtomicTriangular.FiniteCertificate.DBox1 line 1847
336. lemma OAI.AtomicTriangular.FiniteCertificate.DBox1_calc line 1848
337. lemma OAI.AtomicTriangular.FiniteCertificate.DBox1_mem line 1849
338. lemma OAI.AtomicTriangular.FiniteCertificate.Q_1_bounds line 1857
339. lemma OAI.AtomicTriangular.FiniteCertificate.D_1_bound line 1861
340. def OAI.AtomicTriangular.FiniteCertificate.jetBox2_3 line 1866
341. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox2_3_calc line 1867
342. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox2_3_mem line 1868
343. def OAI.AtomicTriangular.FiniteCertificate.jetBox3_3 line 1871
344. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox3_3_calc line 1872
345. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox3_3_mem line 1873
346. def OAI.AtomicTriangular.FiniteCertificate.QBox3 line 1876
347. lemma OAI.AtomicTriangular.FiniteCertificate.QBox3_calc line 1877
348. lemma OAI.AtomicTriangular.FiniteCertificate.QBox3_mem line 1878
349. def OAI.AtomicTriangular.FiniteCertificate.DBox3 line 1881
350. lemma OAI.AtomicTriangular.FiniteCertificate.DBox3_calc line 1882
351. lemma OAI.AtomicTriangular.FiniteCertificate.DBox3_mem line 1883
352. lemma OAI.AtomicTriangular.FiniteCertificate.Q_3_bounds line 1891
353. lemma OAI.AtomicTriangular.FiniteCertificate.D_3_bound line 1895
354. def OAI.AtomicTriangular.FiniteCertificate.jetBox2_4 line 1900
355. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox2_4_calc line 1901
356. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox2_4_mem line 1902
357. def OAI.AtomicTriangular.FiniteCertificate.jetBox3_4 line 1905
358. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox3_4_calc line 1906
359. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox3_4_mem line 1907
360. def OAI.AtomicTriangular.FiniteCertificate.QBox4 line 1910
361. lemma OAI.AtomicTriangular.FiniteCertificate.QBox4_calc line 1911
362. lemma OAI.AtomicTriangular.FiniteCertificate.QBox4_mem line 1912
363. def OAI.AtomicTriangular.FiniteCertificate.DBox4 line 1915
364. lemma OAI.AtomicTriangular.FiniteCertificate.DBox4_calc line 1916
365. lemma OAI.AtomicTriangular.FiniteCertificate.DBox4_mem line 1917
366. lemma OAI.AtomicTriangular.FiniteCertificate.Q_4_bounds line 1925
367. lemma OAI.AtomicTriangular.FiniteCertificate.D_4_bound line 1929
368. def OAI.AtomicTriangular.FiniteCertificate.jetBox2_7 line 1934
369. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox2_7_calc line 1935
370. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox2_7_mem line 1936
371. def OAI.AtomicTriangular.FiniteCertificate.jetBox3_7 line 1939
372. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox3_7_calc line 1940
373. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox3_7_mem line 1941
374. def OAI.AtomicTriangular.FiniteCertificate.QBox7 line 1944
375. lemma OAI.AtomicTriangular.FiniteCertificate.QBox7_calc line 1945
376. lemma OAI.AtomicTriangular.FiniteCertificate.QBox7_mem line 1946
377. def OAI.AtomicTriangular.FiniteCertificate.DBox7 line 1949
378. lemma OAI.AtomicTriangular.FiniteCertificate.DBox7_calc line 1950
379. lemma OAI.AtomicTriangular.FiniteCertificate.DBox7_mem line 1951
380. lemma OAI.AtomicTriangular.FiniteCertificate.Q_7_bounds line 1959
381. lemma OAI.AtomicTriangular.FiniteCertificate.D_7_bound line 1963
382. def OAI.AtomicTriangular.FiniteCertificate.jetBox2_9 line 1968
383. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox2_9_calc line 1969
384. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox2_9_mem line 1970
385. def OAI.AtomicTriangular.FiniteCertificate.jetBox3_9 line 1973
386. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox3_9_calc line 1974
387. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox3_9_mem line 1975
388. def OAI.AtomicTriangular.FiniteCertificate.QBox9 line 1978
389. lemma OAI.AtomicTriangular.FiniteCertificate.QBox9_calc line 1979
390. lemma OAI.AtomicTriangular.FiniteCertificate.QBox9_mem line 1980
391. def OAI.AtomicTriangular.FiniteCertificate.DBox9 line 1983
392. lemma OAI.AtomicTriangular.FiniteCertificate.DBox9_calc line 1984
393. lemma OAI.AtomicTriangular.FiniteCertificate.DBox9_mem line 1985
394. lemma OAI.AtomicTriangular.FiniteCertificate.Q_9_bounds line 1993
395. lemma OAI.AtomicTriangular.FiniteCertificate.D_9_bound line 1997
396. def OAI.AtomicTriangular.FiniteCertificate.jetBox2_12 line 2002
397. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox2_12_calc line 2003
398. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox2_12_mem line 2004
399. def OAI.AtomicTriangular.FiniteCertificate.jetBox3_12 line 2007
400. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox3_12_calc line 2008
401. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox3_12_mem line 2009
402. def OAI.AtomicTriangular.FiniteCertificate.QBox12 line 2012
403. lemma OAI.AtomicTriangular.FiniteCertificate.QBox12_calc line 2013
404. lemma OAI.AtomicTriangular.FiniteCertificate.QBox12_mem line 2014
405. def OAI.AtomicTriangular.FiniteCertificate.DBox12 line 2017
406. lemma OAI.AtomicTriangular.FiniteCertificate.DBox12_calc line 2018
407. lemma OAI.AtomicTriangular.FiniteCertificate.DBox12_mem line 2019
408. lemma OAI.AtomicTriangular.FiniteCertificate.Q_12_bounds line 2027
409. lemma OAI.AtomicTriangular.FiniteCertificate.D_12_bound line 2031
410. def OAI.AtomicTriangular.FiniteCertificate.jetBox2_13 line 2036
411. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox2_13_calc line 2037
412. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox2_13_mem line 2038
413. def OAI.AtomicTriangular.FiniteCertificate.jetBox3_13 line 2041
414. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox3_13_calc line 2042
415. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox3_13_mem line 2043
416. def OAI.AtomicTriangular.FiniteCertificate.QBox13 line 2046
417. lemma OAI.AtomicTriangular.FiniteCertificate.QBox13_calc line 2047
418. lemma OAI.AtomicTriangular.FiniteCertificate.QBox13_mem line 2048
419. def OAI.AtomicTriangular.FiniteCertificate.DBox13 line 2051
420. lemma OAI.AtomicTriangular.FiniteCertificate.DBox13_calc line 2052
421. lemma OAI.AtomicTriangular.FiniteCertificate.DBox13_mem line 2053
422. lemma OAI.AtomicTriangular.FiniteCertificate.Q_13_bounds line 2061
423. lemma OAI.AtomicTriangular.FiniteCertificate.D_13_bound line 2065
424. def OAI.AtomicTriangular.FiniteCertificate.jetBox2_16 line 2070
425. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox2_16_calc line 2071
426. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox2_16_mem line 2072
427. def OAI.AtomicTriangular.FiniteCertificate.jetBox3_16 line 2075
428. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox3_16_calc line 2076
429. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox3_16_mem line 2077
430. def OAI.AtomicTriangular.FiniteCertificate.QBox16 line 2080
431. lemma OAI.AtomicTriangular.FiniteCertificate.QBox16_calc line 2081
432. lemma OAI.AtomicTriangular.FiniteCertificate.QBox16_mem line 2082
433. def OAI.AtomicTriangular.FiniteCertificate.DBox16 line 2085
434. lemma OAI.AtomicTriangular.FiniteCertificate.DBox16_calc line 2086
435. lemma OAI.AtomicTriangular.FiniteCertificate.DBox16_mem line 2087
436. lemma OAI.AtomicTriangular.FiniteCertificate.Q_16_bounds line 2095
437. lemma OAI.AtomicTriangular.FiniteCertificate.D_16_bound line 2099
438. def OAI.AtomicTriangular.FiniteCertificate.jetBox2_19 line 2104
439. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox2_19_calc line 2105
440. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox2_19_mem line 2106
441. def OAI.AtomicTriangular.FiniteCertificate.jetBox3_19 line 2109
442. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox3_19_calc line 2110
443. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox3_19_mem line 2111
444. def OAI.AtomicTriangular.FiniteCertificate.QBox19 line 2114
445. lemma OAI.AtomicTriangular.FiniteCertificate.QBox19_calc line 2115
446. lemma OAI.AtomicTriangular.FiniteCertificate.QBox19_mem line 2116
447. def OAI.AtomicTriangular.FiniteCertificate.DBox19 line 2119
448. lemma OAI.AtomicTriangular.FiniteCertificate.DBox19_calc line 2120
449. lemma OAI.AtomicTriangular.FiniteCertificate.DBox19_mem line 2121
450. lemma OAI.AtomicTriangular.FiniteCertificate.Q_19_bounds line 2129
451. lemma OAI.AtomicTriangular.FiniteCertificate.D_19_bound line 2133
452. def OAI.AtomicTriangular.FiniteCertificate.jetBox2_21 line 2138
453. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox2_21_calc line 2139
454. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox2_21_mem line 2140
455. def OAI.AtomicTriangular.FiniteCertificate.jetBox3_21 line 2143
456. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox3_21_calc line 2144
457. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox3_21_mem line 2145
458. def OAI.AtomicTriangular.FiniteCertificate.QBox21 line 2148
459. lemma OAI.AtomicTriangular.FiniteCertificate.QBox21_calc line 2149
460. lemma OAI.AtomicTriangular.FiniteCertificate.QBox21_mem line 2150
461. def OAI.AtomicTriangular.FiniteCertificate.DBox21 line 2153
462. lemma OAI.AtomicTriangular.FiniteCertificate.DBox21_calc line 2154
463. lemma OAI.AtomicTriangular.FiniteCertificate.DBox21_mem line 2155
464. lemma OAI.AtomicTriangular.FiniteCertificate.Q_21_bounds line 2163
465. lemma OAI.AtomicTriangular.FiniteCertificate.D_21_bound line 2167
466. def OAI.AtomicTriangular.FiniteCertificate.jetBox2_25 line 2172
467. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox2_25_calc line 2173
468. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox2_25_mem line 2174
469. def OAI.AtomicTriangular.FiniteCertificate.jetBox3_25 line 2177
470. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox3_25_calc line 2178
471. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox3_25_mem line 2179
472. def OAI.AtomicTriangular.FiniteCertificate.QBox25 line 2182
473. lemma OAI.AtomicTriangular.FiniteCertificate.QBox25_calc line 2183
474. lemma OAI.AtomicTriangular.FiniteCertificate.QBox25_mem line 2184
475. def OAI.AtomicTriangular.FiniteCertificate.DBox25 line 2187
476. lemma OAI.AtomicTriangular.FiniteCertificate.DBox25_calc line 2188
477. lemma OAI.AtomicTriangular.FiniteCertificate.DBox25_mem line 2189
478. lemma OAI.AtomicTriangular.FiniteCertificate.Q_25_bounds line 2197
479. lemma OAI.AtomicTriangular.FiniteCertificate.D_25_bound line 2201
480. def OAI.AtomicTriangular.FiniteCertificate.jetBox2_27 line 2206
481. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox2_27_calc line 2207
482. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox2_27_mem line 2208
483. def OAI.AtomicTriangular.FiniteCertificate.jetBox3_27 line 2211
484. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox3_27_calc line 2212
485. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox3_27_mem line 2213
486. def OAI.AtomicTriangular.FiniteCertificate.QBox27 line 2216
487. lemma OAI.AtomicTriangular.FiniteCertificate.QBox27_calc line 2217
488. lemma OAI.AtomicTriangular.FiniteCertificate.QBox27_mem line 2218
489. def OAI.AtomicTriangular.FiniteCertificate.DBox27 line 2221
490. lemma OAI.AtomicTriangular.FiniteCertificate.DBox27_calc line 2222
491. lemma OAI.AtomicTriangular.FiniteCertificate.DBox27_mem line 2223
492. lemma OAI.AtomicTriangular.FiniteCertificate.Q_27_bounds line 2231
493. lemma OAI.AtomicTriangular.FiniteCertificate.D_27_bound line 2235
494. def OAI.AtomicTriangular.FiniteCertificate.jetBox2_28 line 2240
495. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox2_28_calc line 2241
496. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox2_28_mem line 2242
497. def OAI.AtomicTriangular.FiniteCertificate.jetBox3_28 line 2245
498. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox3_28_calc line 2246
499. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox3_28_mem line 2247
500. def OAI.AtomicTriangular.FiniteCertificate.QBox28 line 2250
501. lemma OAI.AtomicTriangular.FiniteCertificate.QBox28_calc line 2251
502. lemma OAI.AtomicTriangular.FiniteCertificate.QBox28_mem line 2252
503. def OAI.AtomicTriangular.FiniteCertificate.DBox28 line 2255
504. lemma OAI.AtomicTriangular.FiniteCertificate.DBox28_calc line 2256
505. lemma OAI.AtomicTriangular.FiniteCertificate.DBox28_mem line 2257
506. lemma OAI.AtomicTriangular.FiniteCertificate.Q_28_bounds line 2265
507. lemma OAI.AtomicTriangular.FiniteCertificate.D_28_bound line 2269
508. def OAI.AtomicTriangular.FiniteCertificate.jetBox2_31 line 2274
509. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox2_31_calc line 2275
510. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox2_31_mem line 2276
511. def OAI.AtomicTriangular.FiniteCertificate.jetBox3_31 line 2279
512. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox3_31_calc line 2280
513. lemma OAI.AtomicTriangular.FiniteCertificate.jetBox3_31_mem line 2281
514. def OAI.AtomicTriangular.FiniteCertificate.QBox31 line 2284
515. lemma OAI.AtomicTriangular.FiniteCertificate.QBox31_calc line 2285
516. lemma OAI.AtomicTriangular.FiniteCertificate.QBox31_mem line 2286
517. def OAI.AtomicTriangular.FiniteCertificate.DBox31 line 2289
518. lemma OAI.AtomicTriangular.FiniteCertificate.DBox31_calc line 2290
519. lemma OAI.AtomicTriangular.FiniteCertificate.DBox31_mem line 2291
520. lemma OAI.AtomicTriangular.FiniteCertificate.Q_31_bounds line 2299
521. lemma OAI.AtomicTriangular.FiniteCertificate.D_31_bound line 2303
522. def OAI.AtomicTriangular.FiniteCertificate.restPolynomial line 2315
523. lemma OAI.AtomicTriangular.FiniteCertificate.atomPolynomial_factor line 2318
524. lemma OAI.AtomicTriangular.FiniteCertificate.restPolynomial_degree line 2322
525. lemma OAI.AtomicTriangular.FiniteCertificate.restPolynomial_coeff line 2330
526. def OAI.AtomicTriangular.FiniteCertificate.recoverRest line 2344
527. lemma OAI.AtomicTriangular.FiniteCertificate.recoverRest_mem line 2349
528. lemma OAI.AtomicTriangular.FiniteCertificate.cCoefficient_eq line 2372
529. lemma OAI.AtomicTriangular.FiniteCertificate.dCoefficient_eq line 2378
530. lemma OAI.AtomicTriangular.FiniteCertificate.cShift_degree line 2390
531. lemma OAI.AtomicTriangular.FiniteCertificate.dAtom_degree line 2398
532. lemma OAI.AtomicTriangular.FiniteCertificate.polynomial_fourier line 2405
533. lemma OAI.AtomicTriangular.FiniteCertificate.finiteC_fourier line 2414
534. lemma OAI.AtomicTriangular.FiniteCertificate.finiteD_fourier line 2425
535. def OAI.AtomicTriangular.FiniteCertificate.kappaBox line 2435
536. lemma OAI.AtomicTriangular.FiniteCertificate.kappaBox_mem line 2436
537. def OAI.AtomicTriangular.FiniteCertificate.cCoeffBox line 2440
538. def OAI.AtomicTriangular.FiniteCertificate.dCoeffBox line 2442
539. lemma OAI.AtomicTriangular.FiniteCertificate.cCoeffBox_mem line 2445
540. lemma OAI.AtomicTriangular.FiniteCertificate.dCoeffBox_mem line 2454
541. def OAI.AtomicTriangular.FiniteCertificate.restBox0 line 2467
542. lemma OAI.AtomicTriangular.FiniteCertificate.restBox0_calc line 2499
543. lemma OAI.AtomicTriangular.FiniteCertificate.restBox0_mem line 2502
544. def OAI.AtomicTriangular.FiniteCertificate.cBox0 line 2508
545. lemma OAI.AtomicTriangular.FiniteCertificate.cBox0_calc line 2540
546. lemma OAI.AtomicTriangular.FiniteCertificate.cBox0_mem line 2543
547. def OAI.AtomicTriangular.FiniteCertificate.dBox0 line 2546
548. lemma OAI.AtomicTriangular.FiniteCertificate.dBox0_calc line 2578
549. lemma OAI.AtomicTriangular.FiniteCertificate.dBox0_mem line 2581
550. def OAI.AtomicTriangular.FiniteCertificate.restBox1 line 2588
551. lemma OAI.AtomicTriangular.FiniteCertificate.restBox1_calc line 2620
552. lemma OAI.AtomicTriangular.FiniteCertificate.restBox1_mem line 2623
553. def OAI.AtomicTriangular.FiniteCertificate.cBox1 line 2629
554. lemma OAI.AtomicTriangular.FiniteCertificate.cBox1_calc line 2661
555. lemma OAI.AtomicTriangular.FiniteCertificate.cBox1_mem line 2664
556. def OAI.AtomicTriangular.FiniteCertificate.dBox1 line 2667
557. lemma OAI.AtomicTriangular.FiniteCertificate.dBox1_calc line 2699
558. lemma OAI.AtomicTriangular.FiniteCertificate.dBox1_mem line 2702
559. def OAI.AtomicTriangular.FiniteCertificate.restBox3 line 2709
560. lemma OAI.AtomicTriangular.FiniteCertificate.restBox3_calc line 2741
561. lemma OAI.AtomicTriangular.FiniteCertificate.restBox3_mem line 2744
562. def OAI.AtomicTriangular.FiniteCertificate.cBox3 line 2750
563. lemma OAI.AtomicTriangular.FiniteCertificate.cBox3_calc line 2782
564. lemma OAI.AtomicTriangular.FiniteCertificate.cBox3_mem line 2785
565. def OAI.AtomicTriangular.FiniteCertificate.dBox3 line 2788
566. lemma OAI.AtomicTriangular.FiniteCertificate.dBox3_calc line 2820
567. lemma OAI.AtomicTriangular.FiniteCertificate.dBox3_mem line 2823
568. def OAI.AtomicTriangular.FiniteCertificate.restBox4 line 2830
569. lemma OAI.AtomicTriangular.FiniteCertificate.restBox4_calc line 2862
570. lemma OAI.AtomicTriangular.FiniteCertificate.restBox4_mem line 2865
571. def OAI.AtomicTriangular.FiniteCertificate.cBox4 line 2871
572. lemma OAI.AtomicTriangular.FiniteCertificate.cBox4_calc line 2903
573. lemma OAI.AtomicTriangular.FiniteCertificate.cBox4_mem line 2906
574. def OAI.AtomicTriangular.FiniteCertificate.dBox4 line 2909
575. lemma OAI.AtomicTriangular.FiniteCertificate.dBox4_calc line 2941
576. lemma OAI.AtomicTriangular.FiniteCertificate.dBox4_mem line 2944
577. def OAI.AtomicTriangular.FiniteCertificate.restBox7 line 2951
578. lemma OAI.AtomicTriangular.FiniteCertificate.restBox7_calc line 2983
579. lemma OAI.AtomicTriangular.FiniteCertificate.restBox7_mem line 2986
580. def OAI.AtomicTriangular.FiniteCertificate.cBox7 line 2992
581. lemma OAI.AtomicTriangular.FiniteCertificate.cBox7_calc line 3024
582. lemma OAI.AtomicTriangular.FiniteCertificate.cBox7_mem line 3027
583. def OAI.AtomicTriangular.FiniteCertificate.dBox7 line 3030
584. lemma OAI.AtomicTriangular.FiniteCertificate.dBox7_calc line 3062
585. lemma OAI.AtomicTriangular.FiniteCertificate.dBox7_mem line 3065
586. def OAI.AtomicTriangular.FiniteCertificate.restBox9 line 3072
587. lemma OAI.AtomicTriangular.FiniteCertificate.restBox9_calc line 3104
588. lemma OAI.AtomicTriangular.FiniteCertificate.restBox9_mem line 3107
589. def OAI.AtomicTriangular.FiniteCertificate.cBox9 line 3113
590. lemma OAI.AtomicTriangular.FiniteCertificate.cBox9_calc line 3145
591. lemma OAI.AtomicTriangular.FiniteCertificate.cBox9_mem line 3148
592. def OAI.AtomicTriangular.FiniteCertificate.dBox9 line 3151
593. lemma OAI.AtomicTriangular.FiniteCertificate.dBox9_calc line 3183
594. lemma OAI.AtomicTriangular.FiniteCertificate.dBox9_mem line 3186
595. def OAI.AtomicTriangular.FiniteCertificate.restBox12 line 3193
596. lemma OAI.AtomicTriangular.FiniteCertificate.restBox12_calc line 3225
597. lemma OAI.AtomicTriangular.FiniteCertificate.restBox12_mem line 3228
598. def OAI.AtomicTriangular.FiniteCertificate.cBox12 line 3234
599. lemma OAI.AtomicTriangular.FiniteCertificate.cBox12_calc line 3266
600. lemma OAI.AtomicTriangular.FiniteCertificate.cBox12_mem line 3269
601. def OAI.AtomicTriangular.FiniteCertificate.dBox12 line 3272
602. lemma OAI.AtomicTriangular.FiniteCertificate.dBox12_calc line 3304
603. lemma OAI.AtomicTriangular.FiniteCertificate.dBox12_mem line 3307
604. def OAI.AtomicTriangular.FiniteCertificate.restBox13 line 3314
605. lemma OAI.AtomicTriangular.FiniteCertificate.restBox13_calc line 3346
606. lemma OAI.AtomicTriangular.FiniteCertificate.restBox13_mem line 3349
607. def OAI.AtomicTriangular.FiniteCertificate.cBox13 line 3355
608. lemma OAI.AtomicTriangular.FiniteCertificate.cBox13_calc line 3387
609. lemma OAI.AtomicTriangular.FiniteCertificate.cBox13_mem line 3390
610. def OAI.AtomicTriangular.FiniteCertificate.dBox13 line 3393
611. lemma OAI.AtomicTriangular.FiniteCertificate.dBox13_calc line 3425
612. lemma OAI.AtomicTriangular.FiniteCertificate.dBox13_mem line 3428
613. def OAI.AtomicTriangular.FiniteCertificate.restBox16 line 3435
614. lemma OAI.AtomicTriangular.FiniteCertificate.restBox16_calc line 3467
615. lemma OAI.AtomicTriangular.FiniteCertificate.restBox16_mem line 3470
616. def OAI.AtomicTriangular.FiniteCertificate.cBox16 line 3476
617. lemma OAI.AtomicTriangular.FiniteCertificate.cBox16_calc line 3508
618. lemma OAI.AtomicTriangular.FiniteCertificate.cBox16_mem line 3511
619. def OAI.AtomicTriangular.FiniteCertificate.dBox16 line 3514
620. lemma OAI.AtomicTriangular.FiniteCertificate.dBox16_calc line 3546
621. lemma OAI.AtomicTriangular.FiniteCertificate.dBox16_mem line 3549
622. def OAI.AtomicTriangular.FiniteCertificate.restBox19 line 3556
623. lemma OAI.AtomicTriangular.FiniteCertificate.restBox19_calc line 3588
624. lemma OAI.AtomicTriangular.FiniteCertificate.restBox19_mem line 3591
625. def OAI.AtomicTriangular.FiniteCertificate.cBox19 line 3597
626. lemma OAI.AtomicTriangular.FiniteCertificate.cBox19_calc line 3629
627. lemma OAI.AtomicTriangular.FiniteCertificate.cBox19_mem line 3632
628. def OAI.AtomicTriangular.FiniteCertificate.dBox19 line 3635
629. lemma OAI.AtomicTriangular.FiniteCertificate.dBox19_calc line 3667
630. lemma OAI.AtomicTriangular.FiniteCertificate.dBox19_mem line 3670
631. def OAI.AtomicTriangular.FiniteCertificate.restBox21 line 3677
632. lemma OAI.AtomicTriangular.FiniteCertificate.restBox21_calc line 3709
633. lemma OAI.AtomicTriangular.FiniteCertificate.restBox21_mem line 3712
634. def OAI.AtomicTriangular.FiniteCertificate.cBox21 line 3718
635. lemma OAI.AtomicTriangular.FiniteCertificate.cBox21_calc line 3750
636. lemma OAI.AtomicTriangular.FiniteCertificate.cBox21_mem line 3753
637. def OAI.AtomicTriangular.FiniteCertificate.dBox21 line 3756
638. lemma OAI.AtomicTriangular.FiniteCertificate.dBox21_calc line 3788
639. lemma OAI.AtomicTriangular.FiniteCertificate.dBox21_mem line 3791
640. def OAI.AtomicTriangular.Construction.damping line 3805
641. lemma OAI.AtomicTriangular.Construction.b_pos line 3806
642. lemma OAI.AtomicTriangular.Construction.b_sq line 3807
643. lemma OAI.AtomicTriangular.Construction.damping_pos line 3811
644. lemma OAI.AtomicTriangular.Construction.waveDen_pos line 3815
645. lemma OAI.AtomicTriangular.Construction.transformedWave_hasDeriv line 3818
646. lemma OAI.AtomicTriangular.Construction.complex_gaussian_transform line 3824
647. def OAI.AtomicTriangular.Construction.spectralParameter line 3846
648. lemma OAI.AtomicTriangular.Construction.spectralParameter_pos line 3847
649. lemma OAI.AtomicTriangular.Construction.spectralParameter_inv line 3849
650. lemma OAI.AtomicTriangular.Construction.spectral_exponent line 3862
651. lemma OAI.AtomicTriangular.Construction.transformed_spectral_wave line 3878
652. def OAI.AtomicTriangular.FiniteCertificate.bBox line 3903
653. lemma OAI.AtomicTriangular.FiniteCertificate.bBox_mem line 3906
654. def OAI.AtomicTriangular.FiniteCertificate.dampingBox line 3915
655. lemma OAI.AtomicTriangular.FiniteCertificate.dampingBox_mem line 3916
656. def OAI.AtomicTriangular.FiniteCertificate.realFrequencyBox line 3921
657. lemma OAI.AtomicTriangular.FiniteCertificate.realFrequencyBox_mem line 3922
658. def OAI.AtomicTriangular.FiniteCertificate.denBox line 3927
659. lemma OAI.AtomicTriangular.FiniteCertificate.denBox_mem line 3929
660. lemma OAI.AtomicTriangular.FiniteCertificate.denBox_pos line 3932
661. lemma OAI.AtomicTriangular.FiniteCertificate.bdenBox_pos line 3935
662. def OAI.AtomicTriangular.FiniteCertificate.xwaveBox line 3939
663. lemma OAI.AtomicTriangular.FiniteCertificate.xwaveBox_mem line 3941
664. def OAI.AtomicTriangular.FiniteCertificate.lambdaBox line 3948
665. lemma OAI.AtomicTriangular.FiniteCertificate.lambdaBox_mem line 3951
666. def OAI.AtomicTriangular.FiniteCertificate.zetaBox line 3959
667. lemma OAI.AtomicTriangular.FiniteCertificate.zetaBox_mem line 3962
668. def OAI.AtomicTriangular.FiniteCertificate.wavePhaseBox line 3970
669. lemma OAI.AtomicTriangular.FiniteCertificate.wavePhaseBox_mem line 3972