OAI/Combinatorics/KMedian/Preparation/PreparedKernelProgram.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.SparsePrepared.Program.KernelInput.bundles line 13
  2. def OAI.MetricKMedian.SparsePrepared.Program.bundleData line 16
  3. theorem OAI.MetricKMedian.SparsePrepared.Program.bundleData_poly line 17
  4. def OAI.MetricKMedian.SparsePrepared.Program.bundleInputProgram line 21
  5. abbrev OAI.MetricKMedian.SparsePrepared.Program.PreparedRaw line 28
  6. def OAI.MetricKMedian.SparsePrepared.Program.attach line 29
  7. theorem OAI.MetricKMedian.SparsePrepared.Program.attach_poly line 31
  8. def OAI.MetricKMedian.SparsePrepared.Program.view line 36
  9. def OAI.MetricKMedian.SparsePrepared.Program.KernelInput.result line 38
  10. theorem OAI.MetricKMedian.SparsePrepared.Program.kernel_result line 41
  11. def OAI.MetricKMedian.SparsePrepared.Program.kernelProgram line 45