OAI/Combinatorics/RamseyFive/Entropy/FinalMarking.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.SharpRamseyFive.Marking.final_marking_entropyline 18 - theorem
OAI.SharpRamseyFive.Marking.final_marking_entropy_on_supportline 43 - lemma
OAI.SharpRamseyFive.SelectedTuple.CodedStream.final_entropy_boundline 82 - theorem
OAI.SharpRamseyFive.SelectedTuple.eventually_stream_entropy_gainline 113