OAI/Combinatorics/KMedian/Rounding/MarginalRounding.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.MarginalRounding.fractional line 12
  2. theorem OAI.MetricKMedian.MarginalRounding.mem_fractional line 15
  3. theorem OAI.MetricKMedian.MarginalRounding.nonfractional_integral line 18
  4. theorem OAI.MetricKMedian.MarginalRounding.second_fractional line 25
  5. def OAI.MetricKMedian.MarginalRounding.adjust line 60
  6. theorem OAI.MetricKMedian.MarginalRounding.adjust_left line 64
  7. theorem OAI.MetricKMedian.MarginalRounding.adjust_right line 67
  8. theorem OAI.MetricKMedian.MarginalRounding.adjust_other line 70
  9. theorem OAI.MetricKMedian.MarginalRounding.adjust_sum line 73
  10. def OAI.MetricKMedian.MarginalRounding.up line 78
  11. def OAI.MetricKMedian.MarginalRounding.down line 79
  12. theorem OAI.MetricKMedian.MarginalRounding.up_pos line 82
  13. theorem OAI.MetricKMedian.MarginalRounding.down_pos line 86
  14. theorem OAI.MetricKMedian.MarginalRounding.adjust_bounds line 91
  15. theorem OAI.MetricKMedian.MarginalRounding.fractional_adjust_subset line 110
  16. theorem OAI.MetricKMedian.MarginalRounding.up_smaller line 120
  17. theorem OAI.MetricKMedian.MarginalRounding.down_smaller line 137
  18. theorem OAI.MetricKMedian.MarginalRounding.exists_law line 154