OAI/Combinatorics/RamseyFive/Entropy/ChronologicalCapDomination.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpRamseyFive.FiniteEntropy.adaptive_event_first line 10
2. lemma OAI.SharpRamseyFive.FiniteEntropy.adaptive_event_second line 20
3. lemma OAI.SharpRamseyFive.FiniteEntropy.adaptive_event_second_le line 26
4. lemma OAI.SharpRamseyFive.ReverseCap.excludes_pure_none line 37
5. theorem OAI.SharpRamseyFive.ProjectiveIncidence.nextCapLaw_domination line 52
6. theorem OAI.SharpRamseyFive.ProjectiveIncidence.second_cap_unconditioned line 82