OAI/Probability/BinarySweep/SparseBounds/SparseReduction.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinaryCoordinateSweeps.Young.minTail line 20
2. lemma OAI.BinaryCoordinateSweeps.Young.diagramF_le_rowTail line 23
3. lemma OAI.BinaryCoordinateSweeps.Young.diagramF_transpose line 36
4. lemma OAI.BinaryCoordinateSweeps.Young.minTail_orientation line 40
5. lemma OAI.BinaryCoordinateSweeps.Young.diagramF_le_minTail line 47
6. lemma OAI.BinaryCoordinateSweeps.Young.minTail_le_diagramF line 55
7. lemma OAI.BinaryCoordinateSweeps.const_mul_rpow_eventually line 68
8. lemma OAI.BinaryCoordinateSweeps.sparse_reduction_eventually line 78
9. lemma OAI.BinaryCoordinateSweeps.outside_card_mul_axis line 144
10. lemma OAI.BinaryCoordinateSweeps.outside_inv_axis_ratio line 152
11. lemma OAI.BinaryCoordinateSweeps.many_axis_size_bound line 160
12. lemma OAI.BinaryCoordinateSweeps.many_collision_base_eventually line 175