OAI/Probability/GammaPassage/GridVerticalPaths.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GammaFPP.CrossingBridge.pathIn_append line 8
2. lemma OAI.GammaFPP.CrossingBridge.vertical_straight_subset line 21
3. lemma OAI.GammaFPP.CrossingBridge.vertical_straight_in line 40
4. theorem OAI.GammaFPP.CrossingBridge.vertical_interval_all_pairs line 56

   Source documentation

   Both traversal directions use the same internal-edge sum, with each edge charged exactly once on the straight attachment path.

   theorem vertical_interval_all_pairs (w : Edge → ℝ) (hw : ∀ e, 0 ≤ w e)
       (X lo hi : ℤ) (p q : Vertex) (hp : p.1=X ∧ lo ≤ p.2 ∧ p.2 ≤ hi)
       (hq : q.1=X ∧ lo ≤ q.2 ∧ q.2 ≤ hi) :
       ∃ ds, p+displacement ds=q ∧
         pathCost w p ds ≤ ∑ e ∈ verticalIntervalEdges X lo hi,w e ∧
         PathIn p ds {z | z.1=X ∧ lo ≤ z.2 ∧ z.2 ≤ hi} := by
   …

   Mentions: OAI.GammaFPP.CrossingBridge.PathIn

5. lemma OAI.GammaFPP.CrossingBridge.transverse_interval_all_pairs line 95