OAI/Probability/FirstPassage/LatticeSwap.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarFPP.swapStep line 9
  2. lemma OAI.PlanarFPP.swapStep_swap line 15
  3. lemma OAI.PlanarFPP.swapStep_delta line 16
  4. def OAI.PlanarFPP.swapEdge line 18
  5. lemma OAI.PlanarFPP.swapEdge_swap line 19
  6. lemma OAI.PlanarFPP.swapEdge_injective line 20
  7. lemma OAI.PlanarFPP.swapStep_edge line 22
  8. lemma OAI.PlanarFPP.displacement_swap line 25
  9. lemma OAI.PlanarFPP.pathCost_swap line 30
  10. lemma OAI.PlanarFPP.passageTime_swap line 36
  11. def OAI.PlanarFPP.swapPlane line 52
  12. lemma OAI.PlanarFPP.swapPlane_zero line 55
  13. lemma OAI.PlanarFPP.swapPlane_one line 57
  14. lemma OAI.PlanarFPP.swapPlane_swap line 59
  15. lemma OAI.PlanarFPP.latticeFloor_swap line 62
  16. lemma OAI.PlanarFPP.ExponentialEnvironment.swap line 67
  17. theorem OAI.PlanarFPP.actualSourceTimeConstant_swap line 74