OAI/Analysis/PlanarPacking/Certificate/TableDensity1Panel3.lean

GitHub source file

34 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.density1_r3_0 line 14
  2. lemma OAI.SharpPlanar.CachedData.density1_r3_0_eq line 15
  3. def OAI.SharpPlanar.CachedData.density1_r3_1 line 16
  4. lemma OAI.SharpPlanar.CachedData.density1_r3_1_eq line 17
  5. def OAI.SharpPlanar.CachedData.density1_r3_2 line 18
  6. lemma OAI.SharpPlanar.CachedData.density1_r3_2_eq line 19
  7. def OAI.SharpPlanar.CachedData.density1_r3_3 line 20
  8. lemma OAI.SharpPlanar.CachedData.density1_r3_3_eq line 21
  9. def OAI.SharpPlanar.CachedData.density1_r3_4 line 22
  10. lemma OAI.SharpPlanar.CachedData.density1_r3_4_eq line 23
  11. def OAI.SharpPlanar.CachedData.density1_r3_5 line 24
  12. lemma OAI.SharpPlanar.CachedData.density1_r3_5_eq line 25
  13. def OAI.SharpPlanar.CachedData.density1_r3_6 line 26
  14. lemma OAI.SharpPlanar.CachedData.density1_r3_6_eq line 27
  15. def OAI.SharpPlanar.CachedData.density1_r3_7 line 28
  16. lemma OAI.SharpPlanar.CachedData.density1_r3_7_eq line 29
  17. def OAI.SharpPlanar.CachedData.density1_r3_8 line 30
  18. lemma OAI.SharpPlanar.CachedData.density1_r3_8_eq line 31
  19. def OAI.SharpPlanar.CachedData.density1_r3_9 line 32
  20. lemma OAI.SharpPlanar.CachedData.density1_r3_9_eq line 33
  21. def OAI.SharpPlanar.CachedData.density1_r3_10 line 34
  22. lemma OAI.SharpPlanar.CachedData.density1_r3_10_eq line 35
  23. def OAI.SharpPlanar.CachedData.density1_r3_11 line 36
  24. lemma OAI.SharpPlanar.CachedData.density1_r3_11_eq line 37
  25. def OAI.SharpPlanar.CachedData.density1_r3_12 line 38
  26. lemma OAI.SharpPlanar.CachedData.density1_r3_12_eq line 39
  27. def OAI.SharpPlanar.CachedData.density1_r3_13 line 40
  28. lemma OAI.SharpPlanar.CachedData.density1_r3_13_eq line 41
  29. def OAI.SharpPlanar.CachedData.density1_r3_14 line 42
  30. lemma OAI.SharpPlanar.CachedData.density1_r3_14_eq line 43
  31. def OAI.SharpPlanar.CachedData.density1_r3_15 line 44
  32. lemma OAI.SharpPlanar.CachedData.density1_r3_15_eq line 45
  33. def OAI.SharpPlanar.CachedData.density1_r3 line 46
  34. lemma OAI.SharpPlanar.CachedData.density1_r3_eq line 47