OAI/Probability/Ballisticity/Crossings/FirstHitPairGap.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.recordIndexTime_zero line 17
2. lemma OAI.DirectionalTransience.recordCount_commonTimes_second line 25
3. lemma OAI.DirectionalTransience.recordTime_between line 46
4. lemma OAI.DirectionalTransience.coordinate_prefix_bound line 59
5. lemma OAI.DirectionalTransience.firstHit_common_boundary_error line 71
6. def OAI.DirectionalTransience.firstHitPairGap line 121
7. lemma OAI.DirectionalTransience.measurable_firstHitPairGap line 126
8. lemma OAI.DirectionalTransience.independent_firstHit_decoration_bound line 133
9. theorem OAI.DirectionalTransience.independent_firstHit_decoration_small line 169