OAI/Probability/GammaPassage/ContourCounts.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The closedness count in crossings.tex:cr:oriented-paths. A contour need not be simple at vertices; its zero displacement alone gives the half-length count.

  1. theorem OAI.PlanarFPP.displacement_counts line 11

    Also declared: OAI/Probability/FirstPassage/ContourCounts.lean:8 (same declaration text).

  2. theorem OAI.PlanarFPP.closed_walk_up_left_count line 22

    Source documentation

    Exactly half the edges of a closed square-lattice walk point upward or leftward, as required before selecting bad sites in the source contour proof.

    Also declared: OAI/Probability/FirstPassage/ContourCounts.lean:17 (same declaration text).

    theorem closed_walk_up_left_count (ds : List Step) (h : displacement ds=0) :
    ds.length=2*(ds.count Step.north+ds.count Step.west) := by
…

    Mentions: OAI.PlanarFPP.Step, OAI.PlanarFPP.displacement