OAI/Probability/ThorpShuffle/FourierBounds.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Thorp.Fourier.Family.reciprocalSum line 16
2. lemma OAI.Thorp.Fourier.Family.reciprocalSum_nonneg line 18
3. lemma OAI.Thorp.Fourier.Family.low_degree_sq line 21
4. def OAI.Thorp.Fourier.hsSq line 58
5. lemma OAI.Thorp.Fourier.hsSq_nonneg line 61
6. lemma OAI.Thorp.Fourier.hsSq_le line 64
7. lemma OAI.Thorp.Fourier.norm_integrated_sq line 71
8. lemma OAI.Thorp.Fourier.hsSq_integrated line 86
9. theorem OAI.Thorp.Fourier.Family.parseval line 104
10. lemma OAI.Thorp.Fourier.power_norm_sq line 135
11. lemma OAI.Thorp.Fourier.eight_degree_bound line 144
12. lemma OAI.Thorp.Fourier.Family.l1_sq_le_parseval line 158