OAI/Analysis/PlanarPacking/Certificate/DEntries.lean

GitHub source file

75 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.Dmat line 18
  2. def OAI.SharpPlanar.Numerical.dentry0_0 line 19
  3. lemma OAI.SharpPlanar.Numerical.dentry0_0_contains line 20
  4. def OAI.SharpPlanar.Numerical.dentry3_0 line 26
  5. lemma OAI.SharpPlanar.Numerical.dentry3_0_contains line 27
  6. def OAI.SharpPlanar.Numerical.dentry0_3 line 33
  7. lemma OAI.SharpPlanar.Numerical.dentry0_3_contains line 34
  8. def OAI.SharpPlanar.Numerical.dentry3_3 line 40
  9. lemma OAI.SharpPlanar.Numerical.dentry3_3_contains line 41
  10. def OAI.SharpPlanar.Numerical.dentry1_0 line 47
  11. lemma OAI.SharpPlanar.Numerical.dentry1_0_contains line 48
  12. def OAI.SharpPlanar.Numerical.dentry4_0 line 54
  13. lemma OAI.SharpPlanar.Numerical.dentry4_0_contains line 55
  14. def OAI.SharpPlanar.Numerical.dentry1_3 line 61
  15. lemma OAI.SharpPlanar.Numerical.dentry1_3_contains line 62
  16. def OAI.SharpPlanar.Numerical.dentry4_3 line 68
  17. lemma OAI.SharpPlanar.Numerical.dentry4_3_contains line 69
  18. def OAI.SharpPlanar.Numerical.dentry2_0 line 75
  19. lemma OAI.SharpPlanar.Numerical.dentry2_0_contains line 76
  20. def OAI.SharpPlanar.Numerical.dentry5_0 line 82
  21. lemma OAI.SharpPlanar.Numerical.dentry5_0_contains line 83
  22. def OAI.SharpPlanar.Numerical.dentry2_3 line 89
  23. lemma OAI.SharpPlanar.Numerical.dentry2_3_contains line 90
  24. def OAI.SharpPlanar.Numerical.dentry5_3 line 96
  25. lemma OAI.SharpPlanar.Numerical.dentry5_3_contains line 97
  26. def OAI.SharpPlanar.Numerical.dentry0_1 line 103
  27. lemma OAI.SharpPlanar.Numerical.dentry0_1_contains line 104
  28. def OAI.SharpPlanar.Numerical.dentry3_1 line 110
  29. lemma OAI.SharpPlanar.Numerical.dentry3_1_contains line 111
  30. def OAI.SharpPlanar.Numerical.dentry0_4 line 117
  31. lemma OAI.SharpPlanar.Numerical.dentry0_4_contains line 118
  32. def OAI.SharpPlanar.Numerical.dentry3_4 line 124
  33. lemma OAI.SharpPlanar.Numerical.dentry3_4_contains line 125
  34. def OAI.SharpPlanar.Numerical.dentry1_1 line 131
  35. lemma OAI.SharpPlanar.Numerical.dentry1_1_contains line 132
  36. def OAI.SharpPlanar.Numerical.dentry4_1 line 138
  37. lemma OAI.SharpPlanar.Numerical.dentry4_1_contains line 139
  38. def OAI.SharpPlanar.Numerical.dentry1_4 line 145
  39. lemma OAI.SharpPlanar.Numerical.dentry1_4_contains line 146
  40. def OAI.SharpPlanar.Numerical.dentry4_4 line 152
  41. lemma OAI.SharpPlanar.Numerical.dentry4_4_contains line 153
  42. def OAI.SharpPlanar.Numerical.dentry2_1 line 159
  43. lemma OAI.SharpPlanar.Numerical.dentry2_1_contains line 160
  44. def OAI.SharpPlanar.Numerical.dentry5_1 line 166
  45. lemma OAI.SharpPlanar.Numerical.dentry5_1_contains line 167
  46. def OAI.SharpPlanar.Numerical.dentry2_4 line 173
  47. lemma OAI.SharpPlanar.Numerical.dentry2_4_contains line 174
  48. def OAI.SharpPlanar.Numerical.dentry5_4 line 180
  49. lemma OAI.SharpPlanar.Numerical.dentry5_4_contains line 181
  50. def OAI.SharpPlanar.Numerical.dentry0_2 line 187
  51. lemma OAI.SharpPlanar.Numerical.dentry0_2_contains line 188
  52. def OAI.SharpPlanar.Numerical.dentry3_2 line 194
  53. lemma OAI.SharpPlanar.Numerical.dentry3_2_contains line 195
  54. def OAI.SharpPlanar.Numerical.dentry0_5 line 201
  55. lemma OAI.SharpPlanar.Numerical.dentry0_5_contains line 202
  56. def OAI.SharpPlanar.Numerical.dentry3_5 line 208
  57. lemma OAI.SharpPlanar.Numerical.dentry3_5_contains line 209
  58. def OAI.SharpPlanar.Numerical.dentry1_2 line 215
  59. lemma OAI.SharpPlanar.Numerical.dentry1_2_contains line 216
  60. def OAI.SharpPlanar.Numerical.dentry4_2 line 222
  61. lemma OAI.SharpPlanar.Numerical.dentry4_2_contains line 223
  62. def OAI.SharpPlanar.Numerical.dentry1_5 line 229
  63. lemma OAI.SharpPlanar.Numerical.dentry1_5_contains line 230
  64. def OAI.SharpPlanar.Numerical.dentry4_5 line 236
  65. lemma OAI.SharpPlanar.Numerical.dentry4_5_contains line 237
  66. def OAI.SharpPlanar.Numerical.dentry2_2 line 243
  67. lemma OAI.SharpPlanar.Numerical.dentry2_2_contains line 244
  68. def OAI.SharpPlanar.Numerical.dentry5_2 line 250
  69. lemma OAI.SharpPlanar.Numerical.dentry5_2_contains line 251
  70. def OAI.SharpPlanar.Numerical.dentry2_5 line 257
  71. lemma OAI.SharpPlanar.Numerical.dentry2_5_contains line 258
  72. def OAI.SharpPlanar.Numerical.dentry5_5 line 264
  73. lemma OAI.SharpPlanar.Numerical.dentry5_5_contains line 265
  74. def OAI.SharpPlanar.Numerical.dEntries line 271
  75. lemma OAI.SharpPlanar.Numerical.dEntries_contains line 277