OAI/Probability/GammaPassage/PathChain.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GammaFPP.IntervalTravelBridge.pathIn_append line 9
2. theorem OAI.GammaFPP.IntervalTravelBridge.exists_path_chain line 23

   Source documentation

   Concatenating a finite list of connections preserves vertex localization and adds traversal costs.

   theorem exists_path_chain (w : Edge → ℝ) (p : ℕ → Vertex) (S : Set Vertex)
       (a : ℕ → ℝ) (n : ℕ) (hp : p 0 ∈ S)
       (h : ∀ i < n, ∃ ds, p i+displacement ds=p (i+1) ∧
         pathCost w (p i) ds ≤ a i ∧ PathIn (p i) ds S) :
       ∃ ds, p 0+displacement ds=p n ∧
         pathCost w (p 0) ds ≤ ∑ i ∈ range n, a i ∧ PathIn (p 0) ds S := by
   …

   Mentions: OAI.GammaFPP.IntervalTravelBridge.PathIn