OAI/Probability/DirectionalWalk/LateEndpoints.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalZeroOne.finiteLateEndpointEvent line 12
2. lemma OAI.DirectionalZeroOne.measurableSet_finiteLateEndpointEvent line 16
3. lemma OAI.DirectionalZeroOne.finiteLateContact_prefix line 21
4. lemma OAI.DirectionalZeroOne.finite_bridge_late_bound line 44
5. lemma OAI.DirectionalZeroOne.renewalCut_two_mass line 99
6. lemma OAI.DirectionalZeroOne.axis_two_cuts_lower line 152
7. lemma OAI.DirectionalZeroOne.reversed_cut_bridge_law line 174
8. lemma OAI.DirectionalZeroOne.mixed_bridge_late_bound line 197