OAI/Probability/GammaPassage/LocalGlobalEquality.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GammaFPP.FiniteLocal.localization_trace_take line 8
2. lemma OAI.GammaFPP.FiniteLocal.localization_prefix_cost_le line 17
3. lemma OAI.GammaFPP.FiniteLocal.trail_short_of_no_cheap_prefix line 29

   Source documentation

   If no trail of length R has cost at most B, every trail with cost at most B has fewer than R steps.

   lemma trail_short_of_no_cheap_prefix (w : Edge → ℝ) (hw : ∀ e, 0 ≤ w e)
       (p : Vertex) (R : ℕ) (B : ℝ)
       (hno : ¬ ∃ es : List Step, es.length = R ∧
         ((trace p es).map traversalEdge).Nodup ∧ pathCost w p es ≤ B)
       (ds : List Step) (hn : ((trace p ds).map traversalEdge).Nodup)
       (hc : pathCost w p ds ≤ B) : ds.length < R := by
   …

4. theorem OAI.GammaFPP.FiniteLocal.exists_local_near_optimal_of_no_cheap_trail line 45

   Source documentation

   Near-optimal paths belong to the finite local family when some endpoint path has cost below B and no trail of length R has cost at most B.

   theorem exists_local_near_optimal_of_no_cheap_trail
       (w : Edge → ℝ) (hw : ∀ e, 0 ≤ w e) (p q : Vertex) (R : ℕ) (B : ℝ)
       (hpath : ∃ ds : List Step, p + displacement ds = q ∧ pathCost w p ds < B)
       (hno : ¬ ∃ es : List Step, es.length = R ∧
         ((trace p es).map traversalEdge).Nodup ∧ pathCost w p es ≤ B)
       (ε : ℝ) (hε : 0 < ε) :
       ∃ ds ∈ candidates p q R,
         pathCost w p ds < PlanarFPP.passageTime w p q + ε := by
   …

   Mentions: OAI.GammaFPP.FiniteLocal.candidates, OAI.PlanarFPP.passageTime

5. theorem OAI.GammaFPP.FiniteLocal.passageTime_eq_unrestricted_of_no_cheap_trail line 68

   Source documentation

   The finite local minimum equals the unrestricted passage time when no trail of length R has cost at most the comparison threshold.

   theorem passageTime_eq_unrestricted_of_no_cheap_trail
       (w : Edge → ℝ) (hw : ∀ e, 0 ≤ w e) (p q : Vertex) (R : ℕ) (B : ℝ)
       (hR : latticeDistance p q < R)
       (hpath : ∃ ds : List Step, p + displacement ds = q ∧ pathCost w p ds < B)
       (hno : ¬ ∃ es : List Step, es.length = R ∧
         ((trace p es).map traversalEdge).Nodup ∧ pathCost w p es ≤ B) :
       passageTime w p q R = PlanarFPP.passageTime w p q := by
   …

   Mentions: OAI.GammaFPP.FiniteLocal.passageTime, OAI.PlanarFPP.passageTime

6. theorem OAI.GammaFPP.FiniteLocal.passageTime_eq_unrestricted_of_no_cheap_linear_trail line 84

   Source documentation

   Localization at the linear cost threshold c * R.

   theorem passageTime_eq_unrestricted_of_no_cheap_linear_trail
       (w : Edge → ℝ) (hw : ∀ e, 0 ≤ w e) (p q : Vertex) (R : ℕ) (c : ℝ)
       (hR : latticeDistance p q < R)
       (hpath : ∃ ds : List Step, p + displacement ds = q ∧ pathCost w p ds < c * R)
       (hno : ¬ ∃ es : List Step, es.length = R ∧
         ((trace p es).map traversalEdge).Nodup ∧ pathCost w p es ≤ c * R) :
       passageTime w p q R = PlanarFPP.passageTime w p q :=
   …

   Mentions: OAI.GammaFPP.FiniteLocal.passageTime, OAI.PlanarFPP.passageTime