OAI/Combinatorics/KMedian/Rounding/RationalWeightedStep.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.RationalWeightedStep.point line 12
  2. def OAI.MetricKMedian.RationalWeightedStep.realPoint line 13
  3. def OAI.MetricKMedian.RationalWeightedStep.fractional line 14
  4. def OAI.MetricKMedian.RationalWeightedStep.pair line 17
  5. def OAI.MetricKMedian.RationalWeightedStep.move line 31
  6. def OAI.MetricKMedian.RationalWeightedStep.up line 34
  7. def OAI.MetricKMedian.RationalWeightedStep.down line 35
  8. theorem OAI.MetricKMedian.RationalWeightedStep.real_move line 37
  9. theorem OAI.MetricKMedian.RationalWeightedStep.real_up line 44
  10. theorem OAI.MetricKMedian.RationalWeightedStep.real_down line 48
  11. theorem OAI.MetricKMedian.RationalWeightedStep.real_fractional line 52
  12. theorem OAI.MetricKMedian.RationalWeightedStep.up_pos line 59
  13. theorem OAI.MetricKMedian.RationalWeightedStep.down_pos line 64
  14. def OAI.MetricKMedian.RationalWeightedStep.probability line 69
  15. def OAI.MetricKMedian.RationalWeightedStep.endpoint line 76
  16. theorem OAI.MetricKMedian.RationalWeightedStep.probability_unit line 83
  17. theorem OAI.MetricKMedian.RationalWeightedStep.endpoint_mean line 95