OAI/Combinatorics/RamseyFive/Entropy/MarkingNumerics.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpRamseyFive.Marking.point_log_one_add_card line 13
2. lemma OAI.SharpRamseyFive.Marking.expensiveBound_coarse line 27
3. theorem OAI.SharpRamseyFive.Marking.eventually_stream_cheap_entropy line 36