OAI/Analysis/PlanarPacking/Certificate/TableData.lean

GitHub source file

17 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.tableRaw line 18
  2. def OAI.SharpPlanar.tableC line 72
  3. def OAI.SharpPlanar.tableD line 76
  4. def OAI.SharpPlanar.tableConstant line 80
  5. def OAI.SharpPlanar.tableNodes line 82
  6. def OAI.SharpPlanar.tableAllNodes line 84
  7. def OAI.SharpPlanar.tableNorm line 86
  8. def OAI.SharpPlanar.tableTailNorm line 89
  9. lemma OAI.SharpPlanar.tableNorm_false line 92
  10. lemma OAI.SharpPlanar.tableNorm_true line 95
  11. lemma OAI.SharpPlanar.tableTailNorm_false line 98
  12. lemma OAI.SharpPlanar.tableTailNorm_true line 101
  13. lemma OAI.SharpPlanar.tableNorm_lt line 104
  14. lemma OAI.SharpPlanar.tableTailNorm_lt line 109
  15. def OAI.SharpPlanar.rationalTailLower line 115
  16. lemma OAI.SharpPlanar.rationalTailLower_false line 123
  17. lemma OAI.SharpPlanar.rationalTailLower_true line 126