OAI/Combinatorics/KMedian/Rounding/RationalBatchData.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.RationalBatchData.graph line 12
  2. theorem OAI.MetricKMedian.RationalBatchData.graph_eq line 17
  3. def OAI.MetricKMedian.RationalBatchData.heavy line 19
  4. theorem OAI.MetricKMedian.RationalBatchData.heavy_eq line 24
  5. def OAI.MetricKMedian.RationalBatchData.balanced line 26
  6. def OAI.MetricKMedian.RationalBatchData.conflicts line 29
  7. theorem OAI.MetricKMedian.RationalBatchData.balanced_eq line 34
  8. def OAI.MetricKMedian.RationalBatchData.amount line 36
  9. def OAI.MetricKMedian.RationalBatchData.bias line 38
  10. def OAI.MetricKMedian.RationalBatchData.heavySet line 40
  11. def OAI.MetricKMedian.RationalBatchData.graphMass line 43
  12. theorem OAI.MetricKMedian.RationalBatchData.cast_amount line 46
  13. theorem OAI.MetricKMedian.RationalBatchData.cast_bias line 50
  14. theorem OAI.MetricKMedian.RationalBatchData.cast_graphMass line 56
  15. theorem OAI.MetricKMedian.RationalBatchData.heavySet_eq line 61