OAI/Probability/ThorpShuffle/CosetBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Thorp.Fourier.coset_sum_reindex line 16
2. lemma OAI.Thorp.Fourier.weighted_coset_bound line 28
3. lemma OAI.Thorp.Fourier.Family.coset_coefficient_evaluation line 51
4. theorem OAI.Thorp.Fourier.Family.weighted_coefficient line 62
5. lemma OAI.Thorp.Fourier.norm_weighted_sum_sq line 97
6. theorem OAI.Thorp.Fourier.Family.split_weighted_coefficient line 115
7. theorem OAI.Thorp.Fourier.Family.integrated_norm_sq line 154