LocalTrailCandidates.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.GammaFPP.FiniteLocal.pathCost_one_eq_length line 12
Source documentation
A path with unit edge weights has cost equal to its number of steps.
```
lemma pathCost_one_eq_length (p : Vertex) (ds : List Step) :
    pathCost (fun _ : Edge => (1 : ℝ)) p ds = (ds.length : ℝ) := by
…
```
lemma OAI.GammaFPP.FiniteLocal.coordinatePath_length line 20
Source documentation
The coordinate path has length equal to the lattice distance.
```
private lemma coordinatePath_length (p q : Vertex) :
    (coordinatePath p q).length = latticeDistance p q := by
…
```

lemma OAI.GammaFPP.FiniteLocal.exists_short_trail line 31

Source documentation

Loop erasure at unit weights produces a trail of at most the lattice distance.

lemma exists_short_trail (p q : Vertex) :
    ∃ ds : List Step, p + displacement ds = q ∧
      ((trace p ds).map traversalEdge).Nodup ∧ ds.length ≤ latticeDistance p q := by
…

def OAI.GammaFPP.FiniteLocal.candidates line 43
Source documentation
Trails with fewer than R steps connecting the specified endpoints.
```
noncomputable def candidates (p q : Vertex) (R : ℕ) : Finset (List Step) := by
…
```
lemma OAI.GammaFPP.FiniteLocal.mem_candidates line 48
lemma OAI.GammaFPP.FiniteLocal.candidates_nonempty line 65