OAI/Probability/BinarySweep/GridBounds/GridDenseCost.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BinaryCoordinateSweeps.GridSplit.sum_row_holes line 17
2. lemma OAI.BinaryCoordinateSweeps.GridSplit.sum_column_holes line 22
3. lemma OAI.BinaryCoordinateSweeps.GridSplit.child_error_sum line 28
4. lemma OAI.BinaryCoordinateSweeps.GridSplit.blockLogSize_le line 41
5. lemma OAI.BinaryCoordinateSweeps.GridSplit.blocksLog_le line 50
6. theorem OAI.BinaryCoordinateSweeps.GridSplit.conditional_hook_with_cost line 62
7. def OAI.BinaryCoordinateSweeps.inductionGap line 106
8. lemma OAI.BinaryCoordinateSweeps.dense_error_eventually line 108
9. theorem OAI.BinaryCoordinateSweeps.dense_induction_absorption_eventually line 148