OAI/Combinatorics/KMedianRecovery/Recovery/Removal.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.ValidExecution.phase_pos line 21
  2. lemma OAI.MetricKMedianRecovery.ValidExecution.opened_mono line 27
  3. lemma OAI.MetricKMedianRecovery.ValidExecution.phase_mono line 34
  4. lemma OAI.MetricKMedianRecovery.ValidExecution.active_antitone line 41
  5. lemma OAI.MetricKMedianRecovery.ValidExecution.inactive_persists line 47
  6. lemma OAI.MetricKMedianRecovery.ValidExecution.budget_frozen line 52
  7. lemma OAI.MetricKMedianRecovery.ValidExecution.initial_active line 61
  8. lemma OAI.MetricKMedianRecovery.ValidExecution.exists_removal line 67
  9. def OAI.MetricKMedianRecovery.ValidExecution.removal line 86
  10. lemma OAI.MetricKMedianRecovery.ValidExecution.removal_active line 89
  11. lemma OAI.MetricKMedianRecovery.ValidExecution.removal_inactive line 94
  12. lemma OAI.MetricKMedianRecovery.ValidExecution.active_iff_before_removal line 99
  13. lemma OAI.MetricKMedianRecovery.ValidExecution.final_cap line 110
  14. lemma OAI.MetricKMedianRecovery.ValidExecution.no_overbid line 116
  15. def OAI.MetricKMedianRecovery.CertifiedRegularStep line 138
  16. def OAI.MetricKMedianRecovery.clientSlack line 149
  17. def OAI.MetricKMedianRecovery.totalSlack line 153
  18. lemma OAI.MetricKMedianRecovery.activeAt_of_superset line 157
  19. lemma OAI.MetricKMedianRecovery.inactive_connection_le_phase line 162
  20. lemma OAI.MetricKMedianRecovery.regular_slack_gain line 170
  21. lemma OAI.MetricKMedianRecovery.regular_payment_gain line 228
  22. lemma OAI.MetricKMedianRecovery.AtomicStep.budget_mono line 248
  23. lemma OAI.MetricKMedianRecovery.AtomicStep.slack_mono line 256
  24. lemma OAI.MetricKMedianRecovery.AtomicStep.total_slack_mono line 280
  25. lemma OAI.MetricKMedianRecovery.ValidExecution.active_budget line 292
  26. lemma OAI.MetricKMedianRecovery.ValidExecution.total_slack_mono line 300
  27. lemma OAI.MetricKMedianRecovery.ValidExecution.regular_payment_gain line 305
  28. theorem OAI.MetricKMedianRecovery.valid_execution_payment line 317
  29. def OAI.MetricKMedianRecovery.dualRowTerm line 368
  30. lemma OAI.MetricKMedianRecovery.dualRowTerm_pair line 374