OAI/Probability/ThorpShuffle/Reynolds.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Thorp.Fourier.integrated line 19

   Also declared: ComparatorChallenges/ThorpFirstReciprocal.lean:41 (same declaration text).

2. def OAI.Thorp.Fourier.reynolds line 22
3. lemma OAI.Thorp.Fourier.reynolds_intertwines line 25
4. def OAI.Thorp.Fourier.reynoldsMap line 39
5. lemma OAI.Thorp.Fourier.reynolds_scalar line 43
6. lemma OAI.Thorp.Fourier.reynolds_zero line 52
7. lemma OAI.Thorp.Fourier.trace_reynolds line 59
8. lemma OAI.Thorp.Fourier.reynolds_eq_trace line 72
9. lemma OAI.Thorp.Fourier.inner_inv line 86
10. theorem OAI.Thorp.Fourier.coefficient_second_moment line 93
11. def OAI.Thorp.Fourier.convolution line 123
12. def OAI.Thorp.Fourier.delta line 125
13. lemma OAI.Thorp.Fourier.integrated_delta line 127
14. lemma OAI.Thorp.Fourier.integrated_sum line 130
15. lemma OAI.Thorp.Fourier.integrated_sub line 135
16. lemma OAI.Thorp.Fourier.integrated_convolution line 139
17. lemma OAI.Thorp.Fourier.integrated_central line 152
18. lemma OAI.Thorp.Fourier.central_scalar line 164
19. lemma OAI.Thorp.Fourier.trace_integrated line 175