OAI/Analysis/PlanarPacking/Certificate/Bernstein0.lean

GitHub source file

119 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.Bernstein0.N1_right.t0 line 23
  2. lemma OAI.SharpPlanar.Bernstein0.N1_right.t0_checked line 24
  3. lemma OAI.SharpPlanar.Bernstein0.N1_right.t0_contains line 25
  4. def OAI.SharpPlanar.Bernstein0.N1_right.t1 line 29
  5. lemma OAI.SharpPlanar.Bernstein0.N1_right.t1_checked line 30
  6. lemma OAI.SharpPlanar.Bernstein0.N1_right.t1_contains line 31
  7. def OAI.SharpPlanar.Bernstein0.N1_right.t2 line 35
  8. lemma OAI.SharpPlanar.Bernstein0.N1_right.t2_checked line 36
  9. lemma OAI.SharpPlanar.Bernstein0.N1_right.t2_contains line 37
  10. def OAI.SharpPlanar.Bernstein0.N1_right.t3 line 41
  11. lemma OAI.SharpPlanar.Bernstein0.N1_right.t3_checked line 42
  12. lemma OAI.SharpPlanar.Bernstein0.N1_right.t3_contains line 43
  13. def OAI.SharpPlanar.Bernstein0.N1_right.t4 line 47
  14. lemma OAI.SharpPlanar.Bernstein0.N1_right.t4_checked line 48
  15. lemma OAI.SharpPlanar.Bernstein0.N1_right.t4_contains line 49
  16. def OAI.SharpPlanar.Bernstein0.N1_right.t5 line 53
  17. lemma OAI.SharpPlanar.Bernstein0.N1_right.t5_checked line 54
  18. lemma OAI.SharpPlanar.Bernstein0.N1_right.t5_contains line 55
  19. def OAI.SharpPlanar.Bernstein0.N1_right.t6 line 59
  20. lemma OAI.SharpPlanar.Bernstein0.N1_right.t6_checked line 60
  21. lemma OAI.SharpPlanar.Bernstein0.N1_right.t6_contains line 61
  22. def OAI.SharpPlanar.Bernstein0.N1_right.t7 line 65
  23. lemma OAI.SharpPlanar.Bernstein0.N1_right.t7_checked line 66
  24. lemma OAI.SharpPlanar.Bernstein0.N1_right.t7_contains line 67
  25. def OAI.SharpPlanar.Bernstein0.N1_right.t8 line 71
  26. lemma OAI.SharpPlanar.Bernstein0.N1_right.t8_checked line 72
  27. lemma OAI.SharpPlanar.Bernstein0.N1_right.t8_contains line 73
  28. def OAI.SharpPlanar.Bernstein0.N1_right.t9 line 77
  29. lemma OAI.SharpPlanar.Bernstein0.N1_right.t9_checked line 78
  30. lemma OAI.SharpPlanar.Bernstein0.N1_right.t9_contains line 79
  31. def OAI.SharpPlanar.Bernstein0.N1_right.t10 line 83
  32. lemma OAI.SharpPlanar.Bernstein0.N1_right.t10_checked line 84
  33. lemma OAI.SharpPlanar.Bernstein0.N1_right.t10_contains line 85
  34. def OAI.SharpPlanar.Bernstein0.N1_right.t11 line 89
  35. lemma OAI.SharpPlanar.Bernstein0.N1_right.t11_checked line 90
  36. lemma OAI.SharpPlanar.Bernstein0.N1_right.t11_contains line 91
  37. def OAI.SharpPlanar.Bernstein0.N1_right.t12 line 95
  38. lemma OAI.SharpPlanar.Bernstein0.N1_right.t12_checked line 96
  39. lemma OAI.SharpPlanar.Bernstein0.N1_right.t12_contains line 97
  40. def OAI.SharpPlanar.Bernstein0.N1_right.t13 line 101
  41. lemma OAI.SharpPlanar.Bernstein0.N1_right.t13_checked line 102
  42. lemma OAI.SharpPlanar.Bernstein0.N1_right.t13_contains line 103
  43. def OAI.SharpPlanar.Bernstein0.N1_right.t14 line 107
  44. lemma OAI.SharpPlanar.Bernstein0.N1_right.t14_checked line 108
  45. lemma OAI.SharpPlanar.Bernstein0.N1_right.t14_contains line 109
  46. def OAI.SharpPlanar.Bernstein0.N1_right.t15 line 113
  47. lemma OAI.SharpPlanar.Bernstein0.N1_right.t15_checked line 114
  48. lemma OAI.SharpPlanar.Bernstein0.N1_right.t15_contains line 115
  49. def OAI.SharpPlanar.Bernstein0.N1_right.t16 line 119
  50. lemma OAI.SharpPlanar.Bernstein0.N1_right.t16_checked line 120
  51. lemma OAI.SharpPlanar.Bernstein0.N1_right.t16_contains line 121
  52. def OAI.SharpPlanar.Bernstein0.N1_right.t17 line 125
  53. lemma OAI.SharpPlanar.Bernstein0.N1_right.t17_checked line 126
  54. lemma OAI.SharpPlanar.Bernstein0.N1_right.t17_contains line 127
  55. def OAI.SharpPlanar.Bernstein0.N1_right.t18 line 131
  56. lemma OAI.SharpPlanar.Bernstein0.N1_right.t18_checked line 132
  57. lemma OAI.SharpPlanar.Bernstein0.N1_right.t18_contains line 133
  58. def OAI.SharpPlanar.Bernstein0.N1_right.t19 line 137
  59. lemma OAI.SharpPlanar.Bernstein0.N1_right.t19_checked line 138
  60. lemma OAI.SharpPlanar.Bernstein0.N1_right.t19_contains line 139
  61. def OAI.SharpPlanar.Bernstein0.N1_right.t20 line 143
  62. lemma OAI.SharpPlanar.Bernstein0.N1_right.t20_checked line 144
  63. lemma OAI.SharpPlanar.Bernstein0.N1_right.t20_contains line 145
  64. def OAI.SharpPlanar.Bernstein0.N1_right.t21 line 149
  65. lemma OAI.SharpPlanar.Bernstein0.N1_right.t21_checked line 150
  66. lemma OAI.SharpPlanar.Bernstein0.N1_right.t21_contains line 151
  67. def OAI.SharpPlanar.Bernstein0.N1_right.t22 line 155
  68. lemma OAI.SharpPlanar.Bernstein0.N1_right.t22_checked line 156
  69. lemma OAI.SharpPlanar.Bernstein0.N1_right.t22_contains line 157
  70. def OAI.SharpPlanar.Bernstein0.N1_right.t23 line 161
  71. lemma OAI.SharpPlanar.Bernstein0.N1_right.t23_checked line 162
  72. lemma OAI.SharpPlanar.Bernstein0.N1_right.t23_contains line 163
  73. def OAI.SharpPlanar.Bernstein0.N1_right.t24 line 167
  74. lemma OAI.SharpPlanar.Bernstein0.N1_right.t24_checked line 168
  75. lemma OAI.SharpPlanar.Bernstein0.N1_right.t24_contains line 169
  76. def OAI.SharpPlanar.Bernstein0.N1_right.t25 line 173
  77. lemma OAI.SharpPlanar.Bernstein0.N1_right.t25_checked line 174
  78. lemma OAI.SharpPlanar.Bernstein0.N1_right.t25_contains line 175
  79. def OAI.SharpPlanar.Bernstein0.N1_right.t26 line 179
  80. lemma OAI.SharpPlanar.Bernstein0.N1_right.t26_checked line 180
  81. lemma OAI.SharpPlanar.Bernstein0.N1_right.t26_contains line 181
  82. def OAI.SharpPlanar.Bernstein0.N1_right.t27 line 185
  83. lemma OAI.SharpPlanar.Bernstein0.N1_right.t27_checked line 186
  84. lemma OAI.SharpPlanar.Bernstein0.N1_right.t27_contains line 187
  85. def OAI.SharpPlanar.Bernstein0.N1_right.t28 line 191
  86. lemma OAI.SharpPlanar.Bernstein0.N1_right.t28_checked line 192
  87. lemma OAI.SharpPlanar.Bernstein0.N1_right.t28_contains line 193
  88. def OAI.SharpPlanar.Bernstein0.N1_right.ts line 197
  89. lemma OAI.SharpPlanar.Bernstein0.N1_right.ts_contains line 198
  90. lemma OAI.SharpPlanar.Bernstein0.N1_right.bound0 line 229
  91. lemma OAI.SharpPlanar.Bernstein0.N1_right.bound1 line 231
  92. lemma OAI.SharpPlanar.Bernstein0.N1_right.bound2 line 233
  93. lemma OAI.SharpPlanar.Bernstein0.N1_right.bound3 line 235
  94. lemma OAI.SharpPlanar.Bernstein0.N1_right.bound4 line 237
  95. lemma OAI.SharpPlanar.Bernstein0.N1_right.bound5 line 239
  96. lemma OAI.SharpPlanar.Bernstein0.N1_right.bound6 line 241
  97. lemma OAI.SharpPlanar.Bernstein0.N1_right.bound7 line 243
  98. lemma OAI.SharpPlanar.Bernstein0.N1_right.bound8 line 245
  99. lemma OAI.SharpPlanar.Bernstein0.N1_right.bound9 line 247
  100. lemma OAI.SharpPlanar.Bernstein0.N1_right.bound10 line 249
  101. lemma OAI.SharpPlanar.Bernstein0.N1_right.bound11 line 251
  102. lemma OAI.SharpPlanar.Bernstein0.N1_right.bound12 line 253
  103. lemma OAI.SharpPlanar.Bernstein0.N1_right.bound13 line 255
  104. lemma OAI.SharpPlanar.Bernstein0.N1_right.bound14 line 257
  105. lemma OAI.SharpPlanar.Bernstein0.N1_right.bound15 line 259
  106. lemma OAI.SharpPlanar.Bernstein0.N1_right.bound16 line 261
  107. lemma OAI.SharpPlanar.Bernstein0.N1_right.bound17 line 263
  108. lemma OAI.SharpPlanar.Bernstein0.N1_right.bound18 line 265
  109. lemma OAI.SharpPlanar.Bernstein0.N1_right.bound19 line 267
  110. lemma OAI.SharpPlanar.Bernstein0.N1_right.bound20 line 269
  111. lemma OAI.SharpPlanar.Bernstein0.N1_right.bound21 line 271
  112. lemma OAI.SharpPlanar.Bernstein0.N1_right.bound22 line 273
  113. lemma OAI.SharpPlanar.Bernstein0.N1_right.bound23 line 275
  114. lemma OAI.SharpPlanar.Bernstein0.N1_right.bound24 line 277
  115. lemma OAI.SharpPlanar.Bernstein0.N1_right.bound25 line 279
  116. lemma OAI.SharpPlanar.Bernstein0.N1_right.bound26 line 281
  117. lemma OAI.SharpPlanar.Bernstein0.N1_right.bound27 line 283
  118. lemma OAI.SharpPlanar.Bernstein0.N1_right.bound28 line 285
  119. lemma OAI.SharpPlanar.Bernstein0.N1_right.bound line 287