OAI/Combinatorics/SharpRamsey/Construction/FiniteStreamTail.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLogRamsey.FiniteStreamTail.hits line 12
2. def OAI.SharpLogRamsey.FiniteStreamTail.probability line 15
3. lemma OAI.SharpLogRamsey.FiniteStreamTail.moment line 17
4. lemma OAI.SharpLogRamsey.FiniteStreamTail.card_pos line 34
5. lemma OAI.SharpLogRamsey.FiniteStreamTail.average_moment line 36
6. lemma OAI.SharpLogRamsey.FiniteStreamTail.average_moment_le line 44
7. lemma OAI.SharpLogRamsey.FiniteStreamTail.single_tail line 52
8. lemma OAI.SharpLogRamsey.FiniteStreamTail.probability_univ line 79
9. lemma OAI.SharpLogRamsey.FiniteStreamTail.probability_compl line 83
10. lemma OAI.SharpLogRamsey.FiniteStreamTail.hits_embedding line 88
11. theorem OAI.SharpLogRamsey.FiniteStreamTail.simultaneous_tail line 99