OAI/Probability/ThorpRouting/Harmonic/ModifiedReverseCoins.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ThorpNine.Harmonic.Thorp.modifiedReverseCoins line 10
2. lemma OAI.ThorpNine.Harmonic.Thorp.modifiedReverseCoins_involutive line 18
3. def OAI.ThorpNine.Harmonic.Thorp.modifiedReverseEquiv line 34
4. lemma OAI.ThorpNine.Harmonic.Thorp.modifiedPerm_reverse line 40
5. lemma OAI.ThorpNine.Harmonic.Thorp.modified_kernel_symmetric line 61
6. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.card_cell line 73

   Also declared: ComparatorChallenges/CoordinateTrace.lean:252 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:329 (same declaration text).

7. def OAI.ThorpNine.Harmonic.Thorp.Specht.columnEquiv line 76
8. def OAI.ThorpNine.Harmonic.Thorp.Specht.columnValues line 83
9. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.mem_columnValues line 86
10. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.card_columnValues line 91
11. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.strictMono_fin_nat_ge line 101
12. def OAI.ThorpNine.Harmonic.Thorp.Specht.rankCell line 115
13. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.rankCell_col line 121
14. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.rankCell_orderEmb line 125
15. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.rankCell_injective line 134
16. def OAI.ThorpNine.Harmonic.Thorp.Specht.rankPerm line 148
17. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.rankCell_row_le line 152
18. theorem OAI.ThorpNine.Harmonic.Thorp.Specht.column_transporter line 158
19. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.tabloidAct_inv line 171
20. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.tabloidRep_apply line 176
21. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.tabloidRep_delta line 179
22. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.mem_colGroup line 187
23. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.colGroup_row_stabilizer line 190
24. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.tabloid_column_transporter line 199
25. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.permSign_one line 217
26. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.permSign_mul line 219
27. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.permSign_inv line 221
28. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.permSign_sq line 223
29. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.permSign_swap line 228
30. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.conj_permSign line 230
31. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.alternator_mul line 235
32. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.mul_alternator line 250
33. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.alternator_apply_action line 265
34. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.action_alternator_apply line 270
35. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.alternator_eq_zero_of_odd_stabilizer line 275
36. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.swap_mem_colGroup line 291
37. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.swap_fixes_tabloid line 301
38. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.alternator_delta_rank_one line 313
39. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.polytabloid_formula line 329
40. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.polytabloid_base line 335
41. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.polytabloid_ne_zero line 348
42. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.delta_decomposition line 353
43. theorem OAI.ThorpNine.Harmonic.Thorp.Specht.alternator_rank_one line 360
44. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.alternator_rank_one_exact line 368
45. def OAI.ThorpNine.Harmonic.Thorp.Specht.pairing line 376
46. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.pairing_delta line 379
47. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.pairing_sum_left line 384
48. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.pairing_smul_left line 390
49. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.pairing_zero_left line 397
50. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.pairing_add_left line 400
51. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.pairing_self_eq_zero line 404
52. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.pairing_action line 412
53. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.alternator_base_pairing line 423
54. theorem OAI.ThorpNine.Harmonic.Thorp.Specht.alternator_pairing line 433
55. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.polytabloid_mem_space line 438
56. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.alternator_mem_invariant line 441
57. theorem OAI.ThorpNine.Harmonic.Thorp.Specht.submodule_theorem line 448
58. theorem OAI.ThorpNine.Harmonic.Thorp.Specht.space_simple line 479
59. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.space_ne_bot line 490
60. theorem OAI.ThorpNine.Harmonic.Thorp.Specht.representation_irreducible line 496
61. def OAI.ThorpNine.Harmonic.Thorp.Specht.symmetrizer line 535
62. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.symmetrizer_mul line 539
63. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.symmetrizer_eq_zero_of_neg line 545
64. def OAI.ThorpNine.Harmonic.Thorp.Specht.fiberGroup line 557
65. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.swap_mem_fiberGroup line 564
66. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.swap_polytabloid line 575
67. theorem OAI.ThorpNine.Harmonic.Thorp.Specht.tall_column_average_zero line 582
68. def OAI.ThorpNine.Harmonic.Thorp.Specht.rowEquiv line 606
69. def OAI.ThorpNine.Harmonic.Thorp.Specht.rowCost line 616
70. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.eq_of_row_preserving line 618
71. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.column_injective_rowCost line 635
72. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.swap_relabel line 653
73. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.sign_vector_rowCost line 659
74. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.polytabloid_col_action line 684
75. theorem OAI.ThorpNine.Harmonic.Thorp.Specht.shapes_eq_of_equivariant_equiv line 688
76. def OAI.ThorpNine.Harmonic.Thorp.Specht.cellRowsEquiv line 729

    Also declared: ComparatorChallenges/CoordinateTrace.lean:255 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:332 (same declaration text).

77. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.card_eq_sum_rowLen line 736

    Also declared: ComparatorChallenges/CoordinateTrace.lean:262 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:339 (same declaration text).

78. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.sum_rowLens line 740

    Also declared: ComparatorChallenges/CoordinateTrace.lean:266 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:343 (same declaration text).

79. def OAI.ThorpNine.Harmonic.Thorp.Specht.diagramPartition line 749

    Also declared: ComparatorChallenges/CoordinateTrace.lean:275 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:352 (same declaration text).

80. def OAI.ThorpNine.Harmonic.Thorp.Specht.partitionDiagram line 754

    Also declared: ComparatorChallenges/CoordinateTrace.lean:280 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:357 (same declaration text).