OAI/Probability/Ballisticity/Walk/RecordLinearPath.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalTransience.recordLinearPath line 99
2. lemma OAI.DirectionalTransience.measurable_recordLinearPath line 103
3. lemma OAI.DirectionalTransience.recordLinearPath_suffix_small line 108
4. lemma OAI.DirectionalTransience.weighted_recordLinearPath_limit line 155
5. lemma OAI.DirectionalTransience.noDropWeighted_recordLinearPath_limit line 224