OAI/Combinatorics/RamseyFive/Geometry/TrainingLineCard.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SharpRamseyFive.ScoreGeometry.training_line_cardline 18 - theorem
OAI.SharpRamseyFive.ScoreGeometry.score_degree_uniform_normalizedline 32 - theorem
OAI.SharpRamseyFive.ScoreGeometry.score_row_uniform_momentline 69 - def
OAI.SharpRamseyFive.ScoreGeometry.highCertificateMajorantline 103 - lemma
OAI.SharpRamseyFive.ScoreGeometry.highCertificateMajorant_nonnegline 108 - theorem
OAI.SharpRamseyFive.ScoreGeometry.score_high_certificate_majorantline 119