OAI/Combinatorics/KMedian/Geometry/RationalFractionalInput.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MetricKMedian.Preparation.computedNearest_ordered line 14
  2. def OAI.MetricKMedian.Preparation.FractionalRefinement.y line 25
  3. theorem OAI.MetricKMedian.Preparation.FractionalRefinement.mass_one line 28
  4. def OAI.MetricKMedian.Preparation.FractionalRefinement.x line 34
  5. theorem OAI.MetricKMedian.Preparation.FractionalRefinement.x_spec line 37
  6. def OAI.MetricKMedian.Preparation.FractionalRefinement.count line 53
  7. def OAI.MetricKMedian.Preparation.FractionalRefinement.original line 56
  8. def OAI.MetricKMedian.Preparation.FractionalRefinement.unitInput line 59
  9. theorem OAI.MetricKMedian.Preparation.FractionalRefinement.input_mass line 66
  10. theorem OAI.MetricKMedian.Preparation.FractionalRefinement.input_cost line 73
  11. def OAI.MetricKMedian.Preparation.FractionalRefinement.realization line 82