OAI/Combinatorics/RamseyFive/Entropy/HighBudgetPoly.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SharpRamseyFive.ScoreGeometry.highBudgetPolyline 10 - lemma
OAI.SharpRamseyFive.ScoreGeometry.highMomentBudget_normalizedline 14 - lemma
OAI.SharpRamseyFive.ScoreGeometry.highMomentBudget_le_polyline 25