OAI/Probability/Ballisticity/Crossings/FirstLayerHitRecordIndexTime.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.firstLayerHit_recordIndexTime line 127
2. lemma OAI.DirectionalTransience.noDrop_firstLayerHit_exists line 151
3. lemma OAI.DirectionalTransience.survivingLane_record_iff line 161
4. lemma OAI.DirectionalTransience.sharedConditionedPairLaw_absolutelyContinuous line 217
5. lemma OAI.DirectionalTransience.sharedConditionedPairLaw_noDrop line 222