OAI/Probability/ThorpRouting/SparseSaving/ShapePartitionEquiv.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ThorpNine.SparseSaving.Thorp.Specht.shapePartitionEquiv line 11
2. instance OAI.ThorpNine.SparseSaving.Thorp.Specht.(instance at line 25) line 25
3. def OAI.ThorpNine.SparseSaving.Thorp.Specht.conjugacyPartition line 27
4. lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.conjugacyPartition_injective line 31
5. lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.card_conjugacy_le_shapes line 39
6. def OAI.ThorpNine.SparseSaving.Thorp.Specht.labels line 44
7. def OAI.ThorpNine.SparseSaving.Thorp.Specht.labelledRepresentation line 47
8. lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.labelledRepresentation_irreducible line 51
9. lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.labelledRepresentation_equiv_shapes line 77
10. def OAI.ThorpNine.SparseSaving.Thorp.FiniteCharacters.classRep line 102
11. lemma OAI.ThorpNine.SparseSaving.Thorp.FiniteCharacters.classRep_spec line 104
12. def OAI.ThorpNine.SparseSaving.Thorp.FiniteCharacters.characterClass line 109
13. lemma OAI.ThorpNine.SparseSaving.Thorp.FiniteCharacters.characterClass_mk line 113
14. def OAI.ThorpNine.SparseSaving.Thorp.FiniteCharacters.characterDual line 120
15. lemma OAI.ThorpNine.SparseSaving.Thorp.FiniteCharacters.characterDual_characterClass line 130
16. theorem OAI.ThorpNine.SparseSaving.Thorp.FiniteCharacters.complete_of_card_conjugacy_le line 142
17. theorem OAI.ThorpNine.SparseSaving.Thorp.Specht.labelled_complete line 191
18. def OAI.ThorpNine.SparseSaving.Thorp.PermutationHilbert.act line 212
19. lemma OAI.ThorpNine.SparseSaving.Thorp.PermutationHilbert.act_apply line 215
20. lemma OAI.ThorpNine.SparseSaving.Thorp.PermutationHilbert.act_single line 218
21. lemma OAI.ThorpNine.SparseSaving.Thorp.PermutationHilbert.trace_projection line 222
22. lemma OAI.ThorpNine.SparseSaving.Thorp.PermutationHilbert.projection_diagonal line 235
23. lemma OAI.ThorpNine.SparseSaving.Thorp.PermutationHilbert.projection_comm line 248
24. lemma OAI.ThorpNine.SparseSaving.Thorp.PermutationHilbert.uniform_diagonal line 256
25. theorem OAI.ThorpNine.SparseSaving.Thorp.PermutationHilbert.uncertainty line 273
26. lemma OAI.ThorpNine.SparseSaving.Thorp.PermutationHilbert.trace_projection_real line 299
27. theorem OAI.ThorpNine.SparseSaving.Thorp.PermutationHilbert.footprint_dimension line 305
28. lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.finrank_hilbertSpace line 335
29. lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.hilbert_action line 339
30. lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.hilbertSpace_invariant line 345
31. lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.tabloidAct_transitive line 360
32. lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.polytabloid_pairing line 370
33. lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.polytabloid_norm_sq line 382
34. theorem OAI.ThorpNine.SparseSaving.Thorp.Specht.dimension_times_column_ge_tabloids line 390
35. def OAI.ThorpNine.SparseSaving.Thorp.Specht.fiberGroupEquiv line 406
36. lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.nat_card_fiberGroup line 433
37. lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.card_fiberGroups_mul_le line 440
38. def OAI.ThorpNine.SparseSaving.Thorp.Specht.rowGroup line 467
39. def OAI.ThorpNine.SparseSaving.Thorp.Specht.colIndex line 470
40. lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.colGroup_eq line 473
41. instance OAI.ThorpNine.SparseSaving.Thorp.Specht.tabloidMulAction line 479
42. lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.tabloid_orbit_all line 484
43. lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.tabloid_stabilizer line 491
44. lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.card_tabloid_mul_row line 504
45. theorem OAI.ThorpNine.SparseSaving.Thorp.Specht.factorial_le_dimension_row_column line 513
46. lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.card_row_fiber line 519
47. lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.card_col_fiber line 525
48. lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.card_rowGroup line 531
49. lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.card_colGroup line 537
50. abbrev OAI.ThorpNine.SparseSaving.Thorp.Specht.Tail line 542
51. lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.tail_card line 544
52. lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.rowLen_zero_le_card line 549
53. def OAI.ThorpNine.SparseSaving.Thorp.Specht.tailColumnEquiv line 553
54. lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.card_tail_col line 573
55. lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.card_tail_row line 577
56. lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.tail_row_group line 592
57. lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.sum_tail_columns line 619
58. lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.column_pos line 624
59. lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.nat_le_two_pow_pred line 627
60. lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.column_group_le_tail line 634
61. theorem OAI.ThorpNine.SparseSaving.Thorp.Specht.choose_tail_le_dimension line 651
62. lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.exists_perm_mem_iff line 685
63. def OAI.ThorpNine.SparseSaving.Thorp.Specht.tailSet line 704
64. lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.mem_tailSet line 707
65. lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.tailSet_act line 710
66. lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.card_tailSet line 718
67. def OAI.ThorpNine.SparseSaving.Thorp.Specht.footprint line 726
68. lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.tail_fiber_card_eq line 729
69. lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.footprint_card_product line 746
70. lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.footprint_fixed line 778
71. def OAI.ThorpNine.SparseSaving.Thorp.Specht.fixedHilbert line 797
72. lemma OAI.ThorpNine.SparseSaving.Thorp.Specht.fixedHilbert_le line 807
73. theorem OAI.ThorpNine.SparseSaving.Thorp.Specht.fixedHilbert_dimension line 810
74. def OAI.ThorpNine.SparseSaving.Thorp.UnitaryFinite.IsUnitary line 842
75. lemma OAI.ThorpNine.SparseSaving.Thorp.UnitaryFinite.unitary_inner_inv line 846
76. def OAI.ThorpNine.SparseSaving.Thorp.UnitaryFinite.averageMap line 856