OAI/Combinatorics/RamseyFive/Marking/ReciprocalLevelProducer.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpRamseyFive.FiniteEntropy.eventMass_complement line 13
2. lemma OAI.SharpRamseyFive.FiniteEntropy.entropy_swap line 18
3. lemma OAI.SharpRamseyFive.FiniteEntropy.support_swap_card line 21
4. lemma OAI.SharpRamseyFive.FiniteEntropy.relationMass_good_uniform line 26
5. def OAI.SharpRamseyFive.Marking.reciprocalBadMass line 47
6. theorem OAI.SharpRamseyFive.Marking.reciprocal_bad_endpoints line 50
7. structure OAI.SharpRamseyFive.Marking.ReciprocalLevels line 75
8. theorem OAI.SharpRamseyFive.Marking.reciprocal_levels_exist line 88
9. lemma OAI.SharpRamseyFive.Marking.ReciprocalLevels.first_size line 133
10. lemma OAI.SharpRamseyFive.Marking.ReciprocalLevels.second_size line 141
11. theorem OAI.SharpRamseyFive.Marking.reciprocal_levels_cross line 149
12. theorem OAI.SharpRamseyFive.Marking.ordered_level_sparsity line 183
13. theorem OAI.SharpRamseyFive.Marking.ordered_good_u_monotone line 197