OAI/Probability/BinarySweep/YoungTheory/YoungDimensionLower.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BinaryCoordinateSweeps.Young.two_pow_card_sub_diagonal_le_dimension line 12
2. theorem OAI.BinaryCoordinateSweeps.Young.log_dimension_lower line 25
3. lemma OAI.BinaryCoordinateSweeps.Young.tail_min_eq_card_sub_max line 44
4. theorem OAI.BinaryCoordinateSweeps.Young.log_dimension_lower_min_tail line 48