OAI/Combinatorics/KMedianRecovery/Recovery/BoundedMinimizingExtreme.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MetricKMedianRecovery.PolytopeCertificate.bounded_minimizing_extreme line 15
2. theorem OAI.MetricKMedianRecovery.PolytopeCertificate.integer_min_certificate line 56
3. abbrev OAI.MetricKMedianRecovery.PolytopeCertificate.SlackRow line 83
4. def OAI.MetricKMedianRecovery.PolytopeCertificate.slackMatrix line 85
5. def OAI.MetricKMedianRecovery.PolytopeCertificate.slackBounds line 90
6. lemma OAI.MetricKMedianRecovery.PolytopeCertificate.slack_region_iff line 96
7. lemma OAI.MetricKMedianRecovery.PolytopeCertificate.positive_fraction_gap line 145
8. theorem OAI.MetricKMedianRecovery.PolytopeCertificate.approximate_implies_feasible line 160