OAI/Combinatorics/RamseyFive/Geometry/LocalLines.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.GlobalRadial.localLines line 16
2. def OAI.SharpRamseyFive.GlobalRadial.badCenters line 20
3. lemma OAI.SharpRamseyFive.GlobalRadial.sum_localLines_le line 24
4. lemma OAI.SharpRamseyFive.GlobalRadial.badCenters_mass_le line 38
5. lemma OAI.SharpRamseyFive.GlobalRadial.exception_fraction line 51
6. theorem OAI.SharpRamseyFive.GlobalRadial.captured_exception_fraction line 75
7. lemma OAI.SharpRamseyFive.ScoreGeometry.outsideAt_filter_card line 110
8. lemma OAI.SharpRamseyFive.ScoreGeometry.richRadials_le_localLines line 132
9. theorem OAI.SharpRamseyFive.ScoreGeometry.score_pairs_off_radial_exception line 155