OAI/Analysis/PlanarPacking/Certificate/CoarseBound15.lean

GitHub source file

18 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_15_13 line 14
  2. lemma OAI.SharpPlanar.coarse_15_14 line 17
  3. lemma OAI.SharpPlanar.coarse_15_15 line 20
  4. lemma OAI.SharpPlanar.coarse_15_16 line 23
  5. lemma OAI.SharpPlanar.coarse_15_17 line 26
  6. lemma OAI.SharpPlanar.coarse_15_18 line 29
  7. lemma OAI.SharpPlanar.coarse_15_19 line 32
  8. lemma OAI.SharpPlanar.coarse_15_20 line 35
  9. lemma OAI.SharpPlanar.coarse_15_21 line 38
  10. lemma OAI.SharpPlanar.coarse_15_22 line 41
  11. lemma OAI.SharpPlanar.coarse_15_23 line 44
  12. lemma OAI.SharpPlanar.coarse_15_24 line 47
  13. lemma OAI.SharpPlanar.coarse_15_25 line 50
  14. lemma OAI.SharpPlanar.coarse_15_26 line 53
  15. lemma OAI.SharpPlanar.coarse_15_27 line 56
  16. lemma OAI.SharpPlanar.coarse_15_28 line 59
  17. lemma OAI.SharpPlanar.coarse_15_29 line 62
  18. lemma OAI.SharpPlanar.coarse_15_30 line 65