OAI/Analysis/PlanarPacking/Certificate/WCertificates.lean

GitHub source file

22 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.WplusInt line 16
  2. def OAI.SharpPlanar.Numerical.Wplus line 22
  3. def OAI.SharpPlanar.Numerical.WplusBox line 23
  4. lemma OAI.SharpPlanar.Numerical.WplusBox_contains line 24
  5. def OAI.SharpPlanar.Numerical.Aplus line 25
  6. def OAI.SharpPlanar.Numerical.AplusBox line 26
  7. lemma OAI.SharpPlanar.Numerical.AplusBox_contains line 27
  8. def OAI.SharpPlanar.Numerical.defectplusBox line 31
  9. lemma OAI.SharpPlanar.Numerical.defectplusBox_contains line 32
  10. lemma OAI.SharpPlanar.Numerical.defectplus_column line 36
  11. lemma OAI.SharpPlanar.Numerical.Wplus_column line 41
  12. def OAI.SharpPlanar.Numerical.WminusInt line 45
  13. def OAI.SharpPlanar.Numerical.Wminus line 51
  14. def OAI.SharpPlanar.Numerical.WminusBox line 52
  15. lemma OAI.SharpPlanar.Numerical.WminusBox_contains line 53
  16. def OAI.SharpPlanar.Numerical.Aminus line 54
  17. def OAI.SharpPlanar.Numerical.AminusBox line 55
  18. lemma OAI.SharpPlanar.Numerical.AminusBox_contains line 56
  19. def OAI.SharpPlanar.Numerical.defectminusBox line 60
  20. lemma OAI.SharpPlanar.Numerical.defectminusBox_contains line 61
  21. lemma OAI.SharpPlanar.Numerical.defectminus_column line 65
  22. lemma OAI.SharpPlanar.Numerical.Wminus_column line 70