OAI/Probability/BinarySweep/GridBounds/GridSplitCost.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BinaryCoordinateSweeps.GridSplit.left_path_address line 17
2. lemma OAI.BinaryCoordinateSweeps.GridSplit.right_path_address line 26
3. lemma OAI.BinaryCoordinateSweeps.GridSplit.card_pair_fiber line 35
4. lemma OAI.BinaryCoordinateSweeps.GridSplit.lineHoles_left line 51
5. lemma OAI.BinaryCoordinateSweeps.GridSplit.lineHoles_right line 68
6. theorem OAI.BinaryCoordinateSweeps.GridSplit.pathCost_split line 85
7. def OAI.BinaryCoordinateSweeps.GridSplit.rowFreeSize line 123
8. def OAI.BinaryCoordinateSweeps.GridSplit.columnFreeSize line 124
9. lemma OAI.BinaryCoordinateSweeps.GridSplit.holeCount_junction line 126
10. theorem OAI.BinaryCoordinateSweeps.GridSplit.conditional_dense_bound line 136
11. theorem OAI.BinaryCoordinateSweeps.GridSplit.conditional_hook_dense_bound line 163