OAI/Probability/ThorpShuffle/Classification.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Thorp.Young.rowCellsEquiv line 15

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

  2. lemma OAI.Thorp.Young.card_cells_eq_sum line 22
  3. def OAI.Thorp.Young.ofPartition line 27

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

  4. lemma OAI.Thorp.Young.rowLens_ofPartition line 30
  5. lemma OAI.Thorp.Young.card_ofPartition line 36
  6. lemma OAI.Thorp.Young.ofPartition_injective line 40
  7. def OAI.Thorp.Young.toPartition line 47
  8. lemma OAI.Thorp.Young.of_toPartition line 52
  9. def OAI.Thorp.Fourier.charPair line 68
  10. lemma OAI.Thorp.Fourier.charPair_sum line 70
  11. lemma OAI.Thorp.Fourier.charPair_zero line 80
  12. lemma OAI.Thorp.Fourier.irreducible_char_independent line 82
  13. abbrev OAI.Thorp.Specht.Shape line 108

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

  14. def OAI.Thorp.Specht.canonicalTableau line 110

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

  15. abbrev OAI.Thorp.Specht.Space line 125

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

  16. def OAI.Thorp.Specht.family line 127
  17. instance OAI.Thorp.Specht.family_irreducible line 130
  18. lemma OAI.Thorp.Specht.family_inequiv line 133
  19. lemma OAI.Thorp.Specht.characters_independent line 138
  20. def OAI.Thorp.Specht.classLift line 141
  21. lemma OAI.Thorp.Specht.classLift_apply line 144
  22. lemma OAI.Thorp.Specht.character_isClass line 152
  23. lemma OAI.Thorp.Specht.liftedCharacters_independent line 158
  24. def OAI.Thorp.Specht.characterBasis line 169
  25. lemma OAI.Thorp.Specht.characterBasis_apply line 172
  26. lemma OAI.Thorp.Specht.class_expansion line 181
  27. lemma OAI.Thorp.Specht.char_orthogonal line 190
  28. lemma OAI.Thorp.Specht.class_coeff line 199
  29. def OAI.Thorp.Specht.degree line 208

    Distinct definitions of this name: ComparatorChallenges/ThorpFirstReciprocal.lean:185 (same statement text; different proof or body). Qualify references as OAI.Thorp.Specht.degree@path.

  30. theorem OAI.Thorp.Specht.regular_char line 210
  31. theorem OAI.Thorp.Specht.degree_sq_sum line 234