OAI/Probability/CubeShuffle/FourierBound.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CubeShuffle.Specht.cardLabels line 10

   Also declared: ComparatorChallenges/WeightedSweepMoments.lean:225 (same declaration text).

2. def OAI.CubeShuffle.Specht.cardRepresentation line 13

   Also declared: ComparatorChallenges/WeightedSweepMoments.lean:228 (same declaration text).

3. lemma OAI.CubeShuffle.Specht.cardRepresentation_unitary line 17
4. instance OAI.CubeShuffle.Specht.cardRepresentation_irreducible line 21
5. lemma OAI.CubeShuffle.Specht.relabelledUnitary_neq line 25
6. lemma OAI.CubeShuffle.Specht.cardRepresentation_distinct line 50
7. lemma OAI.CubeShuffle.Specht.card_conjugacy_shapes line 55
8. lemma OAI.CubeShuffle.Specht.row_zero_of_full_row line 60
9. lemma OAI.CubeShuffle.Specht.tabloid_subsingleton_of_full_row line 66
10. lemma OAI.CubeShuffle.Specht.representation_full_row line 77
11. lemma OAI.CubeShuffle.Specht.relabelled_full_row line 87
12. lemma OAI.CubeShuffle.UnitaryFinite.sample_uniform_left line 98
13. lemma OAI.CubeShuffle.UnitaryFinite.uniform_zero_of_sample_norm_lt_one line 102
14. lemma OAI.CubeShuffle.UnitaryFinite.sampleOperator_trivial line 110
15. lemma OAI.CubeShuffle.UnitaryFinite.uniformOperator_trivial line 122
16. lemma OAI.CubeShuffle.UnitaryFinite.weighted_sub line 127
17. lemma OAI.CubeShuffle.physical_palindrome_norm line 138
18. lemma OAI.CubeShuffle.physical_power_bound line 147