OAI/Probability/ThorpShuffle/PermutationCharacters.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Thorp.Specht.degree_gt_one line 16
2. lemma OAI.Thorp.Specht.full_reciprocal_bound line 28
3. lemma OAI.Thorp.Specht.exceptional_count line 48
4. def OAI.Thorp.Specht.permutationFamily line 58
5. lemma OAI.Thorp.Specht.complexSign_permCongr line 61
6. lemma OAI.Thorp.Specht.complexSign_norm line 65
7. lemma OAI.Thorp.Specht.complexSign_eq line 68
8. lemma OAI.Thorp.Specht.complexSign_sum line 73
9. lemma OAI.Thorp.Specht.permutation_exceptional_action line 80
10. def OAI.Thorp.Fourier.realConv line 97
11. def OAI.Thorp.Fourier.realPower line 99
12. lemma OAI.Thorp.Fourier.realConv_nonneg line 103
13. lemma OAI.Thorp.Fourier.realConv_sum line 106
14. lemma OAI.Thorp.Fourier.realPower_nonneg line 115
15. lemma OAI.Thorp.Fourier.realPower_sum line 120
16. lemma OAI.Thorp.Fourier.integrated_realConv line 127
17. lemma OAI.Thorp.Fourier.integrated_realPower line 135
18. lemma OAI.Thorp.Fourier.integrated_real_sub line 144