OAI/Probability/GammaPassage/PathSubpaths.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GammaFPP.CrossingBridge.pathIn_append_left line 9
2. lemma OAI.GammaFPP.CrossingBridge.pathIn_append_right line 15
3. lemma OAI.GammaFPP.CrossingBridge.reverseSteps_append line 22
4. lemma OAI.GammaFPP.CrossingBridge.reverseSteps_reverse line 25
5. lemma OAI.GammaFPP.CrossingBridge.pathIn_reverseSteps line 29
6. lemma OAI.GammaFPP.CrossingBridge.path_first_column_up line 51

   Source documentation

   First visit to a column from its left, with the prefix staying to the left.

   lemma path_first_column_up (p : Vertex) (ds : List Step) (X : ℤ)
       (hp : p.1 ≤ X) (hend : X ≤ (p+displacement ds).1) :
       ∃ pre rest : List Step, ds=pre++rest ∧ (p+displacement pre).1=X ∧
         PathIn p pre {z | z.1 ≤ X} := by
   …

   Mentions: OAI.GammaFPP.CrossingBridge.PathIn

7. lemma OAI.GammaFPP.CrossingBridge.path_first_column_down line 74

   Source documentation

   First visit to a column from its right, with the prefix staying to the right.

   lemma path_first_column_down (p : Vertex) (ds : List Step) (X : ℤ)
       (hp : X ≤ p.1) (hend : (p+displacement ds).1 ≤ X) :
       ∃ pre rest : List Step, ds=pre++rest ∧ (p+displacement pre).1=X ∧
         PathIn p pre {z | X ≤ z.1} := by
   …

   Mentions: OAI.GammaFPP.CrossingBridge.PathIn