OAI/Probability/FirstPassage/BoundaryGeometry.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.PlanarFPP.(instance at line 10) line 10
2. def OAI.PlanarFPP.Step.left line 14

   Also declared: OAI/Probability/GammaPassage/BoundaryGeometry.lean:18 (same declaration text).

3. def OAI.PlanarFPP.Step.right line 17

   Also declared: OAI/Probability/GammaPassage/BoundaryGeometry.lean:21 (same declaration text).

4. def OAI.PlanarFPP.Step.outward line 20

   Also declared: OAI/Probability/GammaPassage/BoundaryGeometry.lean:24 (same declaration text).

5. def OAI.PlanarFPP.Step.corner line 22

   Also declared: OAI/Probability/GammaPassage/BoundaryGeometry.lean:26 (same declaration text).

6. abbrev OAI.PlanarFPP.SquareSide line 25

   Also declared: OAI/Probability/GammaPassage/BoundaryGeometry.lean:29 (same declaration text).

7. def OAI.PlanarFPP.SquareSide.tail line 27

   Also declared: OAI/Probability/GammaPassage/BoundaryGeometry.lean:31 (same declaration text).

8. def OAI.PlanarFPP.SquareSide.head line 29

   Also declared: OAI/Probability/GammaPassage/BoundaryGeometry.lean:33 (same declaration text).

9. def OAI.PlanarFPP.IsBoundarySide line 31

   Also declared: OAI/Probability/GammaPassage/BoundaryGeometry.lean:35 (same declaration text).

10. instance OAI.PlanarFPP.(instance at line 34) line 34
11. def OAI.PlanarFPP.boundarySides line 37

    Also declared: OAI/Probability/GammaPassage/BoundaryGeometry.lean:41 (same declaration text).

12. theorem OAI.PlanarFPP.mem_boundarySides line 40

    Also declared: OAI/Probability/GammaPassage/BoundaryGeometry.lean:44 (same declaration text).

13. def OAI.PlanarFPP.boundaryNext line 44

    Also declared: OAI/Probability/GammaPassage/BoundaryGeometry.lean:50 (same declaration text).

14. def OAI.PlanarFPP.boundaryPrev line 51

    Also declared: OAI/Probability/GammaPassage/BoundaryGeometry.lean:57 (same declaration text).

15. theorem OAI.PlanarFPP.boundaryNext_boundary line 58

    Also declared: OAI/Probability/GammaPassage/BoundaryGeometry.lean:64 (same declaration text).

16. theorem OAI.PlanarFPP.boundaryNext_tail line 73

    Also declared: OAI/Probability/GammaPassage/BoundaryGeometry.lean:79 (same declaration text).

17. theorem OAI.PlanarFPP.boundaryPrev_next line 85

    Also declared: OAI/Probability/GammaPassage/BoundaryGeometry.lean:91 (same declaration text).

18. abbrev OAI.PlanarFPP.BoundarySide line 98

    Also declared: OAI/Probability/GammaPassage/BoundaryGeometry.lean:104 (same declaration text).

19. def OAI.PlanarFPP.boundarySuccessor line 100

    Also declared: OAI/Probability/GammaPassage/BoundaryGeometry.lean:106 (same declaration text).

20. theorem OAI.PlanarFPP.boundarySuccessor_injective line 104

    Also declared: OAI/Probability/GammaPassage/BoundaryGeometry.lean:110 (same declaration text).

21. def OAI.PlanarFPP.boundaryPerm line 113

    Also declared: OAI/Probability/GammaPassage/BoundaryGeometry.lean:121 (same declaration text).

22. theorem OAI.PlanarFPP.boundaryPerm_tail line 118

    Also declared: OAI/Probability/GammaPassage/BoundaryGeometry.lean:126 (same declaration text).

23. theorem OAI.PlanarFPP.boundaryPerm_ne_self line 121

    Also declared: OAI/Probability/GammaPassage/BoundaryGeometry.lean:129 (same declaration text).

24. theorem OAI.PlanarFPP.boundary_dualEdge_injective line 132

    Also declared: OAI/Probability/GammaPassage/BoundaryGeometry.lean:142 (same declaration text).