OAI/Probability/FirstPassage/Localization.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PlanarFPP.timeConstantNorm_continuous line 11
2. theorem OAI.PlanarFPP.timeConstantNorm_lower_bound line 24
3. theorem OAI.PlanarFPP.pathCost_take_le line 48
4. def OAI.PlanarFPP.PathIn line 56
5. theorem OAI.PlanarFPP.path_confined_of_escape line 59
6. theorem OAI.PlanarFPP.exists_confined_near_optimal line 72
7. theorem OAI.PlanarFPP.UniformShape.eventually_escape line 81