OAI/Combinatorics/KMedian/Process/BatchOrdinalArrays.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MetricKMedian.RationalBatchData.Ordinal.erase_code line 16
  2. theorem OAI.MetricKMedian.RationalBatchData.Ordinal.bal_code line 36
  3. theorem OAI.MetricKMedian.RationalBatchData.Ordinal.overlap_sets line 45
  4. theorem OAI.MetricKMedian.RationalBatchData.Ordinal.conflict_code line 49
  5. theorem OAI.MetricKMedian.RationalBatchData.Ordinal.bias_code line 59
  6. theorem OAI.MetricKMedian.RationalBatchData.Ordinal.data_view line 65
  7. def OAI.MetricKMedian.RationalBatchData.Ordinal.graphView line 99
  8. theorem OAI.MetricKMedian.RationalBatchData.Ordinal.transpose_graph line 100
  9. theorem OAI.MetricKMedian.RationalBatchData.Ordinal.masses_graph line 105
  10. theorem OAI.MetricKMedian.RationalBatchData.Ordinal.heavy_graph line 109
  11. theorem OAI.MetricKMedian.RationalBatchData.Ordinal.prepare_graph line 117