OrientedCompactness.lean`

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Finite branching for oriented square-lattice paths.

def OAI.PlanarFPP.orientedSurvival line 14
Source documentation
n forward steps with all visited sites except possibly the last good.
Also declared: OAI/Probability/FirstPassage/OrientedCompactness.lean:9 (same declaration text).
```
def orientedSurvival (G : Vertex → Prop) (p : Vertex) : ℕ → Prop
  | 0 => True
  | n+1 => G p ∧ (orientedSurvival G (p+(1,0)) n ∨ orientedSurvival G (p+(0,1)) n)
```
Mentions: OAI.PlanarFPP.Vertex
def OAI.PlanarFPP.infiniteOrientedPath line 18
Also declared: OAI/Probability/FirstPassage/OrientedCompactness.lean:13 (same declaration text).
theorem OAI.PlanarFPP.orientedSurvival_pred line 22
Also declared: OAI/Probability/FirstPassage/OrientedCompactness.lean:17 (same declaration text).
theorem OAI.PlanarFPP.orientedSurvival_mono line 32
Also declared: OAI/Probability/FirstPassage/OrientedCompactness.lean:27 (same declaration text).
theorem OAI.PlanarFPP.oriented_surviving_successor line 38
Also declared: OAI/Probability/FirstPassage/OrientedCompactness.lean:33 (same declaration text).
theorem OAI.PlanarFPP.infiniteOrientedPath_iff line 49
Also declared: OAI/Probability/FirstPassage/OrientedCompactness.lean:44 (same declaration text).
def OAI.PlanarFPP.orientedEndpoints line 79
Also declared: OAI/Probability/FirstPassage/OrientedCompactness.lean:74 (same declaration text).
theorem OAI.PlanarFPP.orientedEndpoints_nonempty_iff line 85
Also declared: OAI/Probability/FirstPassage/OrientedCompactness.lean:80 (same declaration text).
def OAI.PlanarFPP.orientedReachable line 95
Source documentation
The reachable set includes a possibly bad terminal site, exactly as in the manuscript's S. This is the finite set to which its contour argument applies.
Also declared: OAI/Probability/FirstPassage/OrientedCompactness.lean:88 (same declaration text).
```
def orientedReachable (G : Vertex → Prop) (p : Vertex) : Set Vertex :=
…
```
Mentions: OAI.PlanarFPP.Vertex
theorem OAI.PlanarFPP.orientedReachable_finite_of_no_infinite_path line 98
Also declared: OAI/Probability/FirstPassage/OrientedCompactness.lean:91 (same declaration text).
theorem OAI.PlanarFPP.orientedReachable_origin line 114
Also declared: OAI/Probability/FirstPassage/OrientedCompactness.lean:107 (same declaration text).
theorem OAI.PlanarFPP.orientedEndpoints_extend line 118
Source documentation
Extend a reachable finite path by a forward step from a good terminal site.
Also declared: OAI/Probability/FirstPassage/OrientedCompactness.lean:110 (same declaration text).
```
theorem orientedEndpoints_extend (G : Vertex → Prop) (p q : Vertex) (n : ℕ)
    (hq : q ∈ orientedEndpoints G p n) (hg : G q) :
    q+(1,0) ∈ orientedEndpoints G p (n+1) ∧ q+(0,1) ∈ orientedEndpoints G p (n+1) := by
…
```
Mentions: OAI.PlanarFPP.Vertex, OAI.PlanarFPP.orientedEndpoints
theorem OAI.PlanarFPP.orientedReachable_forward line 138
Source documentation
The forward neighbors of a good reachable site are reachable.
Also declared: OAI/Probability/FirstPassage/OrientedCompactness.lean:129 (same declaration text).
```
theorem orientedReachable_forward (G : Vertex → Prop) (p q : Vertex)
    (hq : q ∈ orientedReachable G p) (hg : G q) :
    q+(1,0) ∈ orientedReachable G p ∧ q+(0,1) ∈ orientedReachable G p := by
…
```
Mentions: OAI.PlanarFPP.Vertex, OAI.PlanarFPP.orientedReachable
theorem OAI.PlanarFPP.orientedReachable_boundary_bad line 146
Source documentation
The source's upward/leftward boundary edges force their left site bad.
Also declared: OAI/Probability/FirstPassage/OrientedCompactness.lean:136 (same declaration text).
```
theorem orientedReachable_boundary_bad (G : Vertex → Prop) (p q : Vertex)
    (hq : q ∈ orientedReachable G p)
    (hout : q+(1,0) ∉ orientedReachable G p ∨ q+(0,1) ∉ orientedReachable G p) : ¬G q := by
…
```
Mentions: OAI.PlanarFPP.Vertex, OAI.PlanarFPP.orientedReachable
theorem OAI.PlanarFPP.measurableSet_orientedSurvival line 155
Also declared: OAI/Probability/FirstPassage/OrientedCompactness.lean:145 (same declaration text).
theorem OAI.PlanarFPP.measurableSet_infiniteOrientedPath line 162
Also declared: OAI/Probability/FirstPassage/OrientedCompactness.lean:152 (same declaration text).