OAI/Probability/GammaPassage/SquareLoops.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Indexed square-lattice loops, their closedness count, and bad-site count.

  1. structure OAI.PlanarFPP.SquareLoop line 12

    Also declared: OAI/Probability/FirstPassage/SquareLoops.lean:11 (same declaration text).

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

    Also declared: OAI/Probability/FirstPassage/SquareLoops.lean:18 (same declaration text).

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

    Also declared: OAI/Probability/FirstPassage/SquareLoops.lean:20 (same declaration text).

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

    Also declared: OAI/Probability/FirstPassage/SquareLoops.lean:22 (same declaration text).

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

    Also declared: OAI/Probability/FirstPassage/SquareLoops.lean:29 (same declaration text).

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

    Also declared: OAI/Probability/FirstPassage/SquareLoops.lean:32 (same declaration text).

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

    Also declared: OAI/Probability/FirstPassage/SquareLoops.lean:50 (same declaration text).

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

    Source documentation

    The source's m/8 lower bound, without rounding conventions.

    Also declared: OAI/Probability/FirstPassage/SquareLoops.lean:53 (same declaration text).

    theorem length_le_eight_badSites (c : SquareLoop m) (hc : c.NoRepeatedSides) :
    m ≤ 8*c.badSites.card := by
…

    Mentions: OAI.PlanarFPP.SquareLoop