OAI/Probability/ThorpShuffle/FourierFamilies.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Thorp.Fourier.Family line 15
2. def OAI.Thorp.Fourier.Family.degree line 35
3. lemma OAI.Thorp.Fourier.Family.orthogonal line 37
4. lemma OAI.Thorp.Fourier.Family.integrated_faithful line 46
5. lemma OAI.Thorp.Fourier.Family.integrated_injective line 65
6. def OAI.Thorp.Fourier.Family.kernel line 71
7. lemma OAI.Thorp.Fourier.Family.kernel_central line 74
8. lemma OAI.Thorp.Fourier.Family.integrated_kernel line 78
9. lemma OAI.Thorp.Fourier.Family.kernel_convolution line 100
10. lemma OAI.Thorp.Fourier.Family.kernel_sum line 115
11. lemma OAI.Thorp.Fourier.character_inv line 130
12. lemma OAI.Thorp.Fourier.integrated_symmetric line 138
13. lemma OAI.Thorp.Fourier.Family.kernel_star line 154
14. def OAI.Thorp.Fourier.Family.projector line 159
15. lemma OAI.Thorp.Fourier.Family.projector_mul line 161
16. lemma OAI.Thorp.Fourier.Family.projector_idempotent line 166
17. lemma OAI.Thorp.Fourier.Family.projector_sum line 170
18. lemma OAI.Thorp.Fourier.Family.projector_commute line 174
19. lemma OAI.Thorp.Fourier.Family.projector_symmetric line 178
20. lemma OAI.Thorp.Fourier.Family.kernel_sum_sq line 182