OAI/Probability/GammaPassage/GoodSiteEvents.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GammaFPP.CrossingBridge.internalEdges_mono line 9
2. theorem OAI.GammaFPP.CrossingBridge.DependsOnEdges.mono line 15
3. theorem OAI.GammaFPP.CrossingBridge.rareFastVertices_subset_block line 20
4. theorem OAI.GammaFPP.CrossingBridge.connectorVertices_subset_block line 47
5. def OAI.GammaFPP.CrossingBridge.siteTrial line 63
6. def OAI.GammaFPP.CrossingBridge.siteConnector line 68
7. def OAI.GammaFPP.CrossingBridge.goodSiteEvent line 80
8. theorem OAI.GammaFPP.CrossingBridge.measurableSet_goodSiteEvent line 86
9. theorem OAI.GammaFPP.CrossingBridge.goodSiteEvent_depends line 96
10. theorem OAI.GammaFPP.CrossingBridge.goodSiteEvent_independent line 122