OAI/Analysis/PlanarPacking/AtomTail.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpPlanar.atomBase line 7
  2. lemma OAI.SharpPlanar.atomBase_pos line 8
  3. lemma OAI.SharpPlanar.atomBase_lt_one line 9
  4. lemma OAI.SharpPlanar.atomBase_contains line 10
  5. lemma OAI.SharpPlanar.decay_atomBase line 17
  6. def OAI.SharpPlanar.atomRowFactor line 23
  7. def OAI.SharpPlanar.atomRow line 24
  8. def OAI.SharpPlanar.atomRowTable line 26
  9. lemma OAI.SharpPlanar.atomRowFactor_nonneg line 28
  10. lemma OAI.SharpPlanar.atomRow_nonneg line 32
  11. lemma OAI.SharpPlanar.atomRow_period line 36
  12. lemma OAI.SharpPlanar.atomRow_tail_sum line 50
  13. def OAI.SharpPlanar.atomFactorRat line 59
  14. def OAI.SharpPlanar.atomRowRat line 60
  15. def OAI.SharpPlanar.atomTableRat line 62
  16. lemma OAI.SharpPlanar.atomFactorRat_nonneg line 63
  17. lemma OAI.SharpPlanar.atomRowFactor_le line 69
  18. lemma OAI.SharpPlanar.atomRow_le line 79
  19. lemma OAI.SharpPlanar.atomRowTable_le line 87
  20. lemma OAI.SharpPlanar.atomTableRat_hundred line 100
  21. lemma OAI.SharpPlanar.atomRowTable_hundred line 102