OAI/Probability/ThorpShuffle/JointProjectors.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Thorp.Fourier.complex_cauchy line 15
2. theorem OAI.Thorp.Fourier.Family.coefficient_evaluation line 26
3. def OAI.Thorp.Fourier.Family.jointKernel line 50
4. lemma OAI.Thorp.Fourier.Family.jointKernel_sum line 52
5. lemma OAI.Thorp.Fourier.Family.jointKernel_convolution line 69
6. lemma OAI.Thorp.Fourier.Family.jointKernel_star line 86
7. def OAI.Thorp.Fourier.Family.jointProjector line 92
8. lemma OAI.Thorp.Fourier.Family.jointProjector_mul line 95
9. lemma OAI.Thorp.Fourier.Family.jointProjector_idempotent line 100
10. lemma OAI.Thorp.Fourier.Family.jointProjector_sum line 104
11. def OAI.Thorp.Fourier.Family.tensorList line 108
12. lemma OAI.Thorp.Fourier.Family.tensorList_character line 113
13. def OAI.Thorp.Fourier.Family.tensorFamily line 128
14. lemma OAI.Thorp.Fourier.Family.tensorFamily_character line 130
15. lemma OAI.Thorp.Fourier.Family.jointKernel_formula line 135
16. lemma OAI.Thorp.Fourier.Family.trace_jointProjector line 141
17. theorem OAI.Thorp.Fourier.Family.joint_degree_le line 153