OAI/Combinatorics/KMedianRecovery/Recovery/ExecutionState.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MetricKMedianRecovery.phase_update_no_overbid line 8
2. structure OAI.MetricKMedianRecovery.ExecutionState line 44
3. def OAI.MetricKMedianRecovery.initialState line 49
4. def OAI.MetricKMedianRecovery.regularUpdate line 52
5. def OAI.MetricKMedianRecovery.freeUpdate line 61
6. def OAI.MetricKMedianRecovery.phaseUpdate line 67
7. inductive OAI.MetricKMedianRecovery.AtomicStep line 74
8. structure OAI.MetricKMedianRecovery.ValidExecution line 92
9. lemma OAI.MetricKMedianRecovery.AtomicStep.opened_subset line 110
10. lemma OAI.MetricKMedianRecovery.AtomicStep.phase_le line 113
11. lemma OAI.MetricKMedianRecovery.AtomicStep.positive_phase line 121
12. lemma OAI.MetricKMedianRecovery.AtomicStep.active_before line 124
13. lemma OAI.MetricKMedianRecovery.AtomicStep.inactive_frozen line 130
14. lemma OAI.MetricKMedianRecovery.AtomicStep.active_budget_cap line 134
15. lemma OAI.MetricKMedianRecovery.AtomicStep.active_budget_lower line 150
16. lemma OAI.MetricKMedianRecovery.AtomicStep.surviving_budget line 170
17. lemma OAI.MetricKMedianRecovery.AtomicStep.removal_connection_cap line 198
18. lemma OAI.MetricKMedianRecovery.AtomicStep.preserves_no_overbid line 216