OAI/Combinatorics/RamseyFive/Entropy/LevelTreeTrims.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpRamseyFive.FiniteEntropy.relationMass_swap line 11
2. theorem OAI.SharpRamseyFive.ProjectiveIncidence.oriented_level_point_trim line 34
3. theorem OAI.SharpRamseyFive.ProjectiveIncidence.oriented_level_dual_trim line 85
4. lemma OAI.SharpRamseyFive.FiniteEntropy.independent_event line 143
5. lemma OAI.SharpRamseyFive.FiniteEntropy.independent_endpoint_event line 150
6. lemma OAI.SharpRamseyFive.FiniteEntropy.relationMass_mixture_left line 173
7. theorem OAI.SharpRamseyFive.FiniteEntropy.actual_target_average line 186