OAI/Combinatorics/RamseyFive/Marking/Collisions.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpRamseyFive.FiniteEntropy.eventWeight_map line 12
2. def OAI.SharpRamseyFive.LowConflict.tupleMarginal line 26
3. def OAI.SharpRamseyFive.LowConflict.tupleCapture line 29
4. def OAI.SharpRamseyFive.LowConflict.tupleCollision line 35
5. lemma OAI.SharpRamseyFive.LowConflict.tupleCollision_nonneg line 40
6. lemma OAI.SharpRamseyFive.LowConflict.tuple_flag_marginal line 45
7. theorem OAI.SharpRamseyFive.LowConflict.tuple_low_conflict line 52
8. lemma OAI.SharpRamseyFive.LowConflict.tuple_collision_count line 78
9. theorem OAI.SharpRamseyFive.LowConflict.closed_tuple_collision_bound line 106
10. theorem OAI.SharpRamseyFive.LowConflict.high_tuple_collision_bound line 125
11. theorem OAI.SharpRamseyFive.LowConflict.open_tuple_collision_zero line 144