EnclosingContour.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The enclosing contour of the finite reachable set in cr:oriented-paths.

theorem OAI.PlanarFPP.exists_enclosing_squareLoop line 11
Also declared: OAI/Probability/FirstPassage/EnclosingContour.lean:10 (same declaration text).
theorem OAI.PlanarFPP.exists_enclosing_squareLoop_unoriented line 43
Source documentation
The extracted walk also has no repeated unoriented dual edge.
Also declared: OAI/Probability/FirstPassage/EnclosingContour.lean:41 (same declaration text).
```
theorem exists_enclosing_squareLoop_unoriented (S : Finset Vertex) (h0 : (0 : Vertex) ∈ S) :
    ∃ m : ℕ, 0 < m ∧ ∃ c : SquareLoop m,
      c.winding ≠ 0 ∧ (∀ i, IsBoundarySide S (c.side i)) ∧
      Function.Injective (fun i => (c.side i).2.edge (c.side i).tail) := by
…
```
Mentions: OAI.PlanarFPP.Vertex, OAI.PlanarFPP.SquareLoop, OAI.PlanarFPP.IsBoundarySide
theorem OAI.PlanarFPP.SquareLoop.badSites_bad line 54
Source documentation
The upward and leftward sides force bad sites using exactly the source's forward-closure condition, with no probabilistic assumption.
Also declared: OAI/Probability/FirstPassage/EnclosingContour.lean:50 (same declaration text).
```
theorem SquareLoop.badSites_bad {m : ℕ} (c : SquareLoop m)
    (S : Finset Vertex) (G : Vertex → Prop)
    (hb : ∀ i, IsBoundarySide S (c.side i))
    (hforward : ∀ q ∈ S, G q → q+(1,0) ∈ S ∧ q+(0,1) ∈ S) :
    ∀ q ∈ c.badSites, ¬G q := by
…
```
Mentions: OAI.PlanarFPP.SquareLoop, OAI.PlanarFPP.Vertex, OAI.PlanarFPP.IsBoundarySide

theorem OAI.PlanarFPP.no_infinite_path_enclosing_contour line 69

Source documentation

In the absence of an infinite good oriented path, there is an enclosing loop with a separated family of forced-bad sites.

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

theorem no_infinite_path_enclosing_contour (G : Vertex → Prop) (k : ℕ)
    (h : ¬infiniteOrientedPath G 0) :
    ∃ m : ℕ, 0 < m ∧ ∃ c : SquareLoop m,
      c.NoRepeatedSides ∧ c.winding ≠ 0 ∧
      (∀ q ∈ c.badSites, ¬G q) ∧
      ∃ T : Finset Vertex, T ⊆ c.badSites ∧
        Set.Pairwise (↑T : Set Vertex) (fun p q => ¬latticeNear k p q) ∧
        m ≤ 8*(2*k+1)^2*T.card := by
…

Mentions: OAI.PlanarFPP.Vertex, OAI.PlanarFPP.infiniteOrientedPath, OAI.PlanarFPP.SquareLoop, OAI.PlanarFPP.latticeNear