OAI/NumberTheory/ShortEgyptian/ListSelection.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ShortEgyptian.phaseAverage line 12
2. def OAI.ShortEgyptian.FourierBad line 16
3. lemma OAI.ShortEgyptian.frequency_bad_probability line 20
4. lemma OAI.ShortEgyptian.fourierBad_probability line 58
5. lemma OAI.ShortEgyptian.frequency_bad_sum line 74
6. lemma OAI.ShortEgyptian.phaseAverage_sample line 92
7. lemma OAI.ShortEgyptian.random_fourier_failure line 105
8. lemma OAI.ShortEgyptian.expect_eval_function line 142
9. lemma OAI.ShortEgyptian.simultaneous_finite_selection line 153
10. lemma OAI.ShortEgyptian.fourier_good_residues line 199