OAI/Probability/FirstPassage/EndpointEvents.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PlanarFPP.endpointBox_finite line 8
2. def OAI.PlanarFPP.endpointBoxVertices line 11
3. def OAI.PlanarFPP.arbitraryEndpointEvent line 14
4. lemma OAI.PlanarFPP.mem_arbitraryEndpointEvent line 18
5. lemma OAI.PlanarFPP.measurableSet_arbitraryEndpointEvent line 26
6. lemma OAI.PlanarFPP.arbitraryEndpointEvent_depends line 30
7. def OAI.PlanarFPP.coarsePairIndices line 34
8. def OAI.PlanarFPP.coarsePairEvent line 37
9. theorem OAI.PlanarFPP.arbitraryEndpointEvent_coarse_cover line 41