OAI/Combinatorics/KMedian/Sparse/SparseCountFeatures.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.SparseCounts.Table line 14
  2. def OAI.MetricKMedian.SparseCounts.edge line 16
  3. def OAI.MetricKMedian.SparseCounts.edgeCode line 18
  4. def OAI.MetricKMedian.SparseCounts.features line 21
  5. theorem OAI.MetricKMedian.SparseCounts.features_single line 26
  6. theorem OAI.MetricKMedian.SparseCounts.features_pair line 30
  7. def OAI.MetricKMedian.SparseCounts.next line 35
  8. theorem OAI.MetricKMedian.SparseCounts.edge_next line 38
  9. def OAI.MetricKMedian.SparseCounts.step line 42
  10. theorem OAI.MetricKMedian.SparseCounts.step_single line 46
  11. theorem OAI.MetricKMedian.SparseCounts.step_pair line 60
  12. theorem OAI.MetricKMedian.SparseCounts.step_same line 79