OAI/Combinatorics/KMedianRecovery/Recovery/Region.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.PolytopeCertificate.region line 11
2. lemma OAI.MetricKMedianRecovery.PolytopeCertificate.row_perturb line 15
3. theorem OAI.MetricKMedianRecovery.PolytopeCertificate.active_kernel_zero line 23
4. lemma OAI.MetricKMedianRecovery.PolytopeCertificate.region_closed line 54
5. theorem OAI.MetricKMedianRecovery.PolytopeCertificate.bounded_extreme line 63
6. lemma OAI.MetricKMedianRecovery.PolytopeCertificate.gram_det_ne_zero line 75
7. lemma OAI.MetricKMedianRecovery.PolytopeCertificate.abs_det_le line 97
8. lemma OAI.MetricKMedianRecovery.PolytopeCertificate.int_det_cast line 113
9. theorem OAI.MetricKMedianRecovery.PolytopeCertificate.integer_point_certificate line 117