OAI/Combinatorics/KMedianRecovery/Strictness/StrictnessGap.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.strictnessGap line 7
  2. def OAI.MetricKMedianRecovery.SuffixConstraints line 10
  3. def OAI.MetricKMedianRecovery.prefixMass line 18
  4. def OAI.MetricKMedianRecovery.slack line 21
  5. def OAI.MetricKMedianRecovery.linearRow line 24
  6. lemma OAI.MetricKMedianRecovery.sum_linearRow line 27
  7. lemma OAI.MetricKMedianRecovery.suffix_row_bound line 38
  8. lemma OAI.MetricKMedianRecovery.slack_envelope line 50
  9. lemma OAI.MetricKMedianRecovery.slack_nonneg line 70
  10. lemma OAI.MetricKMedianRecovery.slack_truncation line 76
  11. lemma OAI.MetricKMedianRecovery.sum_prefixMass line 102
  12. lemma OAI.MetricKMedianRecovery.sum_slack line 114
  13. lemma OAI.MetricKMedianRecovery.subset_mass_bound line 131
  14. lemma OAI.MetricKMedianRecovery.prefix_le_mass line 149
  15. lemma OAI.MetricKMedianRecovery.one_sub_prefix_le_mass line 154
  16. theorem OAI.MetricKMedianRecovery.suffix_strictness line 173
  17. lemma OAI.MetricKMedianRecovery.positivePart_div line 332
  18. theorem OAI.MetricKMedianRecovery.scaled_suffix_strictness line 339
  19. theorem OAI.MetricKMedianRecovery.suffix_final_budget_bound line 370