OAI/Analysis/HardSphere/PathBounds/VisitCounts.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.FreeVisits.visitorCount line 16
  2. lemma OAI.HardSphere.FreeVisits.visitorCount_sum line 21
  3. lemma OAI.HardSphere.FreeVisits.visitorCount_measurable line 33
  4. lemma OAI.HardSphere.FreeVisits.defectiveTotalVisits_measurable line 45
  5. lemma OAI.HardSphere.FreeVisits.joint_visitor_sum line 52
  6. lemma OAI.HardSphere.FreeVisits.joint_visitors_markov line 60
  7. lemma OAI.HardSphere.Groups.centeredCell_distance line 98
  8. lemma OAI.HardSphere.Groups.intervalTime_zero_one line 109
  9. lemma OAI.HardSphere.Groups.smallDiameter_distance line 113
  10. def OAI.HardSphere.Groups.longVisitors line 118
  11. def OAI.HardSphere.Groups.visitors line 121
  12. structure OAI.HardSphere.Groups.Certificate line 124
  13. lemma OAI.HardSphere.Groups.eligible_of_not_discarded line 134
  14. lemma OAI.HardSphere.Groups.certificate_eligible_count line 165