OAI/Probability/FirstPassage/EndpointCoarseGeometry.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PlanarFPP.gridMesh_scale_bound line 8
2. def OAI.PlanarFPP.coarseColumnIndices line 12
3. lemma OAI.PlanarFPP.coarse_column_index line 15
4. def OAI.PlanarFPP.coarseRegionFactor line 26
5. lemma OAI.PlanarFPP.endpointBox_into_rareFastRegion line 28