OAI/Combinatorics/KMedian/Rounding/SignedPreparationProgram.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.SparseSignedPreparation.Program.QRow line 15
  2. abbrev OAI.MetricKMedian.SparseSignedPreparation.Program.StateRaw line 16
  3. def OAI.MetricKMedian.SparseSignedPreparation.Program.view line 17
  4. structure OAI.MetricKMedian.SparseSignedPreparation.Program.KernelInput line 19
  5. abbrev OAI.MetricKMedian.SparseSignedPreparation.Program.KernelRaw line 25
  6. def OAI.MetricKMedian.SparseSignedPreparation.Program.KernelInput.raw line 26
  7. abbrev OAI.MetricKMedian.SparseSignedPreparation.Program.KernelInput.encode line 28
  8. def OAI.MetricKMedian.SparseSignedPreparation.Program.KernelInput.star line 30
  9. def OAI.MetricKMedian.SparseSignedPreparation.Program.KernelInput.bernoulli line 32
  10. theorem OAI.MetricKMedian.SparseSignedPreparation.Program.point_list line 34
  11. def OAI.MetricKMedian.SparseSignedPreparation.Program.starInputProgram line 38
  12. def OAI.MetricKMedian.SparseSignedPreparation.Program.bernoulliInputProgram line 42
  13. def OAI.MetricKMedian.SparseSignedPreparation.Program.bernoulliProgram line 45
  14. def OAI.MetricKMedian.SparseSignedPreparation.Program.attach line 55
  15. theorem OAI.MetricKMedian.SparseSignedPreparation.Program.attach_poly line 56
  16. def OAI.MetricKMedian.SparseSignedPreparation.Program.KernelInput.result line 61
  17. theorem OAI.MetricKMedian.SparseSignedPreparation.Program.kernel_raw line 63
  18. def OAI.MetricKMedian.SparseSignedPreparation.Program.kernelProgram line 74
  19. structure OAI.MetricKMedian.SparseSignedPreparation.Program.Input line 80
  20. abbrev OAI.MetricKMedian.SparseSignedPreparation.Program.Raw line 88
  21. def OAI.MetricKMedian.SparseSignedPreparation.Program.Input.raw line 89
  22. abbrev OAI.MetricKMedian.SparseSignedPreparation.Program.Input.encode line 91
  23. def OAI.MetricKMedian.SparseSignedPreparation.Program.Input.signed line 93
  24. def OAI.MetricKMedian.SparseSignedPreparation.Program.beta line 95
  25. theorem OAI.MetricKMedian.SparseSignedPreparation.Program.beta_poly line 98
  26. theorem OAI.MetricKMedian.SparseSignedPreparation.Program.beta_input line 99
  27. def OAI.MetricKMedian.SparseSignedPreparation.Program.signedInputProgram line 106
  28. def OAI.MetricKMedian.SparseSignedPreparation.Program.Input.μ line 112
  29. def OAI.MetricKMedian.SparseSignedPreparation.Program.Input.ker line 113
  30. def OAI.MetricKMedian.SparseSignedPreparation.Program.Input.kernels line 117
  31. def OAI.MetricKMedian.SparseSignedPreparation.Program.inputRows line 119
  32. theorem OAI.MetricKMedian.SparseSignedPreparation.Program.inputRows_poly line 121
  33. def OAI.MetricKMedian.SparseSignedPreparation.Program.kernelsProgram line 122
  34. def OAI.MetricKMedian.SparseSignedPreparation.Program.dummy line 134
  35. def OAI.MetricKMedian.SparseSignedPreparation.Program.Input.result line 135
  36. theorem OAI.MetricKMedian.SparseSignedPreparation.Program.result_bind line 138
  37. theorem OAI.MetricKMedian.SparseSignedPreparation.Program.bind_result line 141
  38. def OAI.MetricKMedian.SparseSignedPreparation.Program.weightsProgram line 147
  39. def OAI.MetricKMedian.SparseSignedPreparation.Program.program line 151