OAI/Combinatorics/KMedian/Preparation/PreparedLawProgram.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MetricKMedian.SparsePrepared.Program.Input line 13
  2. abbrev OAI.MetricKMedian.SparsePrepared.Program.Raw line 28
  3. def OAI.MetricKMedian.SparsePrepared.Program.Input.base line 29
  4. def OAI.MetricKMedian.SparsePrepared.Program.Input.raw line 32
  5. abbrev OAI.MetricKMedian.SparsePrepared.Program.Input.encode line 33
  6. def OAI.MetricKMedian.SparsePrepared.Program.Input.outer line 35
  7. def OAI.MetricKMedian.SparsePrepared.Program.outerData line 36
  8. theorem OAI.MetricKMedian.SparsePrepared.Program.outerData_poly line 38
  9. def OAI.MetricKMedian.SparsePrepared.Program.outerInputProgram line 42
  10. def OAI.MetricKMedian.SparsePrepared.Program.Input.μ line 46
  11. def OAI.MetricKMedian.SparsePrepared.Program.Input.ker line 47
  12. def OAI.MetricKMedian.SparsePrepared.Program.Input.kernels line 49
  13. def OAI.MetricKMedian.SparsePrepared.Program.kernelRows line 51
  14. theorem OAI.MetricKMedian.SparsePrepared.Program.kernelRows_poly line 52
  15. def OAI.MetricKMedian.SparsePrepared.Program.kernelsProgram line 53
  16. def OAI.MetricKMedian.SparsePrepared.Program.dummy line 61
  17. def OAI.MetricKMedian.SparsePrepared.Program.Input.result line 63
  18. theorem OAI.MetricKMedian.SparsePrepared.Program.result_bind line 66
  19. theorem OAI.MetricKMedian.SparsePrepared.Program.bind_result line 69
  20. def OAI.MetricKMedian.SparsePrepared.Program.weightsProgram line 75
  21. def OAI.MetricKMedian.SparsePrepared.Program.program line 77