OAI/Probability/BinarySweep/GridBounds/DiagonalDimension.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BinaryCoordinateSweeps.Young.factorial_le_diagonal_dimension line 15
2. lemma OAI.BinaryCoordinateSweeps.Young.specht_dimension_pos line 30
3. theorem OAI.BinaryCoordinateSweeps.Young.log_dimension_lower_of_diagonal_bound line 33
4. lemma OAI.BinaryCoordinateSweeps.Young.diagonal_lt_height_add_width line 53
5. lemma OAI.BinaryCoordinateSweeps.Young.width_add_rectangle_le_card line 62
6. lemma OAI.BinaryCoordinateSweeps.Young.height_add_rectangle_le_card line 99
7. lemma OAI.BinaryCoordinateSweeps.Young.height_width_le_card line 107
8. lemma OAI.BinaryCoordinateSweeps.Young.diagonal_twice_le line 121
9. lemma OAI.BinaryCoordinateSweeps.Young.diagonal_lt_half_card_add_max line 149
10. def OAI.BinaryCoordinateSweeps.Young.assembleFiberPerm line 163
11. lemma OAI.BinaryCoordinateSweeps.Young.assembleFiberPerm_injective line 170
12. lemma OAI.BinaryCoordinateSweeps.Young.product_factorial_le_stabilizer line 177
13. lemma OAI.BinaryCoordinateSweeps.Young.two_pow_sub_one_le_factorial line 182
14. lemma OAI.BinaryCoordinateSweeps.Young.two_pow_card_sub_colors_le_stabilizer line 193