OAI/Combinatorics/KMedianRecovery/Recovery/ShortPrice.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.Surplus.short_price line 10
  2. lemma OAI.MetricKMedianRecovery.Surplus.anchoring_scale line 16
  3. lemma OAI.MetricKMedianRecovery.Surplus.small_bad_cost line 25
  4. lemma OAI.MetricKMedianRecovery.Surplus.small_bad_strict line 30
  5. lemma OAI.MetricKMedianRecovery.Surplus.bounded_mass line 35
  6. lemma OAI.MetricKMedianRecovery.Surplus.normal_strict line 57
  7. lemma OAI.MetricKMedianRecovery.Surplus.small_price_strict line 71
  8. lemma OAI.MetricKMedianRecovery.Surplus.aggregate_gain line 89
  9. theorem OAI.MetricKMedianRecovery.Surplus.low_sensitive_cost line 117