OAI/Probability/FirstPassage/GoodSiteEvents.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PlanarFPP.internalEdges_mono line 10
2. theorem OAI.PlanarFPP.DependsOnEdges.mono line 16
3. theorem OAI.PlanarFPP.rareFastVertices_subset_block line 21
4. theorem OAI.PlanarFPP.connectorVertices_subset_block line 48
5. def OAI.PlanarFPP.siteTrial line 64
6. def OAI.PlanarFPP.siteConnector line 69
7. def OAI.PlanarFPP.goodSiteEvent line 81
8. theorem OAI.PlanarFPP.measurableSet_goodSiteEvent line 87
9. theorem OAI.PlanarFPP.goodSiteEvent_depends line 97
10. theorem OAI.PlanarFPP.goodSiteEvent_independent line 122