OAI/Probability/LatticePassage/CheapPath.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CompanionFPP.pathEdges line 12
2. lemma OAI.CompanionFPP.pathEdges_val line 16
3. lemma OAI.CompanionFPP.pathEdges_length line 22
4. lemma OAI.CompanionFPP.pathEdges_nodup line 28
5. lemma OAI.CompanionFPP.pathCost_eq_edgeList_sum line 34
6. theorem OAI.CompanionFPP.cheap_trail_probability line 40