OAI/Probability/ThorpShuffle/ProductProjectors.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Thorp.Fourier.integrated_single_mul line 16
2. lemma OAI.Thorp.Fourier.Family.jointKernel_single line 41
3. lemma OAI.Thorp.Fourier.Family.jointKernel_split line 52
4. lemma OAI.Thorp.Fourier.Family.jointKernel_single_convolution line 56
5. lemma OAI.Thorp.Fourier.Family.projector_jointProjector line 69
6. lemma OAI.Thorp.Fourier.Family.low_fixes_joint line 77
7. lemma OAI.Thorp.Fourier.norm_sum_sq_of_orthogonal line 89
8. def OAI.Thorp.Fourier.Family.leastFactor line 105
9. lemma OAI.Thorp.Fourier.Family.leastFactor_le line 108
10. lemma OAI.Thorp.Fourier.Family.jointProjector_symmetric line 116
11. lemma OAI.Thorp.Fourier.Family.jointProjector_orthogonal line 121
12. def OAI.Thorp.Fourier.Family.splitVector line 130
13. lemma OAI.Thorp.Fourier.Family.splitVector_sum line 134
14. lemma OAI.Thorp.Fourier.Family.splitVector_orthogonal line 143
15. lemma OAI.Thorp.Fourier.Family.splitVector_sq_sum line 157
16. lemma OAI.Thorp.Fourier.Family.leastFactor_pow_le line 162
17. lemma OAI.Thorp.Fourier.Family.splitVector_low line 170