OAI/Probability/FirstPassage/WitnessSelection.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFPP.takeWitnessPacks line 8
2. lemma OAI.PlanarFPP.takeWitnessPacks_length line 12
3. lemma OAI.PlanarFPP.takeWitnessPacks_flatten line 18
4. lemma OAI.PlanarFPP.takeWitnessPacks_assign line 24
5. lemma OAI.PlanarFPP.long_path_witness_count line 33
6. def OAI.PlanarFPP.witnessLabels line 42
7. lemma OAI.PlanarFPP.witnessLabels_length line 47
8. theorem OAI.PlanarFPP.witnessPacks_strictDisjoint line 56