OAI/Probability/SignedSweeps/SignedPairDimension.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SignedSweeps.signed_hook_prefix_dimension_lower line 11
2. theorem OAI.SignedSweeps.signed_pair_dimension_factorial_lower line 36
3. lemma OAI.SignedSweeps.rowLen_zero_of_height_le line 62
4. lemma OAI.SignedSweeps.rowLen_sum_range line 69
5. lemma OAI.SignedSweeps.partsEntropy_rowLen_range line 81
6. lemma OAI.SignedSweeps.partsEntropy_rowLen_log line 91
7. lemma OAI.SignedSweeps.log_factorial_upper_uniform line 111
8. lemma OAI.SignedSweeps.row_log_factorials_le line 122
9. theorem OAI.SignedSweeps.signed_pair_log_dimension_lower line 133