OAI/Analysis/MatrixSigning/Matrices/PivotReachableBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W23.PivotReachableBounds.stepTicks line 14
2. def OAI.KS.W23.PivotReachableBounds.stepCoefficient line 17
3. def OAI.KS.W23.PivotReachableBounds.stepBudget line 19
4. theorem OAI.KS.W23.PivotReachableBounds.stepBudget_mono line 21
5. theorem OAI.KS.W23.PivotReachableBounds.step_payload_bound line 24
6. theorem OAI.KS.W23.PivotReachableBounds.reachable_step_bound line 37
7. theorem OAI.KS.W23.PivotReachableBounds.original_tape_bound_monomial line 45
8. def OAI.KS.W23.PivotReachableBounds.originalStepCoefficient line 57
9. theorem OAI.KS.W23.PivotReachableBounds.reachable_step_original_payload line 59
10. theorem OAI.KS.W23.PivotReachableBounds.controller_descent_step_bound line 80