LocalTrailPassage.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

def OAI.GammaFPP.FiniteLocal.costs line 9
Source documentation
Costs of trails in the finite candidate family.
```
def costs (w : Edge → ℝ) (p q : Vertex) (R : ℕ) : Set ℝ :=
…
```
lemma OAI.GammaFPP.FiniteLocal.costs_finite line 12
lemma OAI.GammaFPP.FiniteLocal.costs_nonempty line 19
def OAI.GammaFPP.FiniteLocal.passageTime line 26
Source documentation
The infimum of costs among candidate trails. It is a finite minimum whenever the lattice distance is less than R.
```
noncomputable def passageTime (w : Edge → ℝ) (p q : Vertex) (R : ℕ) : ℝ :=
…
```
theorem OAI.GammaFPP.FiniteLocal.minimizing_candidate line 31
Source documentation
A nonempty finite candidate family attains its minimum for every real edge-weight assignment.
```
theorem minimizing_candidate (w : Edge → ℝ) (p q : Vertex) (R : ℕ)
    (hR : latticeDistance p q < R) :
    ∃ ds ∈ candidates p q R, pathCost w p ds = passageTime w p q R := by
…
```
Mentions: OAI.GammaFPP.FiniteLocal.candidates, OAI.GammaFPP.FiniteLocal.passageTime
lemma OAI.GammaFPP.FiniteLocal.passageTime_le_candidate line 43

theorem OAI.GammaFPP.FiniteLocal.exists_minimizing_trail line 50

Source documentation

A minimizing candidate is a trail connecting the endpoints in fewer than R steps.

theorem exists_minimizing_trail (w : Edge → ℝ) (p q : Vertex) (R : ℕ)
    (hR : latticeDistance p q < R) :
    ∃ ds : List Step, p + displacement ds = q ∧
      ((trace p ds).map traversalEdge).Nodup ∧ ds.length < R ∧
      pathCost w p ds = passageTime w p q R := by
…

Mentions: OAI.GammaFPP.FiniteLocal.passageTime

theorem OAI.GammaFPP.FiniteLocal.unrestricted_passageTime_le line 60
Source documentation
Unrestricted passage time is at most the finite local minimum.
```
theorem unrestricted_passageTime_le (w : Edge → ℝ) (hw : ∀ e, 0 ≤ w e)
    (p q : Vertex) (R : ℕ) (hR : latticeDistance p q < R) :
    PlanarFPP.passageTime w p q ≤ passageTime w p q R := by
…
```
Mentions: OAI.PlanarFPP.passageTime, OAI.GammaFPP.FiniteLocal.passageTime
lemma OAI.GammaFPP.FiniteLocal.passageTime_nonneg line 67