OAI/Probability/FirstPassage/SquareLoops.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.PlanarFPP.SquareLoop line 11

   Also declared: OAI/Probability/GammaPassage/SquareLoops.lean:12 (same declaration text).

2. def OAI.PlanarFPP.SquareLoop.winding line 18

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

3. def OAI.PlanarFPP.SquareLoop.NoRepeatedSides line 20

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

4. theorem OAI.PlanarFPP.SquareLoop.sum_delta line 22

   Also declared: OAI/Probability/GammaPassage/SquareLoops.lean:23 (same declaration text).

5. def OAI.PlanarFPP.SquareLoop.upLeftIndices line 29

   Also declared: OAI/Probability/GammaPassage/SquareLoops.lean:30 (same declaration text).

6. theorem OAI.PlanarFPP.SquareLoop.upLeft_count line 32

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

7. def OAI.PlanarFPP.SquareLoop.badSites line 50

   Also declared: OAI/Probability/GammaPassage/SquareLoops.lean:51 (same declaration text).

8. theorem OAI.PlanarFPP.SquareLoop.length_le_eight_badSites line 53

   Also declared: OAI/Probability/GammaPassage/SquareLoops.lean:55 (same declaration text).