OAI/Combinatorics/KMedian/Process/BatchGraphData.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.RationalBatchData.GraphData.transpose line 13
  2. def OAI.MetricKMedian.RationalBatchData.GraphData.masses line 14
  3. def OAI.MetricKMedian.RationalBatchData.GraphData.amount line 15
  4. def OAI.MetricKMedian.RationalBatchData.GraphData.heavy line 16
  5. abbrev OAI.MetricKMedian.RationalBatchData.GraphData.Raw line 17
  6. def OAI.MetricKMedian.RationalBatchData.GraphData.prepare line 18
  7. def OAI.MetricKMedian.RationalBatchData.GraphData.data line 21
  8. theorem OAI.MetricKMedian.RationalBatchData.GraphData.transpose_poly line 23
  9. theorem OAI.MetricKMedian.RationalBatchData.GraphData.masses_poly line 28
  10. theorem OAI.MetricKMedian.RationalBatchData.GraphData.amount_poly line 34
  11. theorem OAI.MetricKMedian.RationalBatchData.GraphData.heavy_poly line 38
  12. theorem OAI.MetricKMedian.RationalBatchData.GraphData.prepare_poly line 39
  13. theorem OAI.MetricKMedian.RationalBatchData.GraphData.data_poly line 40
  14. theorem OAI.MetricKMedian.RationalBatchData.GraphData.transpose_view line 42
  15. theorem OAI.MetricKMedian.RationalBatchData.GraphData.masses_view line 47
  16. theorem OAI.MetricKMedian.RationalBatchData.GraphData.amount_view line 51
  17. theorem OAI.MetricKMedian.RationalBatchData.GraphData.heavy_view line 53
  18. theorem OAI.MetricKMedian.RationalBatchData.GraphData.prepare_view line 56