OAI/Analysis/PlanarPacking/Certificate/TableDensityValues.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. def OAI.SharpPlanar.CachedData.density0 line 25
  2. lemma OAI.SharpPlanar.CachedData.density0_eq line 26
  3. lemma OAI.SharpPlanar.CachedData.density0_contains line 34
  4. def OAI.SharpPlanar.CachedData.density1 line 38
  5. lemma OAI.SharpPlanar.CachedData.density1_eq line 39
  6. lemma OAI.SharpPlanar.CachedData.density1_contains line 47