OAI/Probability/Ballisticity/Estimates/CurveEndpointLaw.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.medianDeviation_le_iff line 15
2. lemma OAI.DirectionalTransience.curvePrefix_ae_eq line 24
3. lemma OAI.DirectionalTransience.curveEndpoint_eq_map line 34
4. lemma OAI.DirectionalTransience.curveEndpoint_lateral_map line 66
5. lemma OAI.DirectionalTransience.hitAt_translate_zero line 88
6. lemma OAI.DirectionalTransience.curvePrefixAt_translate_zero line 105
7. lemma OAI.DirectionalTransience.curveEndpoint_increment_translation line 113
8. lemma OAI.DirectionalTransience.conditional_selection_moment line 139