OAI/Combinatorics/KMedian/Programs/StarActivationProgram.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MetricKMedian.SparseStarActivation.Program.Input line 14
  2. abbrev OAI.MetricKMedian.SparseStarActivation.Program.Raw line 20
  3. def OAI.MetricKMedian.SparseStarActivation.Program.Input.raw line 21
  4. abbrev OAI.MetricKMedian.SparseStarActivation.Program.Input.encode line 23
  5. def OAI.MetricKMedian.SparseStarActivation.Program.Input.column line 25
  6. def OAI.MetricKMedian.SparseStarActivation.Program.Input.columns line 27
  7. def OAI.MetricKMedian.SparseStarActivation.Program.prepare line 29
  8. theorem OAI.MetricKMedian.SparseStarActivation.Program.prepare_poly line 31
  9. theorem OAI.MetricKMedian.SparseStarActivation.Program.prepare_input line 32
  10. def OAI.MetricKMedian.SparseStarActivation.Program.columnsProgram line 36
  11. def OAI.MetricKMedian.SparseStarActivation.Program.dummy line 41
  12. def OAI.MetricKMedian.SparseStarActivation.Program.Input.graph line 42
  13. def OAI.MetricKMedian.SparseStarActivation.Program.graphProgram line 44
  14. def OAI.MetricKMedian.SparseStarActivation.Program.Input.result line 53
  15. def OAI.MetricKMedian.SparseStarActivation.Program.program line 56