OAI/Combinatorics/KMedian/Preparation/PreparedDataOperations.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.SparsePrepared.Program.QRow line 14
  2. abbrev OAI.MetricKMedian.SparsePrepared.Program.NRow line 15
  3. abbrev OAI.MetricKMedian.SparsePrepared.Program.BTable line 16
  4. abbrev OAI.MetricKMedian.SparsePrepared.Program.StateRaw line 17
  5. abbrev OAI.MetricKMedian.SparsePrepared.Program.BaseRaw line 19
  6. abbrev OAI.MetricKMedian.SparsePrepared.Program.KernelRaw line 20
  7. structure OAI.MetricKMedian.SparsePrepared.Program.KernelInput line 21
  8. def OAI.MetricKMedian.SparsePrepared.Program.KernelInput.base line 35
  9. def OAI.MetricKMedian.SparsePrepared.Program.KernelInput.raw line 38
  10. abbrev OAI.MetricKMedian.SparsePrepared.Program.KernelInput.encode line 39
  11. def OAI.MetricKMedian.SparsePrepared.Program.activationData line 41
  12. def OAI.MetricKMedian.SparsePrepared.Program.totalData line 44
  13. def OAI.MetricKMedian.SparsePrepared.Program.pieces line 46
  14. theorem OAI.MetricKMedian.SparsePrepared.Program.activationData_poly line 50
  15. theorem OAI.MetricKMedian.SparsePrepared.Program.totalData_poly line 52
  16. theorem OAI.MetricKMedian.SparsePrepared.Program.pieces_poly line 58
  17. theorem OAI.MetricKMedian.SparsePrepared.Program.activationData_view line 64
  18. theorem OAI.MetricKMedian.SparsePrepared.Program.totalData_view line 70
  19. theorem OAI.MetricKMedian.SparsePrepared.Program.pieces_view line 78