OAI/NumberTheory/ShortEgyptian/DeterministicLists.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ShortEgyptian.nat_dist_one line 12
2. lemma OAI.ShortEgyptian.deterministic_list_moment line 23
3. lemma OAI.ShortEgyptian.deterministic_moment_scalar line 56
4. lemma OAI.ShortEgyptian.deterministic_cutoff_lower line 75
5. lemma OAI.ShortEgyptian.deterministic_T_scale line 86
6. lemma OAI.ShortEgyptian.deterministic_phase_bounds line 103
7. lemma OAI.ShortEgyptian.high_list_moment line 129