OAI/Combinatorics/RamseyFive/Iteration/Scale.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.ScoreRegularity.scale line 15
2. def OAI.SharpRamseyFive.ScoreRegularity.familyCell line 17
3. def OAI.SharpRamseyFive.ScoreRegularity.deviation line 20
4. def OAI.SharpRamseyFive.ScoreRegularity.threshold line 25
5. def OAI.SharpRamseyFive.ScoreRegularity.exceptional line 27
6. lemma OAI.SharpRamseyFive.ScoreRegularity.scale_nonneg line 32
7. lemma OAI.SharpRamseyFive.ScoreRegularity.cell_variance_scale line 36
8. lemma OAI.SharpRamseyFive.ScoreRegularity.total_deviation_bound line 50
9. lemma OAI.SharpRamseyFive.ScoreRegularity.exceptional_card_bound line 73
10. lemma OAI.SharpRamseyFive.ScoreRegularity.exceptional_mass_bound line 102