OAI/RepresentationTheory/PartialPermutation/TailBounds.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartialPermutation.Tableau.transposeCellsEquiv line 13
2. lemma OAI.PartialPermutation.Tableau.standardCount_transpose line 21
3. lemma OAI.PartialPermutation.Tableau.card_transpose line 24
4. lemma OAI.PartialPermutation.Tableau.maxLine_transpose line 27
5. lemma OAI.PartialPermutation.Tableau.deficit_transpose line 30
6. lemma OAI.PartialPermutation.Tableau.two_pow_le_centralBinom line 33
7. lemma OAI.PartialPermutation.Tableau.tail_power_lower_bound_oriented line 49
8. lemma OAI.PartialPermutation.Tableau.tail_power_lower_bound line 77
9. lemma OAI.PartialPermutation.Tableau.longest_binomial_lower_bound line 84
10. lemma OAI.PartialPermutation.Tableau.linear_le_choose line 98
11. lemma OAI.PartialPermutation.Tableau.fixed_deficit_growth line 112