OAI/Combinatorics/KMedianRecovery/Strictness/LinearPayment.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.OpenabilityLinearization.linearPayment line 9
2. lemma OAI.MetricKMedianRecovery.OpenabilityLinearization.near_bid_nonnegative line 17
3. lemma OAI.MetricKMedianRecovery.OpenabilityLinearization.payment_eq_linear line 26
4. def OAI.MetricKMedianRecovery.OpenabilityLinearization.dualTerm line 41
5. lemma OAI.MetricKMedianRecovery.OpenabilityLinearization.dual_eq line 47
6. def OAI.MetricKMedianRecovery.OpenabilityLinearization.Feasible line 55
7. theorem OAI.MetricKMedianRecovery.OpenabilityLinearization.openable_iff_linear_feasible line 63
8. lemma OAI.MetricKMedianRecovery.OpenabilityLinearization.variable_count line 86