OAI/Geometry/TranslativeCovering/CellCounts.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CellCounts.assignmentWeight line 33
  2. def OAI.CellCounts.injectiveSum line 36
  3. theorem OAI.CellCounts.sum_assignmentWeight line 39
  4. theorem OAI.CellCounts.assignmentWeight_nonneg line 44
  5. theorem OAI.CellCounts.injectiveSum_nonneg line 48
  6. theorem OAI.CellCounts.injectiveSum_le line 56
  7. def OAI.CellCounts.collisionSum line 65
  8. def OAI.CellCounts.force line 68
  9. theorem OAI.CellCounts.force_weight line 72
  10. theorem OAI.CellCounts.collision_decompose line 91
  11. theorem OAI.CellCounts.sum_force line 103
  12. theorem OAI.CellCounts.prod_erase_two line 108
  13. theorem OAI.CellCounts.collision_formula line 114
  14. def OAI.CellCounts.pairs line 129
  15. theorem OAI.CellCounts.noninjective_has_pair line 133
  16. theorem OAI.CellCounts.collision_union_bound line 143
  17. theorem OAI.CellCounts.prod_relative_error line 168
  18. theorem OAI.CellCounts.collision_error line 192
  19. theorem OAI.CellCounts.occupation_error line 239
  20. def OAI.CellCounts.slotWeight line 261
  21. theorem OAI.CellCounts.cell_collision_error line 264
  22. lemma OAI.CellCounts.injectiveSum_eq_embeddings line 325
  23. lemma OAI.CellCounts.assignmentWeight_slot line 334
  24. lemma OAI.CellCounts.injectiveSum_slot_eq line 348