OAI/Analysis/PlanarPacking/Nodes.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpPlanar.sinTable line 7
  2. def OAI.SharpPlanar.cosTable line 11
  3. lemma OAI.SharpPlanar.trig_table line 16
  4. lemma OAI.SharpPlanar.squared_sine_to_cos line 31
  5. lemma OAI.SharpPlanar.divided_cos_to_double line 35
  6. lemma OAI.SharpPlanar.Q_as_table line 45
  7. lemma OAI.SharpPlanar.D_as_table line 60
  8. lemma OAI.SharpPlanar.b_lt_one line 75
  9. lemma OAI.SharpPlanar.b_pow_even line 76
  10. lemma OAI.SharpPlanar.b_pow_odd line 77
  11. lemma OAI.SharpPlanar.b_pow_3 line 78
  12. lemma OAI.SharpPlanar.b_pow_4 line 79
  13. lemma OAI.SharpPlanar.b_pow_5 line 80
  14. lemma OAI.SharpPlanar.b_pow_6 line 81
  15. lemma OAI.SharpPlanar.b_pow_7 line 82
  16. lemma OAI.SharpPlanar.b_pow_8 line 83
  17. lemma OAI.SharpPlanar.b_pow_9 line 84
  18. lemma OAI.SharpPlanar.b_pow_10 line 85
  19. lemma OAI.SharpPlanar.Q_0 line 87
  20. lemma OAI.SharpPlanar.Q_1 line 95
  21. lemma OAI.SharpPlanar.Q_3 line 103
  22. lemma OAI.SharpPlanar.Q_4 line 109
  23. lemma OAI.SharpPlanar.Q_7 line 117
  24. lemma OAI.SharpPlanar.Q_9 line 125
  25. lemma OAI.SharpPlanar.one_sub_b_ne line 131
  26. lemma OAI.SharpPlanar.one_add_b_ne line 132
  27. lemma OAI.SharpPlanar.D_0 line 134
  28. lemma OAI.SharpPlanar.D_1 line 146
  29. lemma OAI.SharpPlanar.D_3 line 158
  30. lemma OAI.SharpPlanar.D_4 line 170
  31. lemma OAI.SharpPlanar.D_7 line 182
  32. lemma OAI.SharpPlanar.D_9 line 194
  33. lemma OAI.SharpPlanar.b_lt_thirteen_fifteenths line 206
  34. lemma OAI.SharpPlanar.pi_lower line 207
  35. lemma OAI.SharpPlanar.pi_upper line 208
  36. lemma OAI.SharpPlanar.Q_small_lower line 210
  37. theorem OAI.SharpPlanar.Q_lower line 219
  38. theorem OAI.SharpPlanar.D_abs_bound line 235