OAI/Probability/FirstPassage/SpatialWitnesses.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFPP.spatialWitnessFamily line 9
2. lemma OAI.PlanarFPP.spatialWitness_good_event line 18
3. lemma OAI.PlanarFPP.spatialRareEvent_has_witness line 42
4. lemma OAI.PlanarFPP.translatedEndpointBox_finite line 63
5. def OAI.PlanarFPP.spatialWitnessVertices line 69
6. def OAI.PlanarFPP.spatialWitnessSupport line 73
7. lemma OAI.PlanarFPP.spatialWitness_edges line 76
8. lemma OAI.PlanarFPP.spatialWitness_event_iff line 87
9. def OAI.PlanarFPP.spatialListSupport line 97
10. theorem OAI.PlanarFPP.exponential_spatial_witness_BK line 102
11. theorem OAI.PlanarFPP.actual_spatial_witness_BK_scales line 131