OAI/Probability/FirstPassage/CompanionModel.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PlanarFPP.companion_adj_step line 10
  2. lemma OAI.PlanarFPP.companion_adj_iff line 14
  3. def OAI.PlanarFPP.companionEdge line 31
  4. lemma OAI.PlanarFPP.companionEdge_step line 35
  5. lemma OAI.PlanarFPP.companionEdge_injective line 40
  6. lemma OAI.PlanarFPP.companionEdge_surjective line 47
  7. def OAI.PlanarFPP.companionEdgeEquiv line 54
  8. def OAI.PlanarFPP.companionWeights line 57
  9. lemma OAI.PlanarFPP.companionWeights_edge line 60
  10. lemma OAI.PlanarFPP.companion_pathCost_copy line 65
  11. lemma OAI.PlanarFPP.steps_companion_walk line 70
  12. lemma OAI.PlanarFPP.companion_walk_steps line 86
  13. theorem OAI.PlanarFPP.companion_passageTime_eq line 99
  14. theorem OAI.PlanarFPP.ExponentialEnvironment.companionLaw line 115
  15. lemma OAI.PlanarFPP.measurable_companionWeights line 123