OAI/Probability/FirstPassage/ContiguousWitnesses.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PlanarFPP.trace_append line 8
2. lemma OAI.PlanarFPP.trace_split line 14
3. lemma OAI.PlanarFPP.trace_edges line 30
4. lemma OAI.PlanarFPP.simple_append_edges line 36
5. theorem OAI.PlanarFPP.spatial_negative_prefix_witnesses line 47