OAI/Probability/FirstPassage/EnclosingContour.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PlanarFPP.exists_enclosing_squareLoop line 10

   Also declared: OAI/Probability/GammaPassage/EnclosingContour.lean:11 (same declaration text).

2. theorem OAI.PlanarFPP.exists_enclosing_squareLoop_unoriented line 41

   Also declared: OAI/Probability/GammaPassage/EnclosingContour.lean:43 (same declaration text).

3. theorem OAI.PlanarFPP.SquareLoop.badSites_bad line 50

   Also declared: OAI/Probability/GammaPassage/EnclosingContour.lean:54 (same declaration text).

4. theorem OAI.PlanarFPP.no_infinite_path_enclosing_contour line 63

   Also declared: OAI/Probability/GammaPassage/EnclosingContour.lean:69 (same declaration text).