OAI/Probability/FirstPassage/RareFastGeometry.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFPP.blockLayer line 9
2. def OAI.PlanarFPP.blockLevel line 11
3. def OAI.PlanarFPP.blockX line 13
4. def OAI.PlanarFPP.blockY line 15
5. def OAI.PlanarFPP.blockRegion line 17
6. theorem OAI.PlanarFPP.centers_close_of_point line 21
7. theorem OAI.PlanarFPP.blockRegion_common_indices line 29
8. theorem OAI.PlanarFPP.blockRegion_common_near line 54
9. theorem OAI.PlanarFPP.blockRegion_disjoint line 90