OAI/Probability/Ballisticity/Estimates/CurveWordDisjoint.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.curveWordEvent_cons_mem line 15
2. lemma OAI.DirectionalTransience.curveWordEvent_disjoint line 26
3. lemma OAI.DirectionalTransience.coordinate_hitAt_recordPrefix line 59
4. lemma OAI.DirectionalTransience.recordPrefix_lower line 109
5. lemma OAI.DirectionalTransience.curvePrefix_iff line 139