OAI/Analysis/PlanarPacking/Certificate/MixedBound40.lean

GitHub source file

10 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_40_4 line 14
  2. lemma OAI.SharpPlanar.mixed_40_5 line 17
  3. lemma OAI.SharpPlanar.mixed_40_6 line 20
  4. lemma OAI.SharpPlanar.mixed_40_7 line 23
  5. lemma OAI.SharpPlanar.mixed_40_8 line 26
  6. lemma OAI.SharpPlanar.mixed_40_9 line 29
  7. lemma OAI.SharpPlanar.mixed_40_10 line 32
  8. lemma OAI.SharpPlanar.mixed_40_11 line 35
  9. lemma OAI.SharpPlanar.mixed_40_12 line 38
  10. lemma OAI.SharpPlanar.mixed_40_13 line 41