OAI/Combinatorics/KMedian/Programs/GraphStepProgram.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.SparseGraph.Program.InputRaw line 16
  2. abbrev OAI.MetricKMedian.SparseGraph.Program.ei line 17
  3. structure OAI.MetricKMedian.SparseGraph.Program.Input line 19
  4. def OAI.MetricKMedian.SparseGraph.Program.columnRaw line 23
  5. def OAI.MetricKMedian.SparseGraph.Program.Input.raw line 25
  6. abbrev OAI.MetricKMedian.SparseGraph.Program.Input.encode line 26
  7. structure OAI.MetricKMedian.SparseGraph.Program.Context line 27
  8. def OAI.MetricKMedian.SparseGraph.Program.Context.raw line 30
  9. abbrev OAI.MetricKMedian.SparseGraph.Program.Context.encode line 31
  10. abbrev OAI.MetricKMedian.SparseGraph.Program.T line 32
  11. abbrev OAI.MetricKMedian.SparseGraph.Program.view line 33
  12. abbrev OAI.MetricKMedian.SparseGraph.Program.State line 34
  13. abbrev OAI.MetricKMedian.SparseGraph.Program.State.encode line 35
  14. def OAI.MetricKMedian.SparseGraph.Program.column line 37
  15. def OAI.MetricKMedian.SparseGraph.Program.update line 39
  16. def OAI.MetricKMedian.SparseGraph.Program.rawColumn line 42
  17. theorem OAI.MetricKMedian.SparseGraph.Program.rawColumn_eq line 46
  18. theorem OAI.MetricKMedian.SparseGraph.Program.update_view line 54
  19. def OAI.MetricKMedian.SparseGraph.Program.State.product line 64
  20. def OAI.MetricKMedian.SparseGraph.Program.rawProduct line 65
  21. theorem OAI.MetricKMedian.SparseGraph.Program.rawProduct_eq line 69
  22. def OAI.MetricKMedian.SparseGraph.Program.productProgram line 78
  23. def OAI.MetricKMedian.SparseGraph.Program.dimensionsProgram line 94
  24. def OAI.MetricKMedian.SparseGraph.Program.featuresProgram line 98
  25. def OAI.MetricKMedian.SparseGraph.Program.compressProgram line 106
  26. def OAI.MetricKMedian.SparseGraph.Program.State.increment line 112
  27. def OAI.MetricKMedian.SparseGraph.Program.State.step line 113
  28. def OAI.MetricKMedian.SparseGraph.Program.incrementProgram line 118
  29. def OAI.MetricKMedian.SparseGraph.Program.activeProgram line 125
  30. def OAI.MetricKMedian.SparseGraph.Program.stepProgram line 132