OAI/Analysis/PlanarPacking/Certificate/Residual13.lean

GitHub source file

13 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.Residual13.node line 15
  2. def OAI.SharpPlanar.Residual13.box0_0 line 16
  3. lemma OAI.SharpPlanar.Residual13.contains0_0 line 17
  4. lemma OAI.SharpPlanar.Residual13.bound0_0 line 23
  5. def OAI.SharpPlanar.Residual13.box0_1 line 25
  6. lemma OAI.SharpPlanar.Residual13.contains0_1 line 26
  7. lemma OAI.SharpPlanar.Residual13.bound0_1 line 33
  8. def OAI.SharpPlanar.Residual13.box1_0 line 35
  9. lemma OAI.SharpPlanar.Residual13.contains1_0 line 36
  10. lemma OAI.SharpPlanar.Residual13.bound1_0 line 42
  11. def OAI.SharpPlanar.Residual13.box1_1 line 44
  12. lemma OAI.SharpPlanar.Residual13.contains1_1 line 45
  13. lemma OAI.SharpPlanar.Residual13.bound1_1 line 52