OAI/Probability/SignedSweeps/BudgetBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SignedSweeps.clippedBudget line 10
2. lemma OAI.SignedSweeps.clippedBudget_zero line 13
3. lemma OAI.SignedSweeps.remainderBudget_eq_clippedBudget line 16
4. lemma OAI.SignedSweeps.clippedBudget_mono line 20
5. lemma OAI.SignedSweeps.clippedBudget_le_unclipped line 27
6. lemma OAI.SignedSweeps.line_budgets_le line 61
7. lemma OAI.SignedSweeps.clippedBudget_growth line 82