OAI/Probability/FirstPassage/PathWitnesses.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PlanarFPP.Traversal line 8
2. def OAI.PlanarFPP.traversalEdge line 10
3. def OAI.PlanarFPP.trace line 12
4. def OAI.PlanarFPP.stepDefect line 16
5. theorem OAI.PlanarFPP.support_zero line 19
6. theorem OAI.PlanarFPP.trace_total_defect line 22
7. theorem OAI.PlanarFPP.support_step_bound line 30
8. theorem OAI.PlanarFPP.path_witness_decomposition line 48