OAI/Combinatorics/KMedian/Rounding/WeightedRounding.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.WeightedRounding.sign line 15
  2. def OAI.MetricKMedian.WeightedRounding.move line 17
  3. def OAI.MetricKMedian.WeightedRounding.up line 19
  4. def OAI.MetricKMedian.WeightedRounding.down line 20
  5. theorem OAI.MetricKMedian.WeightedRounding.sign_distinct line 23
  6. theorem OAI.MetricKMedian.WeightedRounding.move_left line 29
  7. theorem OAI.MetricKMedian.WeightedRounding.move_right line 32
  8. theorem OAI.MetricKMedian.WeightedRounding.move_other line 35
  9. theorem OAI.MetricKMedian.WeightedRounding.up_pos line 39
  10. theorem OAI.MetricKMedian.WeightedRounding.down_pos line 44
  11. theorem OAI.MetricKMedian.WeightedRounding.move_bounds line 50
  12. theorem OAI.MetricKMedian.WeightedRounding.fractional_subset line 74
  13. theorem OAI.MetricKMedian.WeightedRounding.up_smaller line 84
  14. theorem OAI.MetricKMedian.WeightedRounding.down_smaller line 102
  15. theorem OAI.MetricKMedian.WeightedRounding.weighted_sum line 120
  16. theorem OAI.MetricKMedian.WeightedRounding.endpoint_mean line 129
  17. theorem OAI.MetricKMedian.WeightedRounding.endpoint_pair line 137
  18. def OAI.MetricKMedian.WeightedRounding.indicator line 152
  19. theorem OAI.MetricKMedian.WeightedRounding.last_fraction line 154
  20. theorem OAI.MetricKMedian.WeightedRounding.exists_law line 216