LocalRegularity.lean`

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.GammaFPP.FiniteLocal.pathCost_eq_of_agree line 10
lemma OAI.GammaFPP.FiniteLocal.candidate_pathCost_eq line 17
theorem OAI.GammaFPP.FiniteLocal.passageTime_eq_of_agree line 26
Source documentation
Agreement on the finite local edge set implies equality of local passage times.
```
theorem passageTime_eq_of_agree (w w' : Edge → ℝ) (p q : Vertex) (R : ℕ)
    (h : ∀ e ∈ localEdges p q R, w e = w' e) :
    passageTime w p q R = passageTime w' p q R := by
…
```
Mentions: OAI.GammaFPP.FiniteLocal.localEdges, OAI.GammaFPP.FiniteLocal.passageTime
theorem OAI.GammaFPP.FiniteLocal.finitePassageTime_restrict line 40
Source documentation
Restricting weights to the local edge set and extending by zero preserves the local passage time.
```
theorem finitePassageTime_restrict (p q : Vertex) (R : ℕ) (w : Edge → ℝ) :
    finitePassageTime p q R (fun e : ↥(localEdges p q R) => w e) =
      passageTime w p q R := by
…
```
Mentions: OAI.GammaFPP.FiniteLocal.finitePassageTime, OAI.GammaFPP.FiniteLocal.localEdges, OAI.GammaFPP.FiniteLocal.passageTime
lemma OAI.GammaFPP.FiniteLocal.continuous_pathCost line 48
Source documentation
The cost of a finite path is continuous in the edge weights.
```
lemma continuous_pathCost (p : Vertex) (ds : List Step) :
    Continuous (fun w : Edge → ℝ => pathCost w p ds) := by
…
```
lemma OAI.GammaFPP.FiniteLocal.passageTime_eq_inf' line 56
Source documentation
Identify the real sInf with the nonempty finite lattice infimum.
```
lemma passageTime_eq_inf' (w : Edge → ℝ) (p q : Vertex) (R : ℕ)
    (hR : latticeDistance p q < R) :
    passageTime w p q R =
      (candidates p q R).inf' (candidates_nonempty p q R hR)
        (fun ds => pathCost w p ds) := by
…
```
Mentions: OAI.GammaFPP.FiniteLocal.passageTime, OAI.GammaFPP.FiniteLocal.candidates, OAI.GammaFPP.FiniteLocal.candidates_nonempty
theorem OAI.GammaFPP.FiniteLocal.continuous_passageTime line 69
Source documentation
Local passage time is continuous when the candidate family is nonempty.
```
theorem continuous_passageTime (p q : Vertex) (R : ℕ)
    (hR : latticeDistance p q < R) :
    Continuous (fun w : Edge → ℝ => passageTime w p q R) := by
…
```
Mentions: OAI.GammaFPP.FiniteLocal.passageTime
lemma OAI.GammaFPP.FiniteLocal.continuous_extend line 81
theorem OAI.GammaFPP.FiniteLocal.continuous_finitePassageTime line 91
theorem OAI.GammaFPP.FiniteLocal.measurable_finitePassageTime line 95
theorem OAI.GammaFPP.FiniteLocal.measurable_passageTime line 100
Source documentation
Local passage time is measurable as a function of the edge weights.
```
@[fun_prop] theorem measurable_passageTime (p q : Vertex) (R : ℕ)
    (hR : latticeDistance p q < R) :
    Measurable (fun w : Edge → ℝ => passageTime w p q R) :=
…
```
Mentions: OAI.GammaFPP.FiniteLocal.passageTime