OAI/Analysis/PlanarPacking/Certificate/LEntries.lean

GitHub source file

148 declarations, 0 contain sorry, 0 declared as axioms

Finite interval certificates for the planar Fourier construction

These rational enclosures certify the numerical bounds in the sharp planar Fourier construction of OpenAI. All interval endpoints are exact integers.

  1. def OAI.SharpPlanar.Numerical.Lmat line 22
  2. def OAI.SharpPlanar.Numerical.lentry0_0 line 23
  3. lemma OAI.SharpPlanar.Numerical.lentry0_0_contains line 24
  4. def OAI.SharpPlanar.Numerical.lentry6_0 line 31
  5. lemma OAI.SharpPlanar.Numerical.lentry6_0_contains line 32
  6. def OAI.SharpPlanar.Numerical.lentry1_0 line 39
  7. lemma OAI.SharpPlanar.Numerical.lentry1_0_contains line 40
  8. def OAI.SharpPlanar.Numerical.lentry7_0 line 47
  9. lemma OAI.SharpPlanar.Numerical.lentry7_0_contains line 48
  10. def OAI.SharpPlanar.Numerical.lentry2_0 line 55
  11. lemma OAI.SharpPlanar.Numerical.lentry2_0_contains line 56
  12. def OAI.SharpPlanar.Numerical.lentry8_0 line 63
  13. lemma OAI.SharpPlanar.Numerical.lentry8_0_contains line 64
  14. def OAI.SharpPlanar.Numerical.lentry3_0 line 71
  15. lemma OAI.SharpPlanar.Numerical.lentry3_0_contains line 72
  16. def OAI.SharpPlanar.Numerical.lentry9_0 line 79
  17. lemma OAI.SharpPlanar.Numerical.lentry9_0_contains line 80
  18. def OAI.SharpPlanar.Numerical.lentry4_0 line 87
  19. lemma OAI.SharpPlanar.Numerical.lentry4_0_contains line 88
  20. def OAI.SharpPlanar.Numerical.lentry10_0 line 95
  21. lemma OAI.SharpPlanar.Numerical.lentry10_0_contains line 96
  22. def OAI.SharpPlanar.Numerical.lentry5_0 line 103
  23. lemma OAI.SharpPlanar.Numerical.lentry5_0_contains line 104
  24. def OAI.SharpPlanar.Numerical.lentry11_0 line 111
  25. lemma OAI.SharpPlanar.Numerical.lentry11_0_contains line 112
  26. def OAI.SharpPlanar.Numerical.lentry0_3 line 119
  27. lemma OAI.SharpPlanar.Numerical.lentry0_3_contains line 120
  28. def OAI.SharpPlanar.Numerical.lentry6_3 line 127
  29. lemma OAI.SharpPlanar.Numerical.lentry6_3_contains line 128
  30. def OAI.SharpPlanar.Numerical.lentry1_3 line 135
  31. lemma OAI.SharpPlanar.Numerical.lentry1_3_contains line 136
  32. def OAI.SharpPlanar.Numerical.lentry7_3 line 143
  33. lemma OAI.SharpPlanar.Numerical.lentry7_3_contains line 144
  34. def OAI.SharpPlanar.Numerical.lentry2_3 line 151
  35. lemma OAI.SharpPlanar.Numerical.lentry2_3_contains line 152
  36. def OAI.SharpPlanar.Numerical.lentry8_3 line 159
  37. lemma OAI.SharpPlanar.Numerical.lentry8_3_contains line 160
  38. def OAI.SharpPlanar.Numerical.lentry3_3 line 167
  39. lemma OAI.SharpPlanar.Numerical.lentry3_3_contains line 168
  40. def OAI.SharpPlanar.Numerical.lentry9_3 line 175
  41. lemma OAI.SharpPlanar.Numerical.lentry9_3_contains line 176
  42. def OAI.SharpPlanar.Numerical.lentry4_3 line 183
  43. lemma OAI.SharpPlanar.Numerical.lentry4_3_contains line 184
  44. def OAI.SharpPlanar.Numerical.lentry10_3 line 191
  45. lemma OAI.SharpPlanar.Numerical.lentry10_3_contains line 192
  46. def OAI.SharpPlanar.Numerical.lentry5_3 line 199
  47. lemma OAI.SharpPlanar.Numerical.lentry5_3_contains line 200
  48. def OAI.SharpPlanar.Numerical.lentry11_3 line 207
  49. lemma OAI.SharpPlanar.Numerical.lentry11_3_contains line 208
  50. def OAI.SharpPlanar.Numerical.lentry0_1 line 215
  51. lemma OAI.SharpPlanar.Numerical.lentry0_1_contains line 216
  52. def OAI.SharpPlanar.Numerical.lentry6_1 line 223
  53. lemma OAI.SharpPlanar.Numerical.lentry6_1_contains line 224
  54. def OAI.SharpPlanar.Numerical.lentry1_1 line 231
  55. lemma OAI.SharpPlanar.Numerical.lentry1_1_contains line 232
  56. def OAI.SharpPlanar.Numerical.lentry7_1 line 239
  57. lemma OAI.SharpPlanar.Numerical.lentry7_1_contains line 240
  58. def OAI.SharpPlanar.Numerical.lentry2_1 line 247
  59. lemma OAI.SharpPlanar.Numerical.lentry2_1_contains line 248
  60. def OAI.SharpPlanar.Numerical.lentry8_1 line 255
  61. lemma OAI.SharpPlanar.Numerical.lentry8_1_contains line 256
  62. def OAI.SharpPlanar.Numerical.lentry3_1 line 263
  63. lemma OAI.SharpPlanar.Numerical.lentry3_1_contains line 264
  64. def OAI.SharpPlanar.Numerical.lentry9_1 line 271
  65. lemma OAI.SharpPlanar.Numerical.lentry9_1_contains line 272
  66. def OAI.SharpPlanar.Numerical.lentry4_1 line 279
  67. lemma OAI.SharpPlanar.Numerical.lentry4_1_contains line 280
  68. def OAI.SharpPlanar.Numerical.lentry10_1 line 287
  69. lemma OAI.SharpPlanar.Numerical.lentry10_1_contains line 288
  70. def OAI.SharpPlanar.Numerical.lentry5_1 line 295
  71. lemma OAI.SharpPlanar.Numerical.lentry5_1_contains line 296
  72. def OAI.SharpPlanar.Numerical.lentry11_1 line 303
  73. lemma OAI.SharpPlanar.Numerical.lentry11_1_contains line 304
  74. def OAI.SharpPlanar.Numerical.lentry0_4 line 311
  75. lemma OAI.SharpPlanar.Numerical.lentry0_4_contains line 312
  76. def OAI.SharpPlanar.Numerical.lentry6_4 line 319
  77. lemma OAI.SharpPlanar.Numerical.lentry6_4_contains line 320
  78. def OAI.SharpPlanar.Numerical.lentry1_4 line 327
  79. lemma OAI.SharpPlanar.Numerical.lentry1_4_contains line 328
  80. def OAI.SharpPlanar.Numerical.lentry7_4 line 335
  81. lemma OAI.SharpPlanar.Numerical.lentry7_4_contains line 336
  82. def OAI.SharpPlanar.Numerical.lentry2_4 line 343
  83. lemma OAI.SharpPlanar.Numerical.lentry2_4_contains line 344
  84. def OAI.SharpPlanar.Numerical.lentry8_4 line 351
  85. lemma OAI.SharpPlanar.Numerical.lentry8_4_contains line 352
  86. def OAI.SharpPlanar.Numerical.lentry3_4 line 359
  87. lemma OAI.SharpPlanar.Numerical.lentry3_4_contains line 360
  88. def OAI.SharpPlanar.Numerical.lentry9_4 line 367
  89. lemma OAI.SharpPlanar.Numerical.lentry9_4_contains line 368
  90. def OAI.SharpPlanar.Numerical.lentry4_4 line 375
  91. lemma OAI.SharpPlanar.Numerical.lentry4_4_contains line 376
  92. def OAI.SharpPlanar.Numerical.lentry10_4 line 383
  93. lemma OAI.SharpPlanar.Numerical.lentry10_4_contains line 384
  94. def OAI.SharpPlanar.Numerical.lentry5_4 line 391
  95. lemma OAI.SharpPlanar.Numerical.lentry5_4_contains line 392
  96. def OAI.SharpPlanar.Numerical.lentry11_4 line 399
  97. lemma OAI.SharpPlanar.Numerical.lentry11_4_contains line 400
  98. def OAI.SharpPlanar.Numerical.lentry0_2 line 407
  99. lemma OAI.SharpPlanar.Numerical.lentry0_2_contains line 408
  100. def OAI.SharpPlanar.Numerical.lentry6_2 line 415
  101. lemma OAI.SharpPlanar.Numerical.lentry6_2_contains line 416
  102. def OAI.SharpPlanar.Numerical.lentry1_2 line 423
  103. lemma OAI.SharpPlanar.Numerical.lentry1_2_contains line 424
  104. def OAI.SharpPlanar.Numerical.lentry7_2 line 431
  105. lemma OAI.SharpPlanar.Numerical.lentry7_2_contains line 432
  106. def OAI.SharpPlanar.Numerical.lentry2_2 line 439
  107. lemma OAI.SharpPlanar.Numerical.lentry2_2_contains line 440
  108. def OAI.SharpPlanar.Numerical.lentry8_2 line 447
  109. lemma OAI.SharpPlanar.Numerical.lentry8_2_contains line 448
  110. def OAI.SharpPlanar.Numerical.lentry3_2 line 455
  111. lemma OAI.SharpPlanar.Numerical.lentry3_2_contains line 456
  112. def OAI.SharpPlanar.Numerical.lentry9_2 line 463
  113. lemma OAI.SharpPlanar.Numerical.lentry9_2_contains line 464
  114. def OAI.SharpPlanar.Numerical.lentry4_2 line 471
  115. lemma OAI.SharpPlanar.Numerical.lentry4_2_contains line 472
  116. def OAI.SharpPlanar.Numerical.lentry10_2 line 479
  117. lemma OAI.SharpPlanar.Numerical.lentry10_2_contains line 480
  118. def OAI.SharpPlanar.Numerical.lentry5_2 line 487
  119. lemma OAI.SharpPlanar.Numerical.lentry5_2_contains line 488
  120. def OAI.SharpPlanar.Numerical.lentry11_2 line 495
  121. lemma OAI.SharpPlanar.Numerical.lentry11_2_contains line 496
  122. def OAI.SharpPlanar.Numerical.lentry0_5 line 503
  123. lemma OAI.SharpPlanar.Numerical.lentry0_5_contains line 504
  124. def OAI.SharpPlanar.Numerical.lentry6_5 line 511
  125. lemma OAI.SharpPlanar.Numerical.lentry6_5_contains line 512
  126. def OAI.SharpPlanar.Numerical.lentry1_5 line 519
  127. lemma OAI.SharpPlanar.Numerical.lentry1_5_contains line 520
  128. def OAI.SharpPlanar.Numerical.lentry7_5 line 527
  129. lemma OAI.SharpPlanar.Numerical.lentry7_5_contains line 528
  130. def OAI.SharpPlanar.Numerical.lentry2_5 line 535
  131. lemma OAI.SharpPlanar.Numerical.lentry2_5_contains line 536
  132. def OAI.SharpPlanar.Numerical.lentry8_5 line 543
  133. lemma OAI.SharpPlanar.Numerical.lentry8_5_contains line 544
  134. def OAI.SharpPlanar.Numerical.lentry3_5 line 551
  135. lemma OAI.SharpPlanar.Numerical.lentry3_5_contains line 552
  136. def OAI.SharpPlanar.Numerical.lentry9_5 line 559
  137. lemma OAI.SharpPlanar.Numerical.lentry9_5_contains line 560
  138. def OAI.SharpPlanar.Numerical.lentry4_5 line 567
  139. lemma OAI.SharpPlanar.Numerical.lentry4_5_contains line 568
  140. def OAI.SharpPlanar.Numerical.lentry10_5 line 575
  141. lemma OAI.SharpPlanar.Numerical.lentry10_5_contains line 576
  142. def OAI.SharpPlanar.Numerical.lentry5_5 line 583
  143. lemma OAI.SharpPlanar.Numerical.lentry5_5_contains line 584
  144. def OAI.SharpPlanar.Numerical.lentry11_5 line 591
  145. lemma OAI.SharpPlanar.Numerical.lentry11_5_contains line 592
  146. def OAI.SharpPlanar.Numerical.lEntries line 599
  147. lemma OAI.SharpPlanar.Numerical.lEntries_contains line 611
  148. lemma OAI.SharpPlanar.Numerical.Lmat_column line 685