OAI/Analysis/PlanarPacking/Certificate/CoarseBound4.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.coarse_4_20 line 14
  2. lemma OAI.SharpPlanar.coarse_4_21 line 17
  3. lemma OAI.SharpPlanar.coarse_4_22 line 20
  4. lemma OAI.SharpPlanar.coarse_4_23 line 23
  5. lemma OAI.SharpPlanar.coarse_4_24 line 26
  6. lemma OAI.SharpPlanar.coarse_4_25 line 29
  7. lemma OAI.SharpPlanar.coarse_4_26 line 32
  8. lemma OAI.SharpPlanar.coarse_4_27 line 35
  9. lemma OAI.SharpPlanar.coarse_4_28 line 38
  10. lemma OAI.SharpPlanar.coarse_4_29 line 41
  11. lemma OAI.SharpPlanar.coarse_4_30 line 44