OAI/Probability/FirstPassage/GoodSitePaths.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PlanarFPP.goodSite_trial_witness line 10
2. theorem OAI.PlanarFPP.sourceSupportCost_of_endpoint line 33
3. theorem OAI.PlanarFPP.goodSite_connector_witness line 40
4. theorem OAI.PlanarFPP.UniformShape.no_goodSite_path line 72
5. theorem OAI.PlanarFPP.exponential_goodSite_path_probability_zero line 106