OAI/Probability/FirstPassage/EndpointGeometry.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFPP.endpointVertex line 8
2. lemma OAI.PlanarFPP.endpointVertex_error line 10
3. lemma OAI.PlanarFPP.endpointVertex_close line 18
4. lemma OAI.PlanarFPP.endpointVertex_self line 23
5. lemma OAI.PlanarFPP.endpointVertex_displacement line 29
6. lemma OAI.PlanarFPP.endpoint_path_defect line 39
7. lemma OAI.PlanarFPP.negative_defect_reverse_span line 57
8. lemma OAI.PlanarFPP.extended_columns_span line 81