OAI/Combinatorics/KMedianRecovery/Algorithms/FinalBudgetPos.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.HistoryCompatibleCertificate.final_budget_pos line 12
2. theorem OAI.MetricKMedianRecovery.HistoryCompatibleCertificate.compatible_certificate line 20
3. def OAI.MetricKMedianRecovery.PhaseMergeCertificate.Budget line 60
4. lemma OAI.MetricKMedianRecovery.PhaseMergeCertificate.certify line 71
5. def OAI.MetricKMedianRecovery.PhaseMergeCertificate.Output line 82
6. def OAI.MetricKMedianRecovery.PhaseMergeCertificate.EnlargedOutput line 91
7. lemma OAI.MetricKMedianRecovery.PhaseMergeCertificate.solved_output line 99
8. theorem OAI.MetricKMedianRecovery.PhaseMergeCertificate.produce line 122