OAI/Combinatorics/SharpRamsey/Marking/HighRankBudgets.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLogRamsey.ActualHighRank.rawRows line 12
2. def OAI.SharpLogRamsey.ActualHighRank.rawThreshold line 13
3. def OAI.SharpLogRamsey.ActualHighRank.richDensity line 14
4. def OAI.SharpLogRamsey.ActualHighRank.rawError line 15
5. lemma OAI.SharpLogRamsey.ActualHighRank.density_positive line 20
6. lemma OAI.SharpLogRamsey.ActualHighRank.density_small line 21
7. lemma OAI.SharpLogRamsey.ActualHighRank.density_scaled line 26
8. lemma OAI.SharpLogRamsey.ActualHighRank.rawError_le line 32
9. theorem OAI.SharpLogRamsey.ActualHighRank.eventual_budgets line 75