OAI/Combinatorics/RamseyFive/Entropy/OriginalMarginalLaw.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpRamseyFive.FiniteEntropy.originalLevelLaw_first_mean line 10
2. lemma OAI.SharpRamseyFive.FiniteEntropy.originalLevelLaw_second_mean line 17
3. lemma OAI.SharpRamseyFive.FiniteEntropy.relationMass_singleton_right line 24
4. lemma OAI.SharpRamseyFive.FiniteEntropy.relationMass_weighted_singleton line 29
5. lemma OAI.SharpRamseyFive.FiniteEntropy.relationMass_mixture_right line 34
6. lemma OAI.SharpRamseyFive.FiniteEntropy.originalLevelLaw_right_domination line 40
7. lemma OAI.SharpRamseyFive.FiniteEntropy.originalLevelLaw_left_domination line 54