OAI/Probability/Ballisticity/Walk/RegularPath.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalTransience.RegularPath line 133
2. lemma OAI.DirectionalTransience.measurableSet_regularPath line 136
3. lemma OAI.DirectionalTransience.annealedFrom_regularPath line 146
4. lemma OAI.DirectionalTransience.sharedConditioned_regularPath line 154
5. lemma OAI.DirectionalTransience.conditionedFrom_regularPath line 165
6. lemma OAI.DirectionalTransience.open_lane_record_iff line 176