OAI/Combinatorics/KMedianRecovery/Strictness/RegularDualWitness.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.final_dual_of_rows line 8
  2. lemma OAI.MetricKMedianRecovery.AtomicStep.preserves_connection_bound line 34
  3. structure OAI.MetricKMedianRecovery.RegularDualWitness line 56
  4. lemma OAI.MetricKMedianRecovery.AtomicStep.witness_cases line 67
  5. def OAI.MetricKMedianRecovery.ValidExecution.finalBudget line 84
  6. def OAI.MetricKMedianRecovery.ValidExecution.Contributor line 86
  7. def OAI.MetricKMedianRecovery.ValidExecution.precedes line 88
  8. lemma OAI.MetricKMedianRecovery.ValidExecution.precedes_asymm line 92
  9. lemma OAI.MetricKMedianRecovery.ValidExecution.finalBudget_at_removal line 100
  10. lemma OAI.MetricKMedianRecovery.ValidExecution.finalBudget_le_connection line 104
  11. def OAI.MetricKMedianRecovery.ValidExecution.RegularFreezesAt line 118
  12. lemma OAI.MetricKMedianRecovery.ValidExecution.freezing_removes_contributor line 122
  13. lemma OAI.MetricKMedianRecovery.dualRowTerm_le_bid line 150
  14. lemma OAI.MetricKMedianRecovery.sum_dualRow_le_bidRow line 175
  15. lemma OAI.MetricKMedianRecovery.ValidExecution.unfrozen_regular_budget line 197
  16. lemma OAI.MetricKMedianRecovery.ValidExecution.phase_removal_budget line 223
  17. lemma OAI.MetricKMedianRecovery.ValidExecution.removal_row line 233
  18. def OAI.MetricKMedianRecovery.lastRelation line 292
  19. lemma OAI.MetricKMedianRecovery.lastRelation_asymm line 295
  20. lemma OAI.MetricKMedianRecovery.ValidExecution.witness_active_removal line 309
  21. lemma OAI.MetricKMedianRecovery.ValidExecution.witness_active_budget line 322
  22. lemma OAI.MetricKMedianRecovery.ValidExecution.witness_inactive_budget line 333
  23. lemma OAI.MetricKMedianRecovery.ValidExecution.contributor_dual_bound line 344