OAI/Analysis/HardSphere/PathBounds/FreeVisitProbability.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.FreeVisits.pathVisitedSites_card_measurable line 16
2. def OAI.HardSphere.FreeVisits.visitCount line 26
3. lemma OAI.HardSphere.FreeVisits.visitCount_measurable line 30
4. lemma OAI.HardSphere.FreeVisits.one_segment_visit_tail line 35
5. lemma OAI.HardSphere.FreeVisits.visit_count_split line 67
6. lemma OAI.HardSphere.FreeVisits.visit_tail_add line 84
7. lemma OAI.HardSphere.FreeVisits.n_segment_visit_tail line 133
8. lemma OAI.HardSphere.FreeVisits.whole_time_visit_tail line 154