OAI/Probability/ThorpShuffle/DegreeBounds.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Thorp.Young.rowTail line 13
  2. lemma OAI.Thorp.Young.mem_rowTail line 24
  3. def OAI.Thorp.Young.rowTailCells line 37
  4. lemma OAI.Thorp.Young.rowTail_ext line 47
  5. def OAI.Thorp.Young.orient line 55
  6. def OAI.Thorp.Young.orientation line 58
  7. lemma OAI.Thorp.Young.orient_rowLen line 60
  8. lemma OAI.Thorp.Young.orient_card line 66
  9. lemma OAI.Thorp.Young.orient_extensions line 72
  10. lemma OAI.Thorp.Young.recover_orientation line 80
  11. lemma OAI.Thorp.Young.longest_le_card line 85
  12. theorem OAI.Thorp.Young.defect_count_le line 88
  13. abbrev OAI.Thorp.Specht.NShape line 127

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

  14. def OAI.Thorp.Specht.defect line 129

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

  15. lemma OAI.Thorp.Specht.diagram_card line 131
  16. lemma OAI.Thorp.Specht.extensions_le_degree line 134
  17. lemma OAI.Thorp.Specht.degree_pos line 138
  18. lemma OAI.Thorp.Specht.defect_add_longest line 142
  19. lemma OAI.Thorp.Specht.choose_longest_le_degree line 147
  20. lemma OAI.Thorp.Specht.small_defect_degree line 159
  21. lemma OAI.Thorp.Specht.fixed_defect_degree line 165
  22. lemma OAI.Thorp.Specht.factorial_third_bound line 173
  23. lemma OAI.Thorp.Specht.small_longest_degree line 187
  24. lemma OAI.Thorp.Specht.bulk_degree line 203
  25. lemma OAI.Thorp.Specht.defect_card_bound line 219