OAI/Combinatorics/KMedian/Programs/TaggedBestProgram.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MetricKMedian.SparseSelect.TaggedProgram.Tag line 13
2. def OAI.MetricKMedian.SparseSelect.TaggedProgram.choose line 14
3. theorem OAI.MetricKMedian.SparseSelect.TaggedProgram.choose_poly line 15
4. def OAI.MetricKMedian.SparseSelect.TaggedProgram.decoder line 16
5. def OAI.MetricKMedian.SparseSelect.TaggedProgram.folded line 17
6. theorem OAI.MetricKMedian.SparseSelect.TaggedProgram.folded_poly line 18
7. theorem OAI.MetricKMedian.SparseSelect.TaggedProgram.decode_step line 22
8. theorem OAI.MetricKMedian.SparseSelect.TaggedProgram.folded_best line 31
9. def OAI.MetricKMedian.SparseSelect.TaggedProgram.raw line 40
10. theorem OAI.MetricKMedian.SparseSelect.TaggedProgram.raw_poly line 41
11. theorem OAI.MetricKMedian.SparseSelect.TaggedProgram.raw_best line 42
12. theorem OAI.MetricKMedian.SparseSelect.best_map line 50