OAI/Combinatorics/RamseyFive/Entropy/SubsetMixture.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.FiniteEntropy.uniformWeight line 12
2. def OAI.SharpRamseyFive.FiniteEntropy.relationMass line 14
3. lemma OAI.SharpRamseyFive.FiniteEntropy.uniformWeight_nonneg line 18
4. lemma OAI.SharpRamseyFive.FiniteEntropy.relationMass_nonneg line 20
5. lemma OAI.SharpRamseyFive.FiniteEntropy.relationMass_uniform line 24
6. lemma OAI.SharpRamseyFive.FiniteEntropy.independent_subset_relation line 40
7. theorem OAI.SharpRamseyFive.FiniteEntropy.independent_subset_domination line 65
8. lemma OAI.SharpRamseyFive.FiniteEntropy.independent_law_lower line 82
9. lemma OAI.SharpRamseyFive.FiniteEntropy.relationMass_by_target line 101
10. lemma OAI.SharpRamseyFive.FiniteEntropy.sum_uniformWeight line 113
11. lemma OAI.SharpRamseyFive.FiniteEntropy.relationMass_neighbors line 121
12. lemma OAI.SharpRamseyFive.FiniteEntropy.independent_support_relation line 127
13. lemma OAI.SharpRamseyFive.FiniteEntropy.independent_support_domination line 153
14. theorem OAI.SharpRamseyFive.FiniteEntropy.adaptive_rejection_average line 169