OAI/Combinatorics/RamseyFive/Entropy/GoodEndpoints.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SharpRamseyFive.FiniteEntropy.scaled_heavy_atom_mass line 11
2. lemma OAI.SharpRamseyFive.FiniteEntropy.small_atom_mass line 59
3. def OAI.SharpRamseyFive.FiniteEntropy.heavyRow line 80
4. def OAI.SharpRamseyFive.FiniteEntropy.goodFirstEndpoints line 83
5. lemma OAI.SharpRamseyFive.FiniteEntropy.weighted_heavy_rows line 87
6. lemma OAI.SharpRamseyFive.FiniteEntropy.bad_conditional_row_mass line 97
7. theorem OAI.SharpRamseyFive.FiniteEntropy.bad_first_endpoint_mass line 112
8. lemma OAI.SharpRamseyFive.FiniteEntropy.goodFirst_positive line 144
9. lemma OAI.SharpRamseyFive.FiniteEntropy.goodFirst_conditional_cap line 148