OAI/Combinatorics/RamseyFive/Entropy/OrderedReciprocalLaw.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.FiniteEntropy.orderedLaw line 12
2. lemma OAI.SharpRamseyFive.FiniteEntropy.orderedLaw_marginal line 14
3. lemma OAI.SharpRamseyFive.FiniteEntropy.orderedLaw_pair line 18
4. lemma OAI.SharpRamseyFive.FiniteEntropy.orderedLaw_positive line 23
5. def OAI.SharpRamseyFive.Windows.slotEquiv line 31
6. lemma OAI.SharpRamseyFive.Windows.slotEquiv_apply line 33
7. def OAI.SharpRamseyFive.Marking.orderedCollision line 44
8. lemma OAI.SharpRamseyFive.Marking.orderedCollision_nonneg line 51
9. lemma OAI.SharpRamseyFive.Marking.orderedCollision_symm line 55
10. lemma OAI.SharpRamseyFive.Marking.orderedCollision_sum line 59
11. lemma OAI.SharpRamseyFive.Marking.ordered_reciprocal_low_conflict line 78
12. lemma OAI.SharpRamseyFive.Marking.ordered_closed_collision_budget line 103
13. lemma OAI.SharpRamseyFive.Marking.ordered_open_collision_zero line 130
14. lemma OAI.SharpRamseyFive.Marking.ordered_collision_subset line 141