OAI/NumberTheory/Ostmann/Supply/ActualLogBudget.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Ostmann.Supply.actualLogBudgetline 13 - theorem
OAI.Ostmann.Supply.actualLogBudget_nonnegline 16 - theorem
OAI.Ostmann.Supply.eventually_actualLogBudget_leline 19