OAI/Combinatorics/KMedianRecovery/Strictness/IndexedPaymentCoeff.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.EffectiveOpenability.payment_coeff_bid line 8
2. lemma OAI.MetricKMedianRecovery.EffectiveOpenability.payment_coeff_slack line 24
3. lemma OAI.MetricKMedianRecovery.EffectiveOpenability.dual_coeff_bid line 31
4. lemma OAI.MetricKMedianRecovery.EffectiveOpenability.dual_coeff_slack line 34
5. def OAI.MetricKMedianRecovery.EffectiveOpenability.indexedPaymentCoeff line 40
6. def OAI.MetricKMedianRecovery.EffectiveOpenability.indexedDualCoeff line 45
7. lemma OAI.MetricKMedianRecovery.EffectiveOpenability.payment_coeff line 48
8. lemma OAI.MetricKMedianRecovery.EffectiveOpenability.dual_coeff line 54
9. def OAI.MetricKMedianRecovery.EffectiveOpenability.indexedCoeff line 60
10. lemma OAI.MetricKMedianRecovery.EffectiveOpenability.indexedCoeff_eq line 75