OAI/Analysis/HardSphere/PathBounds/VisitPacking.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.FreeVisits.packingBox line 14
  2. lemma OAI.HardSphere.FreeVisits.card_packingBox line 17
  3. lemma OAI.HardSphere.FreeVisits.site_packing_witness line 25
  4. lemma OAI.HardSphere.FreeVisits.card_near_sites_le line 51
  5. def OAI.HardSphere.pathVisitsBall line 68
  6. lemma OAI.HardSphere.pathVisitsBall_isClosed line 72
  7. lemma OAI.HardSphere.pathVisitsBall_reverse line 90
  8. def OAI.HardSphere.pathVisitedSites line 100
  9. lemma OAI.HardSphere.pathVisitedSites_measurable line 105
  10. lemma OAI.HardSphere.pathVisitedSites_reverse line 115
  11. lemma OAI.HardSphere.FreeVisits.visited_subset_near line 126
  12. lemma OAI.HardSphere.FreeVisits.visited_card_le_of_short line 139
  13. lemma OAI.HardSphere.FreeVisits.visited_split line 145
  14. lemma OAI.HardSphere.FreeVisits.visited_card_split_le line 178
  15. lemma OAI.HardSphere.FreeVisits.freeTrajectory_coord_dist_le line 187
  16. lemma OAI.HardSphere.FreeVisits.free_visited_card_le_of_norm line 198