OAI/Combinatorics/RamseyFive/Entropy/FiniteGrowth.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.FiniteEntropy.runSamples line 12
2. def OAI.SharpRamseyFive.FiniteEntropy.failedGrowth line 16
3. def OAI.SharpRamseyFive.FiniteEntropy.growthFailures line 19
4. lemma OAI.SharpRamseyFive.FiniteEntropy.runSamples_cons line 24
5. lemma OAI.SharpRamseyFive.FiniteEntropy.growthFailures_cons line 28
6. lemma OAI.SharpRamseyFive.FiniteEntropy.runSamples_rank_mono line 34
7. lemma OAI.SharpRamseyFive.FiniteEntropy.zero_growthFailures line 41
8. theorem OAI.SharpRamseyFive.FiniteEntropy.growthFailures_mean line 63
9. theorem OAI.SharpRamseyFive.FiniteEntropy.iid_growth_failure line 94
10. lemma OAI.SharpRamseyFive.FiniteEntropy.firstAccepted_none_iff line 115
11. lemma OAI.SharpRamseyFive.FiniteEntropy.iid_avoidance line 134
12. lemma OAI.SharpRamseyFive.FiniteEntropy.eventWeight_mono line 142
13. lemma OAI.SharpRamseyFive.FiniteEntropy.eventWeight_union line 151