OAI/Analysis/HardSphere/PathBounds/InteractingVisits.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.spatial_count_mgf_enn line 16
  2. def OAI.HardSphere.FreeVisits.defectiveTotalVisits line 42
  3. lemma OAI.HardSphere.FreeVisits.pathVisitedSites_onePathAt line 47
  4. lemma OAI.HardSphere.FreeVisits.exp_defectiveTotalVisits line 53
  5. lemma OAI.HardSphere.FreeVisits.product_one_add_exp_le line 70
  6. theorem OAI.HardSphere.FreeVisits.interacting_visit_mgf line 83
  7. lemma OAI.HardSphere.torusDistance_add line 155
  8. def OAI.HardSphere.shiftPath line 163
  9. lemma OAI.HardSphere.shiftPath_continuous line 166
  10. lemma OAI.HardSphere.shiftPath_neg line 171
  11. lemma OAI.HardSphere.shiftPath_reverse line 176
  12. lemma OAI.HardSphere.shiftPath_free line 179
  13. lemma OAI.HardSphere.spatialSiteDistance_add line 185
  14. def OAI.HardSphere.ShiftVisits.center line 206
  15. def OAI.HardSphere.ShiftVisits.singleDefect line 208
  16. lemma OAI.HardSphere.ShiftVisits.shifted_visits line 212
  17. lemma OAI.HardSphere.ShiftVisits.singleDefect_eq line 226
  18. lemma OAI.HardSphere.ShiftVisits.singleDefect_measurable line 231
  19. lemma OAI.HardSphere.ShiftVisits.singleDefect_reverse line 240
  20. lemma OAI.HardSphere.ShiftVisits.free_single_defect_bound line 246