OAI/Combinatorics/SharpRamsey/Selection/DyadicGrid.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLogRamsey.DyadicGrid.value line 11
2. lemma OAI.SharpLogRamsey.DyadicGrid.value_pos line 13
3. lemma OAI.SharpLogRamsey.DyadicGrid.value_le_one line 14
4. lemma OAI.SharpLogRamsey.DyadicGrid.value_succ line 16
5. lemma OAI.SharpLogRamsey.DyadicGrid.covers line 19
6. lemma OAI.SharpLogRamsey.DyadicGrid.sum_le_two line 30
7. lemma OAI.SharpLogRamsey.DyadicGrid.sum_pow_le_two line 39
8. lemma OAI.SharpLogRamsey.DyadicGrid.value_log_le line 44
9. theorem OAI.SharpLogRamsey.DyadicGrid.integer_overlap_cover line 51