OAI/Combinatorics/RamseyFive/Geometry/OutsidePairCard.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpRamseyFive.ScoreGeometry.outside_pair_card_le line 20
2. lemma OAI.SharpRamseyFive.ScoreGeometry.score_pairs_le_captured line 33
3. theorem OAI.SharpRamseyFive.ScoreGeometry.score_high_captured_pairs line 60
4. lemma OAI.SharpRamseyFive.ScoreGeometry.score_pairs_le_residual line 89
5. lemma OAI.SharpRamseyFive.ScoreGeometry.pair_tail_training_mono line 118
6. lemma OAI.SharpRamseyFive.ScoreGeometry.outsideAt_antitone line 132
7. theorem OAI.SharpRamseyFive.ScoreGeometry.score_high_captured_pairs_of_le line 138
8. theorem OAI.SharpRamseyFive.ScoreGeometry.score_high_residual_pairs line 158
9. lemma OAI.SharpRamseyFive.ScoreGeometry.high_threshold_scale line 179