OAI/Probability/GammaPassage/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/FirstPassage/BoundaryWinding.lean:10 (same declaration text).

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

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

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

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

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

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

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

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

6. theorem OAI.PlanarFPP.square_rayCross_sum line 35

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

7. def OAI.PlanarFPP.internalSides line 43

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

8. theorem OAI.PlanarFPP.internalSides_opposite line 46

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

9. theorem OAI.PlanarFPP.internalSides_rayCross_sum line 53

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

10. theorem OAI.PlanarFPP.boundarySides_rayCross_sum line 65

    Source documentation

    Before cancellation, only the square centered at zero crosses the ray with net signed count one. Shared sides have opposite counts and cancel.

    Also declared: OAI/Probability/FirstPassage/BoundaryWinding.lean:63 (same declaration text).

    theorem boundarySides_rayCross_sum (S : Finset Vertex) :
        ∑ e ∈ boundarySides S, e.rayCross = if (0 : Vertex) ∈ S then 1 else 0 := by
    …

    Mentions: OAI.PlanarFPP.Vertex, OAI.PlanarFPP.boundarySides