OAI/NumberTheory/ShortEgyptian/LevelSelection.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ShortEgyptian.scaleInterval line 12
2. lemma OAI.ShortEgyptian.scaleInterval_mem line 14
3. lemma OAI.ShortEgyptian.scaleInterval_card line 21
4. def OAI.ShortEgyptian.badLevel line 28
5. lemma OAI.ShortEgyptian.badLevel_of_moment line 31
6. lemma OAI.ShortEgyptian.expected_badLevel line 51
7. lemma OAI.ShortEgyptian.middle_interval_log line 67
8. lemma OAI.ShortEgyptian.random_middle_bad line 81
9. theorem OAI.ShortEgyptian.choose_random_lists line 101