OAI/Combinatorics/RamseyFive/Entropy/GoodRepresentative.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpRamseyFive.FiniteEntropy.good_pair_mass line 14
2. def OAI.SharpRamseyFive.FiniteEntropy.goodRepresentative line 43
3. lemma OAI.SharpRamseyFive.FiniteEntropy.goodRepresentative_first_cap line 46
4. lemma OAI.SharpRamseyFive.FiniteEntropy.goodRepresentative_second_cap line 61
5. lemma OAI.SharpRamseyFive.FiniteEntropy.relationMass_conditionOn_left line 76
6. lemma OAI.SharpRamseyFive.FiniteEntropy.forbidden_product_mass line 86
7. lemma OAI.SharpRamseyFive.FiniteEntropy.conditionOn_ge_on line 102
8. lemma OAI.SharpRamseyFive.FiniteEntropy.uniformWeight_eq_zero_of_not_mem line 108
9. lemma OAI.SharpRamseyFive.FiniteEntropy.supported_levels_conditioned_domination line 111
10. lemma OAI.SharpRamseyFive.FiniteEntropy.relationMass_conditioned_good line 129
11. theorem OAI.SharpRamseyFive.ProjectiveIncidence.good_endpoint_supports line 151