OAI/Probability/FirstPassage/BoundaryWinding.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFPP.SquareSide.rayCross line 10

   Also declared: OAI/Probability/GammaPassage/BoundaryWinding.lean:10 (same declaration text).

2. def OAI.PlanarFPP.SquareSide.opposite line 16

   Also declared: OAI/Probability/GammaPassage/BoundaryWinding.lean:16 (same declaration text).

3. theorem OAI.PlanarFPP.SquareSide.opposite_opposite line 19

   Also declared: OAI/Probability/GammaPassage/BoundaryWinding.lean:19 (same declaration text).

4. theorem OAI.PlanarFPP.SquareSide.opposite_ne_self line 24

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

5. theorem OAI.PlanarFPP.SquareSide.rayCross_opposite line 29

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

6. theorem OAI.PlanarFPP.square_rayCross_sum line 35

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

7. def OAI.PlanarFPP.internalSides line 43

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

8. theorem OAI.PlanarFPP.internalSides_opposite line 46

   Also declared: OAI/Probability/GammaPassage/BoundaryWinding.lean:46 (same declaration text).

9. theorem OAI.PlanarFPP.internalSides_rayCross_sum line 53

   Also declared: OAI/Probability/GammaPassage/BoundaryWinding.lean:53 (same declaration text).

10. theorem OAI.PlanarFPP.boundarySides_rayCross_sum line 63

    Also declared: OAI/Probability/GammaPassage/BoundaryWinding.lean:65 (same declaration text).