OAI/Probability/FirstPassage/ContourEnumeration.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PlanarFPP.SquareLoop.eq_of_start_direction line 11

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

  2. abbrev OAI.PlanarFPP.EnclosingLoop line 45

    Also declared: OAI/Probability/GammaPassage/ContourEnumeration.lean:47 (same declaration text).

  3. def OAI.PlanarFPP.enclosingLoopCode line 48

    Distinct definitions of this name: OAI/Probability/GammaPassage/ContourEnumeration.lean:50 (different declaration text). Qualify references as OAI.PlanarFPP.enclosingLoopCode@path.

  4. theorem OAI.PlanarFPP.enclosingLoopCode_injective line 53

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

  5. instance OAI.PlanarFPP.enclosingLoopFintype line 61

    Also declared: OAI/Probability/GammaPassage/ContourEnumeration.lean:63 (same declaration text).

  6. theorem OAI.PlanarFPP.enclosingLoop_card line 64

    Distinct definitions of this name: OAI/Probability/GammaPassage/ContourEnumeration.lean:68 (same statement text; different proof or body). Qualify references as OAI.PlanarFPP.enclosingLoop_card@path.