OAI/Analysis/PlanarPacking/Certificate/WUCert69.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.Numerical.U69.node line 15
  2. def OAI.SharpPlanar.Numerical.U69.umat line 16
  3. def OAI.SharpPlanar.Numerical.U69.entry0_0 line 17
  4. lemma OAI.SharpPlanar.Numerical.U69.entry0_0_contains line 18
  5. def OAI.SharpPlanar.Numerical.U69.entry3_0 line 25
  6. lemma OAI.SharpPlanar.Numerical.U69.entry3_0_contains line 26
  7. def OAI.SharpPlanar.Numerical.U69.entry1_0 line 33
  8. lemma OAI.SharpPlanar.Numerical.U69.entry1_0_contains line 34
  9. def OAI.SharpPlanar.Numerical.U69.entry4_0 line 41
  10. lemma OAI.SharpPlanar.Numerical.U69.entry4_0_contains line 42
  11. def OAI.SharpPlanar.Numerical.U69.entry2_0 line 49
  12. lemma OAI.SharpPlanar.Numerical.U69.entry2_0_contains line 50
  13. def OAI.SharpPlanar.Numerical.U69.entry5_0 line 57
  14. lemma OAI.SharpPlanar.Numerical.U69.entry5_0_contains line 58
  15. def OAI.SharpPlanar.Numerical.U69.entry0_1 line 65
  16. lemma OAI.SharpPlanar.Numerical.U69.entry0_1_contains line 66
  17. def OAI.SharpPlanar.Numerical.U69.entry3_1 line 73
  18. lemma OAI.SharpPlanar.Numerical.U69.entry3_1_contains line 74
  19. def OAI.SharpPlanar.Numerical.U69.entry1_1 line 81
  20. lemma OAI.SharpPlanar.Numerical.U69.entry1_1_contains line 82
  21. def OAI.SharpPlanar.Numerical.U69.entry4_1 line 89
  22. lemma OAI.SharpPlanar.Numerical.U69.entry4_1_contains line 90
  23. def OAI.SharpPlanar.Numerical.U69.entry2_1 line 97
  24. lemma OAI.SharpPlanar.Numerical.U69.entry2_1_contains line 98
  25. def OAI.SharpPlanar.Numerical.U69.entry5_1 line 105
  26. lemma OAI.SharpPlanar.Numerical.U69.entry5_1_contains line 106
  27. def OAI.SharpPlanar.Numerical.U69.entries line 113
  28. lemma OAI.SharpPlanar.Numerical.U69.entries_contains line 119
  29. def OAI.SharpPlanar.Numerical.U69.wuplusBox line 133
  30. lemma OAI.SharpPlanar.Numerical.U69.wuplus_contains line 134
  31. lemma OAI.SharpPlanar.Numerical.U69.wuplus_column line 135
  32. def OAI.SharpPlanar.Numerical.U69.wuminusBox line 140
  33. lemma OAI.SharpPlanar.Numerical.U69.wuminus_contains line 141
  34. lemma OAI.SharpPlanar.Numerical.U69.wuminus_column line 142