OAI/Probability/Ballisticity/Walk/BoundaryPathCoordinates.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.recordIndexPosition_prefix_coord line 16
2. lemma OAI.DirectionalTransience.regularPath_recenter line 38
3. lemma OAI.DirectionalTransience.noDrop_recenter line 48
4. lemma OAI.DirectionalTransience.trueRecord_recenter line 54
5. lemma OAI.DirectionalTransience.translated_recordIndexPosition_suffix line 66
6. lemma OAI.DirectionalTransience.boundaryData_firstHit_prefix line 97