OAI/Probability/ThorpRouting/Harmonic/Shapes.lean

GitHub source file

79 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.partitionDiagram_rowLens line 11

    Also declared: ComparatorChallenges/CoordinateTrace.lean:283 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:360 (same declaration text).

  2. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.partitionDiagram_card line 17

    Also declared: ComparatorChallenges/CoordinateTrace.lean:289 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:366 (same declaration text).

  3. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.partitionDiagram_diagramPartition line 22

    Also declared: ComparatorChallenges/CoordinateTrace.lean:294 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:371 (same declaration text).

  4. abbrev OAI.ThorpNine.Harmonic.Thorp.Specht.Shapes line 31

    Also declared: ComparatorChallenges/CoordinateTrace.lean:303 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:380 (same declaration text).

  5. def OAI.ThorpNine.Harmonic.Thorp.Specht.shapePartitionEquiv line 33

    Also declared: ComparatorChallenges/CoordinateTrace.lean:305 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:382 (same declaration text).

  6. instance OAI.ThorpNine.Harmonic.Thorp.Specht.(instance at line 47) line 47
  7. def OAI.ThorpNine.Harmonic.Thorp.Specht.conjugacyPartition line 49
  8. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.conjugacyPartition_injective line 53
  9. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.card_conjugacy_le_shapes line 61
  10. def OAI.ThorpNine.Harmonic.Thorp.Specht.labels line 66

    Also declared: ComparatorChallenges/CoordinateTrace.lean:321 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:398 (same declaration text).

  11. def OAI.ThorpNine.Harmonic.Thorp.Specht.labelledRepresentation line 69
  12. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.labelledRepresentation_irreducible line 73
  13. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.labelledRepresentation_equiv_shapes line 99
  14. def OAI.ThorpNine.Harmonic.Thorp.FiniteCharacters.classRep line 124
  15. lemma OAI.ThorpNine.Harmonic.Thorp.FiniteCharacters.classRep_spec line 126
  16. def OAI.ThorpNine.Harmonic.Thorp.FiniteCharacters.characterClass line 131
  17. lemma OAI.ThorpNine.Harmonic.Thorp.FiniteCharacters.characterClass_mk line 135
  18. def OAI.ThorpNine.Harmonic.Thorp.FiniteCharacters.characterDual line 142
  19. lemma OAI.ThorpNine.Harmonic.Thorp.FiniteCharacters.characterDual_characterClass line 152
  20. theorem OAI.ThorpNine.Harmonic.Thorp.FiniteCharacters.complete_of_card_conjugacy_le line 164
  21. theorem OAI.ThorpNine.Harmonic.Thorp.Specht.labelled_complete line 213
  22. def OAI.ThorpNine.Harmonic.Thorp.PermutationHilbert.act line 234
  23. lemma OAI.ThorpNine.Harmonic.Thorp.PermutationHilbert.act_apply line 237
  24. lemma OAI.ThorpNine.Harmonic.Thorp.PermutationHilbert.act_single line 240
  25. lemma OAI.ThorpNine.Harmonic.Thorp.PermutationHilbert.trace_projection line 244
  26. lemma OAI.ThorpNine.Harmonic.Thorp.PermutationHilbert.projection_diagonal line 257
  27. lemma OAI.ThorpNine.Harmonic.Thorp.PermutationHilbert.projection_comm line 270
  28. lemma OAI.ThorpNine.Harmonic.Thorp.PermutationHilbert.uniform_diagonal line 278
  29. theorem OAI.ThorpNine.Harmonic.Thorp.PermutationHilbert.uncertainty line 295
  30. lemma OAI.ThorpNine.Harmonic.Thorp.PermutationHilbert.trace_projection_real line 321
  31. theorem OAI.ThorpNine.Harmonic.Thorp.PermutationHilbert.footprint_dimension line 327
  32. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.finrank_hilbertSpace line 357
  33. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.hilbert_action line 361
  34. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.hilbertSpace_invariant line 367
  35. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.tabloidAct_transitive line 382
  36. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.polytabloid_pairing line 392
  37. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.polytabloid_norm_sq line 404
  38. theorem OAI.ThorpNine.Harmonic.Thorp.Specht.dimension_times_column_ge_tabloids line 412
  39. def OAI.ThorpNine.Harmonic.Thorp.Specht.fiberGroupEquiv line 428
  40. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.nat_card_fiberGroup line 455
  41. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.card_fiberGroups_mul_le line 462
  42. def OAI.ThorpNine.Harmonic.Thorp.Specht.rowGroup line 489
  43. def OAI.ThorpNine.Harmonic.Thorp.Specht.colIndex line 492
  44. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.colGroup_eq line 495
  45. instance OAI.ThorpNine.Harmonic.Thorp.Specht.tabloidMulAction line 501
  46. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.tabloid_orbit_all line 506
  47. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.tabloid_stabilizer line 513
  48. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.card_tabloid_mul_row line 526
  49. theorem OAI.ThorpNine.Harmonic.Thorp.Specht.factorial_le_dimension_row_column line 535
  50. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.card_row_fiber line 541
  51. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.card_col_fiber line 547
  52. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.card_rowGroup line 553
  53. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.card_colGroup line 559
  54. abbrev OAI.ThorpNine.Harmonic.Thorp.Specht.Tail line 564
  55. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.tail_card line 566
  56. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.rowLen_zero_le_card line 571
  57. def OAI.ThorpNine.Harmonic.Thorp.Specht.tailColumnEquiv line 575
  58. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.card_tail_col line 595
  59. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.card_tail_row line 599
  60. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.tail_row_group line 614
  61. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.sum_tail_columns line 641
  62. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.column_pos line 646
  63. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.nat_le_two_pow_pred line 649
  64. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.column_group_le_tail line 656
  65. theorem OAI.ThorpNine.Harmonic.Thorp.Specht.choose_tail_le_dimension line 673
  66. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.exists_perm_mem_iff line 707
  67. def OAI.ThorpNine.Harmonic.Thorp.Specht.tailSet line 726
  68. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.mem_tailSet line 729
  69. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.tailSet_act line 732
  70. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.card_tailSet line 740
  71. def OAI.ThorpNine.Harmonic.Thorp.Specht.footprint line 748
  72. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.tail_fiber_card_eq line 751
  73. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.footprint_card_product line 768
  74. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.footprint_fixed line 800
  75. def OAI.ThorpNine.Harmonic.Thorp.Specht.fixedHilbert line 819
  76. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.fixedHilbert_le line 829
  77. theorem OAI.ThorpNine.Harmonic.Thorp.Specht.fixedHilbert_dimension line 832
  78. def OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.IsUnitary line 864
  79. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.unitary_inner_inv line 868