OAI/Analysis/HardSphere/PathBounds/FreeVisitTravel.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.FreeVisits.torusDistance_le_three_of_coord line 13
  2. lemma OAI.HardSphere.FreeVisits.freeTrajectory_dist_le line 24
  3. def OAI.HardSphere.FreeVisits.visitStartDistance line 37
  4. lemma OAI.HardSphere.FreeVisits.visitStartDistance_nonneg line 42
  5. lemma OAI.HardSphere.FreeVisits.visit_distance_le line 46
  6. lemma OAI.HardSphere.FreeVisits.free_visit_travel_gaussian line 63
  7. theorem OAI.HardSphere.FreeVisits.free_visit_travel line 94
  8. lemma OAI.HardSphere.FreeVisits.lintegral_three_thirds line 129
  9. lemma OAI.HardSphere.FreeVisits.ofReal_exp_rpow line 141
  10. lemma OAI.HardSphere.FreeVisits.indicator_one_third line 145
  11. lemma OAI.HardSphere.FreeVisits.exp_sub_one_le_mul_exp line 150
  12. def OAI.HardSphere.FreeVisits.visitDefect line 156
  13. lemma OAI.HardSphere.FreeVisits.visitDefect_le line 161
  14. theorem OAI.HardSphere.FreeVisits.free_visit_bound line 191