OAI/Analysis/PlanarPacking/Certificate/MixedBound33.lean

GitHub source file

6 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.mixed_33_8 line 14
  2. lemma OAI.SharpPlanar.mixed_33_9 line 17
  3. lemma OAI.SharpPlanar.mixed_33_10 line 20
  4. lemma OAI.SharpPlanar.mixed_33_11 line 23
  5. lemma OAI.SharpPlanar.mixed_33_12 line 26
  6. lemma OAI.SharpPlanar.mixed_33_13 line 29