OAI/Combinatorics/KMedian/Geometry/RationalSplitEnumeration.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MetricKMedian.Preparation.RationalSplitting.sum_fiber_nonneg line 13
  2. theorem OAI.MetricKMedian.Preparation.RationalSplitting.sum_weight_nonneg line 28
  3. def OAI.MetricKMedian.Preparation.RationalSplitting.count line 34
  4. def OAI.MetricKMedian.Preparation.RationalSplitting.index line 36
  5. def OAI.MetricKMedian.Preparation.RationalSplitting.weights line 40
  6. def OAI.MetricKMedian.Preparation.RationalSplitting.original line 43
  7. def OAI.MetricKMedian.Preparation.RationalSplitting.assigned line 46
  8. theorem OAI.MetricKMedian.Preparation.RationalSplitting.count_le line 49
  9. theorem OAI.MetricKMedian.Preparation.RationalSplitting.mem_assigned line 56
  10. theorem OAI.MetricKMedian.Preparation.RationalSplitting.assigned_sum line 66
  11. theorem OAI.MetricKMedian.Preparation.RationalSplitting.weights_sum line 72