OAI/Combinatorics/KMedian/Rounding/RationalSignedStep.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.RationalSignedStep.pairs line 12
  2. def OAI.MetricKMedian.RationalSignedStep.Active line 16
  3. instance OAI.MetricKMedian.RationalSignedStep.(instance at line 17) line 17
  4. def OAI.MetricKMedian.RationalSignedStep.pair line 20
  5. theorem OAI.MetricKMedian.RationalSignedStep.pair_ratio_pos line 27
  6. theorem OAI.MetricKMedian.RationalSignedStep.pair_right_ne line 33
  7. theorem OAI.MetricKMedian.RationalSignedStep.inactive line 40
  8. def OAI.MetricKMedian.RationalSignedStep.probability line 48
  9. def OAI.MetricKMedian.RationalSignedStep.endpoint line 55
  10. theorem OAI.MetricKMedian.RationalSignedStep.probability_unit line 62
  11. theorem OAI.MetricKMedian.RationalSignedStep.endpoint_mean line 74
  12. theorem OAI.MetricKMedian.RationalSignedStep.endpoint_pair line 93
  13. theorem OAI.MetricKMedian.RationalSignedStep.endpoint_feasible line 115
  14. theorem OAI.MetricKMedian.RationalSignedStep.endpoint_smaller line 144
  15. theorem OAI.MetricKMedian.RationalSignedStep.endpoint_weighted line 163