OAI/Combinatorics/RamseyFive/Entropy/IIDLowerTail.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpRamseyFive.FiniteEntropy.exp_neg_one_le_half line 10
2. lemma OAI.SharpRamseyFive.FiniteEntropy.expected_exp_neg_hit line 16
3. lemma OAI.SharpRamseyFive.FiniteEntropy.expected_exp_neg_hits line 28
4. lemma OAI.SharpRamseyFive.FiniteEntropy.expected_exp_neg_hits_le line 39
5. theorem OAI.SharpRamseyFive.FiniteEntropy.iid_low_hit_event line 55
6. theorem OAI.SharpRamseyFive.FiniteEntropy.iid_cap_tail line 67