OAI/Combinatorics/RamseyFive/Marking/HighNumerics.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpRamseyFive.Marking.high_bad_uniform line 13
2. lemma OAI.SharpRamseyFive.Marking.high_four_variance line 35
3. lemma OAI.SharpRamseyFive.Marking.high_four_growth line 46
4. lemma OAI.SharpRamseyFive.Marking.high_four_conflict line 61
5. lemma OAI.SharpRamseyFive.Marking.highFourLoss_bound line 69
6. theorem OAI.SharpRamseyFive.Marking.eventually_high_four_loss line 84
7. lemma OAI.SharpRamseyFive.Marking.eventually_stage_scale line 128
8. lemma OAI.SharpRamseyFive.Marking.highBadMass_le_highFourLoss line 143
9. lemma OAI.SharpRamseyFive.Marking.high_small_geometry line 154
10. theorem OAI.SharpRamseyFive.Marking.eventually_high_geometry line 172