OAI/Combinatorics/RamseyFive/Entropy/WindowTargetInputs.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SharpRamseyFive.FiniteEntropy.map_first_valueline 11 - lemma
OAI.SharpRamseyFive.FiniteEntropy.map_second_valueline 14 - lemma
OAI.SharpRamseyFive.FiniteEntropy.eventMass_bad_mapline 17 - theorem
OAI.SharpRamseyFive.Marking.window_bad_targetline 36