OAI/Probability/LatticePassage/Paths.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CompanionFPP.Weights line 12
  2. def OAI.CompanionFPP.edgeCost line 14
  3. theorem OAI.CompanionFPP.edgeCost_symm line 17
  4. def OAI.CompanionFPP.pathCost line 21
  5. theorem OAI.CompanionFPP.pathCost_nil line 25
  6. theorem OAI.CompanionFPP.pathCost_cons line 28
  7. theorem OAI.CompanionFPP.pathCost_append line 32
  8. theorem OAI.CompanionFPP.pathCost_nonneg line 39
  9. def OAI.CompanionFPP.passageTime line 45
  10. theorem OAI.CompanionFPP.passageTime_le_pathCost line 48
  11. theorem OAI.CompanionFPP.pathCost_reverse line 54
  12. theorem OAI.CompanionFPP.passageTime_nonneg line 61
  13. theorem OAI.CompanionFPP.passageTime_self line 68
  14. theorem OAI.CompanionFPP.passageTime_symm line 74
  15. theorem OAI.CompanionFPP.passageTime_triangle line 81
  16. structure OAI.CompanionFPP.Calibration line 96
  17. theorem OAI.CompanionFPP.Calibration.self line 104
  18. theorem OAI.CompanionFPP.Calibration.reverse line 108
  19. theorem OAI.CompanionFPP.Calibration.le_pathCost line 113
  20. def OAI.CompanionFPP.Calibration.defect line 120
  21. theorem OAI.CompanionFPP.Calibration.defect_nonneg line 122
  22. theorem OAI.CompanionFPP.Calibration.defect_append line 125
  23. theorem OAI.CompanionFPP.Calibration.defect_subpath_le line 130
  24. theorem OAI.CompanionFPP.Calibration.defect_eq_centered line 138