OAI/Combinatorics/RamseyFive/Iteration/RestrictionScale.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SharpRamseyFive.ParameterHierarchy.dyadic_levels_leline 10 - lemma
OAI.SharpRamseyFive.ParameterHierarchy.root_density_scaleline 27 - theorem
OAI.SharpRamseyFive.ParameterHierarchy.eventually_restriction_overheadsline 45