OAI/Probability/FirstPassage/GridCounting.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFPP.gridIndexRange line 8
2. lemma OAI.PlanarFPP.gridIndexRange_card line 11
3. lemma OAI.PlanarFPP.mem_gridIndexRange_of_abs_le line 15
4. def OAI.PlanarFPP.gridTestIndices line 21
5. def OAI.PlanarFPP.gridIndexConstant line 24
6. lemma OAI.PlanarFPP.gridIndexConstant_pos line 27
7. lemma OAI.PlanarFPP.gridTestIndices_card line 30
8. lemma OAI.PlanarFPP.gridTestIndices_level_card line 49
9. lemma OAI.PlanarFPP.grid_interval_index_mem line 74
10. lemma OAI.PlanarFPP.grid_bin_floor line 98