OAI/Combinatorics/KMedian/Programs/OuterLawProgram.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MetricKMedian.SparseOuterLaw.Program.Input line 14
  2. abbrev OAI.MetricKMedian.SparseOuterLaw.Program.Raw line 22
  3. def OAI.MetricKMedian.SparseOuterLaw.Program.Input.raw line 23
  4. abbrev OAI.MetricKMedian.SparseOuterLaw.Program.Input.encode line 25
  5. def OAI.MetricKMedian.SparseOuterLaw.Program.Input.signed line 26
  6. def OAI.MetricKMedian.SparseOuterLaw.Program.post line 28
  7. theorem OAI.MetricKMedian.SparseOuterLaw.Program.post_poly line 29
  8. def OAI.MetricKMedian.SparseOuterLaw.Program.signedProgram line 30
  9. def OAI.MetricKMedian.SparseOuterLaw.Program.Input.result line 34
  10. def OAI.MetricKMedian.SparseOuterLaw.Program.program line 37