OAI/Probability/ThorpShuffle/LinearExtensions.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Thorp.Young.Extensions line 17
2. instance OAI.Thorp.Young.(instance at line 19) line 19
3. lemma OAI.Thorp.Young.labelByKey line 23
4. lemma OAI.Thorp.Young.labelByRank line 32
5. lemma OAI.Thorp.Young.extensions_nonempty line 54
6. lemma OAI.Thorp.Young.fiberPerm_le_extensions line 62
7. lemma OAI.Thorp.Specht.tabloid_card_mul line 84
8. lemma OAI.Thorp.Specht.tabloid_card_le line 108
9. theorem OAI.Thorp.Young.rank_extension_bound line 129
10. lemma OAI.Thorp.Specht.labels_card_le_degree line 140
11. lemma OAI.Thorp.Specht.extensions_card_le_degree line 156
12. def OAI.Thorp.Young.transposeCells line 176
13. lemma OAI.Thorp.Young.extensions_card_orderIso line 186
14. lemma OAI.Thorp.Young.rank_strictMono line 196
15. def OAI.Thorp.Young.longest line 207

    Also declared: ComparatorChallenges/ThorpFirstReciprocal.lean:60 (same declaration text).

16. lemma OAI.Thorp.Young.coord_lt_longest line 209
17. theorem OAI.Thorp.Young.factorial_le_rank_degree line 215