OAI/Combinatorics/SharpRamsey/Construction/RectangleStreamEvent.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLogRamsey.RectangleStreamEvent.rectangle line 17
2. lemma OAI.SharpLogRamsey.RectangleStreamEvent.rectangle_card line 20
3. lemma OAI.SharpLogRamsey.RectangleStreamEvent.flags_card_pos line 26
4. lemma OAI.SharpLogRamsey.RectangleStreamEvent.rectangle_probability line 32
5. lemma OAI.SharpLogRamsey.RectangleStreamEvent.rectangle_mean line 50
6. lemma OAI.SharpLogRamsey.RectangleStreamEvent.union_exponent line 62
7. theorem OAI.SharpLogRamsey.RectangleStreamEvent.simultaneous_rectangle_tail line 73
8. theorem OAI.SharpLogRamsey.RectangleStreamEvent.source_length_tail line 94
9. lemma OAI.SharpLogRamsey.RectangleStreamEvent.dual_rectangle line 107
10. lemma OAI.SharpLogRamsey.RectangleStreamEvent.inherited_occupancy line 112
11. theorem OAI.SharpLogRamsey.RectangleStreamEvent.simultaneous_good_probability line 118
12. theorem OAI.SharpLogRamsey.RectangleStreamEvent.source_good_probability line 140