OAI/Analysis/PlanarPacking/Certificate/TableList.lean

GitHub source file

11 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. lemma OAI.SharpPlanar.tableRaw_large line 15
  2. lemma OAI.SharpPlanar.tableC_large line 18
  3. lemma OAI.SharpPlanar.tableD_large line 20
  4. def OAI.SharpPlanar.tableCoords line 22
  5. lemma OAI.SharpPlanar.tableCoords_mem line 24
  6. def OAI.SharpPlanar.tableList line 41
  7. lemma OAI.SharpPlanar.tableList_apply line 42
  8. def OAI.SharpPlanar.tableData line 44
  9. lemma OAI.SharpPlanar.tableData_false line 46
  10. lemma OAI.SharpPlanar.tableData_true line 48
  11. lemma OAI.SharpPlanar.tableList_discard line 50