OAI/Probability/FirstPassage/SpatialChunks.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PlanarFPP.spatial_chunk_decomposition line 8
2. lemma OAI.PlanarFPP.spatial_chunk_displacement_bound line 28
3. def OAI.PlanarFPP.chunkIndexTail line 45
4. def OAI.PlanarFPP.BoundedIndexSteps line 49
5. lemma OAI.PlanarFPP.chunkIndexTail_length line 53
6. lemma OAI.PlanarFPP.chunkIndexTail_bounded line 59