OAI/Probability/LatticePassage/LocalPassage.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CompanionFPP.localCandidates line 8
  2. lemma OAI.CompanionFPP.mem_localCandidates line 14
  3. def OAI.CompanionFPP.localEdges line 22
  4. lemma OAI.CompanionFPP.pathCost_eq_of_agree line 26
  5. lemma OAI.CompanionFPP.local_pathCost_eq line 32
  6. def OAI.CompanionFPP.localPassageTime line 42
  7. lemma OAI.CompanionFPP.local_costs_finite line 45
  8. theorem OAI.CompanionFPP.measurable_localPassageTime line 52
  9. theorem OAI.CompanionFPP.localPassageTime_eq_of_agree line 69
  10. theorem OAI.CompanionFPP.local_geodesic_exists line 79
  11. theorem OAI.CompanionFPP.localPassageTime_eq_of_short_geodesic line 93
  12. theorem OAI.CompanionFPP.localPassageTime_failure_probability line 105