OAI/Combinatorics/KMedian/Programs/CardinalRoundProgram.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.SparseCardinalRounding.Program.Input line 13
  2. abbrev OAI.MetricKMedian.SparseCardinalRounding.Program.encodeInput line 14
  3. abbrev OAI.MetricKMedian.SparseCardinalRounding.Program.qr line 15
  4. abbrev OAI.MetricKMedian.SparseCardinalRounding.Program.br line 16
  5. def OAI.MetricKMedian.SparseCardinalRounding.Program.weightedInput line 18
  6. def OAI.MetricKMedian.SparseCardinalRounding.Program.result line 21
  7. def OAI.MetricKMedian.SparseCardinalRounding.Program.inputProgram line 24
  8. def OAI.MetricKMedian.SparseCardinalRounding.Program.selectedRow line 33
  9. theorem OAI.MetricKMedian.SparseCardinalRounding.Program.selectedRow_poly line 34
  10. theorem OAI.MetricKMedian.SparseCardinalRounding.Program.selectedRow_eq line 37
  11. def OAI.MetricKMedian.SparseCardinalRounding.Program.program line 46