OAI/Probability/ThorpShuffle/VectorOrbits.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Thorp.Specht.cyclic_scalar_mem line 19
2. lemma OAI.Thorp.Specht.cyclic_scalar_action line 33
3. lemma OAI.Thorp.Specht.cyclic_scalar_finrank line 41
4. lemma OAI.Thorp.Specht.PermutationSpace.translate_alternator line 51
5. lemma OAI.Thorp.Specht.row_zero_of_full line 66
6. lemma OAI.Thorp.Specht.col_zero_of_full line 74
7. lemma OAI.Thorp.Specht.row_rep_action line 84
8. lemma OAI.Thorp.Specht.column_poly_action line 95
9. lemma OAI.Thorp.Specht.exceptional_action line 105
10. lemma OAI.Thorp.Fourier.sum_rep_invariant line 140
11. lemma OAI.Thorp.Fourier.invariant_finrank_le_one line 147
12. lemma OAI.Thorp.Fourier.integrated_uniform_zero line 160
13. lemma OAI.Thorp.Fourier.integrated_scalar line 172
14. lemma OAI.Thorp.Fourier.hsSq_scalar line 179