OAI/Probability/ThorpShuffle/PartitionBounds.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Thorp.Young.idealDiagram line 13
2. lemma OAI.Thorp.Young.mem_idealDiagram line 24
3. def OAI.Thorp.Young.idealCells line 34
4. lemma OAI.Thorp.Young.idealDiagram_extensions_le line 43
5. theorem OAI.Thorp.Young.exists_trimLower line 48
6. theorem OAI.Thorp.Young.choose_le_extensions line 89
7. lemma OAI.Thorp.Young.partition_count_le_pow line 102
8. lemma OAI.Thorp.Young.rectangle_card_le line 107
9. lemma OAI.Thorp.Young.cell_small_coord line 119
10. lemma OAI.Thorp.Young.rowLen_le_card line 128
11. lemma OAI.Thorp.Young.colLen_le_card line 132
12. theorem OAI.Thorp.Young.partition_count_le_sqrt_pow line 136
13. lemma OAI.Thorp.Young.pow_le_choose_mul line 177
14. lemma OAI.Thorp.Young.pow_le_choose_of_mul_le line 202
15. lemma OAI.Thorp.Young.sub_add_one_le_choose line 205