OAI/Probability/ThorpRouting/Tail/ModifiedReverseEquiv.lean

GitHub source file

82 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ThorpNine.Tail.Thorp.modifiedReverseEquiv line 10
  2. lemma OAI.ThorpNine.Tail.Thorp.modifiedPerm_reverse line 16
  3. lemma OAI.ThorpNine.Tail.Thorp.modified_kernel_symmetric line 37
  4. lemma OAI.ThorpNine.Tail.Thorp.Specht.card_cell line 49
  5. def OAI.ThorpNine.Tail.Thorp.Specht.columnEquiv line 52
  6. def OAI.ThorpNine.Tail.Thorp.Specht.columnValues line 59
  7. lemma OAI.ThorpNine.Tail.Thorp.Specht.mem_columnValues line 62
  8. lemma OAI.ThorpNine.Tail.Thorp.Specht.card_columnValues line 67
  9. lemma OAI.ThorpNine.Tail.Thorp.Specht.strictMono_fin_nat_ge line 77
  10. def OAI.ThorpNine.Tail.Thorp.Specht.rankCell line 91
  11. lemma OAI.ThorpNine.Tail.Thorp.Specht.rankCell_col line 97
  12. lemma OAI.ThorpNine.Tail.Thorp.Specht.rankCell_orderEmb line 101
  13. lemma OAI.ThorpNine.Tail.Thorp.Specht.rankCell_injective line 110
  14. def OAI.ThorpNine.Tail.Thorp.Specht.rankPerm line 124
  15. lemma OAI.ThorpNine.Tail.Thorp.Specht.rankCell_row_le line 128
  16. theorem OAI.ThorpNine.Tail.Thorp.Specht.column_transporter line 134
  17. lemma OAI.ThorpNine.Tail.Thorp.Specht.tabloidAct_inv line 147
  18. lemma OAI.ThorpNine.Tail.Thorp.Specht.tabloidRep_apply line 152
  19. lemma OAI.ThorpNine.Tail.Thorp.Specht.tabloidRep_delta line 155
  20. lemma OAI.ThorpNine.Tail.Thorp.Specht.mem_colGroup line 163
  21. lemma OAI.ThorpNine.Tail.Thorp.Specht.colGroup_row_stabilizer line 166
  22. lemma OAI.ThorpNine.Tail.Thorp.Specht.tabloid_column_transporter line 175
  23. lemma OAI.ThorpNine.Tail.Thorp.Specht.permSign_one line 193
  24. lemma OAI.ThorpNine.Tail.Thorp.Specht.permSign_mul line 195
  25. lemma OAI.ThorpNine.Tail.Thorp.Specht.permSign_inv line 197
  26. lemma OAI.ThorpNine.Tail.Thorp.Specht.permSign_sq line 199
  27. lemma OAI.ThorpNine.Tail.Thorp.Specht.permSign_swap line 204
  28. lemma OAI.ThorpNine.Tail.Thorp.Specht.conj_permSign line 206
  29. lemma OAI.ThorpNine.Tail.Thorp.Specht.alternator_mul line 211
  30. lemma OAI.ThorpNine.Tail.Thorp.Specht.mul_alternator line 226
  31. lemma OAI.ThorpNine.Tail.Thorp.Specht.alternator_apply_action line 241
  32. lemma OAI.ThorpNine.Tail.Thorp.Specht.action_alternator_apply line 246
  33. lemma OAI.ThorpNine.Tail.Thorp.Specht.alternator_eq_zero_of_odd_stabilizer line 251
  34. lemma OAI.ThorpNine.Tail.Thorp.Specht.swap_mem_colGroup line 267
  35. lemma OAI.ThorpNine.Tail.Thorp.Specht.swap_fixes_tabloid line 277
  36. lemma OAI.ThorpNine.Tail.Thorp.Specht.alternator_delta_rank_one line 289
  37. lemma OAI.ThorpNine.Tail.Thorp.Specht.polytabloid_formula line 305
  38. lemma OAI.ThorpNine.Tail.Thorp.Specht.polytabloid_base line 311
  39. lemma OAI.ThorpNine.Tail.Thorp.Specht.polytabloid_ne_zero line 324
  40. lemma OAI.ThorpNine.Tail.Thorp.Specht.delta_decomposition line 329
  41. theorem OAI.ThorpNine.Tail.Thorp.Specht.alternator_rank_one line 336
  42. lemma OAI.ThorpNine.Tail.Thorp.Specht.alternator_rank_one_exact line 344
  43. def OAI.ThorpNine.Tail.Thorp.Specht.pairing line 352
  44. lemma OAI.ThorpNine.Tail.Thorp.Specht.pairing_delta line 355
  45. lemma OAI.ThorpNine.Tail.Thorp.Specht.pairing_sum_left line 360
  46. lemma OAI.ThorpNine.Tail.Thorp.Specht.pairing_smul_left line 366
  47. lemma OAI.ThorpNine.Tail.Thorp.Specht.pairing_zero_left line 373
  48. lemma OAI.ThorpNine.Tail.Thorp.Specht.pairing_add_left line 376
  49. lemma OAI.ThorpNine.Tail.Thorp.Specht.pairing_self_eq_zero line 380
  50. lemma OAI.ThorpNine.Tail.Thorp.Specht.pairing_action line 388
  51. lemma OAI.ThorpNine.Tail.Thorp.Specht.alternator_base_pairing line 399
  52. theorem OAI.ThorpNine.Tail.Thorp.Specht.alternator_pairing line 409
  53. lemma OAI.ThorpNine.Tail.Thorp.Specht.polytabloid_mem_space line 414
  54. lemma OAI.ThorpNine.Tail.Thorp.Specht.alternator_mem_invariant line 417
  55. theorem OAI.ThorpNine.Tail.Thorp.Specht.submodule_theorem line 424
  56. theorem OAI.ThorpNine.Tail.Thorp.Specht.space_simple line 455
  57. lemma OAI.ThorpNine.Tail.Thorp.Specht.space_ne_bot line 466
  58. theorem OAI.ThorpNine.Tail.Thorp.Specht.representation_irreducible line 472
  59. def OAI.ThorpNine.Tail.Thorp.Specht.symmetrizer line 511
  60. lemma OAI.ThorpNine.Tail.Thorp.Specht.symmetrizer_mul line 515
  61. lemma OAI.ThorpNine.Tail.Thorp.Specht.symmetrizer_eq_zero_of_neg line 521
  62. def OAI.ThorpNine.Tail.Thorp.Specht.fiberGroup line 533
  63. lemma OAI.ThorpNine.Tail.Thorp.Specht.swap_mem_fiberGroup line 540
  64. lemma OAI.ThorpNine.Tail.Thorp.Specht.swap_polytabloid line 551
  65. theorem OAI.ThorpNine.Tail.Thorp.Specht.tall_column_average_zero line 558
  66. def OAI.ThorpNine.Tail.Thorp.Specht.rowEquiv line 582
  67. def OAI.ThorpNine.Tail.Thorp.Specht.rowCost line 592
  68. lemma OAI.ThorpNine.Tail.Thorp.Specht.eq_of_row_preserving line 594
  69. lemma OAI.ThorpNine.Tail.Thorp.Specht.column_injective_rowCost line 611
  70. lemma OAI.ThorpNine.Tail.Thorp.Specht.swap_relabel line 629
  71. lemma OAI.ThorpNine.Tail.Thorp.Specht.sign_vector_rowCost line 635
  72. lemma OAI.ThorpNine.Tail.Thorp.Specht.polytabloid_col_action line 660
  73. theorem OAI.ThorpNine.Tail.Thorp.Specht.shapes_eq_of_equivariant_equiv line 664
  74. def OAI.ThorpNine.Tail.Thorp.Specht.cellRowsEquiv line 705
  75. lemma OAI.ThorpNine.Tail.Thorp.Specht.card_eq_sum_rowLen line 712
  76. lemma OAI.ThorpNine.Tail.Thorp.Specht.sum_rowLens line 716
  77. def OAI.ThorpNine.Tail.Thorp.Specht.diagramPartition line 725
  78. def OAI.ThorpNine.Tail.Thorp.Specht.partitionDiagram line 730
  79. lemma OAI.ThorpNine.Tail.Thorp.Specht.partitionDiagram_rowLens line 733
  80. lemma OAI.ThorpNine.Tail.Thorp.Specht.partitionDiagram_card line 739
  81. lemma OAI.ThorpNine.Tail.Thorp.Specht.partitionDiagram_diagramPartition line 744
  82. abbrev OAI.ThorpNine.Tail.Thorp.Specht.Shapes line 753