OAI/Probability/FirstPassage/Translation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFPP.shiftEdge line 8
2. theorem OAI.PlanarFPP.shiftEdge_injective line 10
3. theorem OAI.PlanarFPP.step_edge_translate line 14
4. theorem OAI.PlanarFPP.pathCost_translate line 18
5. theorem OAI.PlanarFPP.passageTime_translate line 24
6. theorem OAI.PlanarFPP.ExponentialEnvironment.translate line 33
7. theorem OAI.PlanarFPP.ExponentialEnvironment.jointLaw line 40
8. theorem OAI.PlanarFPP.translated_event_probability line 45