OAI/Analysis/PlanarPacking/Certificate/TableDensityExpr.lean

GitHub source file

106 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.CachedData.allColumns line 24
  2. def OAI.SharpPlanar.CachedData.tableTerm line 78
  3. lemma OAI.SharpPlanar.CachedData.tableTerm0_contains line 79
  4. lemma OAI.SharpPlanar.CachedData.tableTerm1_contains line 84
  5. lemma OAI.SharpPlanar.CachedData.tableTerm2_contains line 89
  6. lemma OAI.SharpPlanar.CachedData.tableTerm3_contains line 92
  7. lemma OAI.SharpPlanar.CachedData.tableTerm4_contains line 97
  8. lemma OAI.SharpPlanar.CachedData.tableTerm5_contains line 102
  9. lemma OAI.SharpPlanar.CachedData.tableTerm6_contains line 105
  10. lemma OAI.SharpPlanar.CachedData.tableTerm7_contains line 108
  11. lemma OAI.SharpPlanar.CachedData.tableTerm8_contains line 113
  12. lemma OAI.SharpPlanar.CachedData.tableTerm9_contains line 116
  13. lemma OAI.SharpPlanar.CachedData.tableTerm10_contains line 121
  14. lemma OAI.SharpPlanar.CachedData.tableTerm11_contains line 124
  15. lemma OAI.SharpPlanar.CachedData.tableTerm12_contains line 127
  16. lemma OAI.SharpPlanar.CachedData.tableTerm13_contains line 132
  17. lemma OAI.SharpPlanar.CachedData.tableTerm14_contains line 137
  18. lemma OAI.SharpPlanar.CachedData.tableTerm15_contains line 140
  19. lemma OAI.SharpPlanar.CachedData.tableTerm16_contains line 145
  20. lemma OAI.SharpPlanar.CachedData.tableTerm17_contains line 150
  21. lemma OAI.SharpPlanar.CachedData.tableTerm18_contains line 153
  22. lemma OAI.SharpPlanar.CachedData.tableTerm19_contains line 156
  23. lemma OAI.SharpPlanar.CachedData.tableTerm20_contains line 161
  24. lemma OAI.SharpPlanar.CachedData.tableTerm21_contains line 164
  25. lemma OAI.SharpPlanar.CachedData.tableTerm22_contains line 169
  26. lemma OAI.SharpPlanar.CachedData.tableTerm23_contains line 172
  27. lemma OAI.SharpPlanar.CachedData.tableTerm24_contains line 175
  28. lemma OAI.SharpPlanar.CachedData.tableTerm25_contains line 180
  29. lemma OAI.SharpPlanar.CachedData.tableTerm26_contains line 185
  30. lemma OAI.SharpPlanar.CachedData.tableTerm27_contains line 188
  31. lemma OAI.SharpPlanar.CachedData.tableTerm28_contains line 193
  32. lemma OAI.SharpPlanar.CachedData.tableTerm29_contains line 198
  33. lemma OAI.SharpPlanar.CachedData.tableTerm30_contains line 201
  34. lemma OAI.SharpPlanar.CachedData.tableTerm31_contains line 204
  35. lemma OAI.SharpPlanar.CachedData.tableTerm32_contains line 209
  36. lemma OAI.SharpPlanar.CachedData.tableTerm33_contains line 212
  37. lemma OAI.SharpPlanar.CachedData.tableTerm34_contains line 217
  38. lemma OAI.SharpPlanar.CachedData.tableTerm35_contains line 220
  39. lemma OAI.SharpPlanar.CachedData.tableTerm36_contains line 223
  40. lemma OAI.SharpPlanar.CachedData.tableTerm37_contains line 228
  41. lemma OAI.SharpPlanar.CachedData.tableTerm38_contains line 233
  42. lemma OAI.SharpPlanar.CachedData.tableTerm39_contains line 236
  43. lemma OAI.SharpPlanar.CachedData.tableTerm40_contains line 241
  44. lemma OAI.SharpPlanar.CachedData.tableTerm41_contains line 246
  45. lemma OAI.SharpPlanar.CachedData.tableTerm42_contains line 249
  46. lemma OAI.SharpPlanar.CachedData.tableTerm43_contains line 252
  47. lemma OAI.SharpPlanar.CachedData.tableTerm44_contains line 257
  48. lemma OAI.SharpPlanar.CachedData.tableTerm45_contains line 260
  49. lemma OAI.SharpPlanar.CachedData.tableTerm46_contains line 265
  50. lemma OAI.SharpPlanar.CachedData.tableTerm47_contains line 268
  51. lemma OAI.SharpPlanar.CachedData.tableTerm48_contains line 271
  52. lemma OAI.SharpPlanar.CachedData.tableTerm49_contains line 276
  53. lemma OAI.SharpPlanar.CachedData.tableTerm50_contains line 281
  54. lemma OAI.SharpPlanar.CachedData.tableTerm51_contains line 284
  55. lemma OAI.SharpPlanar.CachedData.tableTerm52_contains line 289
  56. lemma OAI.SharpPlanar.CachedData.tableTerm53_contains line 294
  57. lemma OAI.SharpPlanar.CachedData.tableTerm54_contains line 297
  58. lemma OAI.SharpPlanar.CachedData.tableTerm55_contains line 300
  59. lemma OAI.SharpPlanar.CachedData.tableTerm56_contains line 305
  60. lemma OAI.SharpPlanar.CachedData.tableTerm57_contains line 308
  61. lemma OAI.SharpPlanar.CachedData.tableTerm58_contains line 313
  62. lemma OAI.SharpPlanar.CachedData.tableTerm59_contains line 316
  63. lemma OAI.SharpPlanar.CachedData.tableTerm60_contains line 319
  64. lemma OAI.SharpPlanar.CachedData.tableTerm61_contains line 324
  65. lemma OAI.SharpPlanar.CachedData.tableTerm62_contains line 329
  66. lemma OAI.SharpPlanar.CachedData.tableTerm63_contains line 332
  67. lemma OAI.SharpPlanar.CachedData.tableTerm64_contains line 337
  68. lemma OAI.SharpPlanar.CachedData.tableTerm65_contains line 342
  69. lemma OAI.SharpPlanar.CachedData.tableTerm66_contains line 345
  70. lemma OAI.SharpPlanar.CachedData.tableTerm67_contains line 348
  71. lemma OAI.SharpPlanar.CachedData.tableTerm68_contains line 353
  72. lemma OAI.SharpPlanar.CachedData.tableTerm69_contains line 356
  73. lemma OAI.SharpPlanar.CachedData.tableTerm70_contains line 361
  74. lemma OAI.SharpPlanar.CachedData.tableTerm71_contains line 364
  75. lemma OAI.SharpPlanar.CachedData.tableTerm72_contains line 367
  76. lemma OAI.SharpPlanar.CachedData.tableTerm73_contains line 372
  77. lemma OAI.SharpPlanar.CachedData.tableTerm74_contains line 377
  78. lemma OAI.SharpPlanar.CachedData.tableTerm75_contains line 380
  79. lemma OAI.SharpPlanar.CachedData.tableTerm76_contains line 385
  80. lemma OAI.SharpPlanar.CachedData.tableTerm77_contains line 390
  81. lemma OAI.SharpPlanar.CachedData.tableTerm78_contains line 393
  82. lemma OAI.SharpPlanar.CachedData.tableTerm79_contains line 396
  83. lemma OAI.SharpPlanar.CachedData.tableTerm80_contains line 401
  84. lemma OAI.SharpPlanar.CachedData.tableTerm81_contains line 404
  85. lemma OAI.SharpPlanar.CachedData.tableTerm82_contains line 409
  86. lemma OAI.SharpPlanar.CachedData.tableTerm83_contains line 412
  87. lemma OAI.SharpPlanar.CachedData.tableTerm84_contains line 415
  88. lemma OAI.SharpPlanar.CachedData.tableTerm85_contains line 420
  89. lemma OAI.SharpPlanar.CachedData.tableTerm86_contains line 425
  90. lemma OAI.SharpPlanar.CachedData.tableTerm87_contains line 428
  91. lemma OAI.SharpPlanar.CachedData.tableTerm88_contains line 433
  92. lemma OAI.SharpPlanar.CachedData.tableTerm89_contains line 438
  93. lemma OAI.SharpPlanar.CachedData.tableTerm90_contains line 441
  94. lemma OAI.SharpPlanar.CachedData.tableTerm91_contains line 444
  95. lemma OAI.SharpPlanar.CachedData.tableTerm92_contains line 449
  96. lemma OAI.SharpPlanar.CachedData.tableTerm93_contains line 452
  97. lemma OAI.SharpPlanar.CachedData.tableTerm94_contains line 457
  98. lemma OAI.SharpPlanar.CachedData.tableTerm95_contains line 460
  99. lemma OAI.SharpPlanar.CachedData.tableTerm96_contains line 463
  100. lemma OAI.SharpPlanar.CachedData.tableTerm97_contains line 468
  101. lemma OAI.SharpPlanar.CachedData.tableTerm98_contains line 473
  102. lemma OAI.SharpPlanar.CachedData.tableTerm99_contains line 476
  103. lemma OAI.SharpPlanar.CachedData.tableTerm100_contains line 481
  104. lemma OAI.SharpPlanar.CachedData.tableTerm_contains line 486
  105. def OAI.SharpPlanar.CachedData.density0Expr line 590
  106. def OAI.SharpPlanar.CachedData.density1Expr line 591