OAI/Combinatorics/KMedian/Process/CountStepProgram.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.SparseCounts.Program.InputRaw line 15
  2. abbrev OAI.MetricKMedian.SparseCounts.Program.ei line 16
  3. structure OAI.MetricKMedian.SparseCounts.Program.Input line 18
  4. def OAI.MetricKMedian.SparseCounts.Program.columnRaw line 22
  5. def OAI.MetricKMedian.SparseCounts.Program.Input.raw line 24
  6. abbrev OAI.MetricKMedian.SparseCounts.Program.Input.encode line 25
  7. structure OAI.MetricKMedian.SparseCounts.Program.Context line 26
  8. def OAI.MetricKMedian.SparseCounts.Program.Context.raw line 29
  9. abbrev OAI.MetricKMedian.SparseCounts.Program.Context.encode line 30
  10. abbrev OAI.MetricKMedian.SparseCounts.Program.T line 31
  11. abbrev OAI.MetricKMedian.SparseCounts.Program.view line 32
  12. abbrev OAI.MetricKMedian.SparseCounts.Program.State line 33
  13. abbrev OAI.MetricKMedian.SparseCounts.Program.State.encode line 34
  14. def OAI.MetricKMedian.SparseCounts.Program.column line 36
  15. def OAI.MetricKMedian.SparseCounts.Program.update line 38
  16. def OAI.MetricKMedian.SparseCounts.Program.rawColumn line 41
  17. theorem OAI.MetricKMedian.SparseCounts.Program.rawColumn_eq line 45
  18. theorem OAI.MetricKMedian.SparseCounts.Program.update_view line 53
  19. def OAI.MetricKMedian.SparseCounts.Program.State.product line 63
  20. def OAI.MetricKMedian.SparseCounts.Program.rawProduct line 64
  21. theorem OAI.MetricKMedian.SparseCounts.Program.rawProduct_eq line 68
  22. def OAI.MetricKMedian.SparseCounts.Program.productProgram line 77
  23. def OAI.MetricKMedian.SparseCounts.Program.dimensionsProgram line 93
  24. def OAI.MetricKMedian.SparseCounts.Program.featuresProgram line 97
  25. def OAI.MetricKMedian.SparseCounts.Program.compressProgram line 105
  26. def OAI.MetricKMedian.SparseCounts.Program.State.increment line 111
  27. def OAI.MetricKMedian.SparseCounts.Program.State.step line 112
  28. def OAI.MetricKMedian.SparseCounts.Program.incrementProgram line 117
  29. def OAI.MetricKMedian.SparseCounts.Program.activeProgram line 124
  30. def OAI.MetricKMedian.SparseCounts.Program.stepProgram line 131