OAI/Combinatorics/BalancedRyser/Local/LocalInjectionBudget.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Balanced.LocalAsymptotics.eventually_mul_ceil_log_leline 12 - theorem
OAI.Balanced.Local.exists_logBudget_token_thresholdline 31