OAI/Probability/BinarySweep/FiniteLaws/SoutheastDimension.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BinaryCoordinateSweeps.Young.southeast_height_mul_le_card line 17
2. lemma OAI.BinaryCoordinateSweeps.Young.southeast_width_mul_le_card line 33
3. lemma OAI.BinaryCoordinateSweeps.Young.southeast_diagonal_bound line 49
4. theorem OAI.BinaryCoordinateSweeps.Young.southeast_log_dimension_lower line 58
5. lemma OAI.BinaryCoordinateSweeps.Young.hook_log_dimension_upper line 79
6. lemma OAI.BinaryCoordinateSweeps.Young.southeast_dense_saving line 99