OAI/Combinatorics/KMedian/Sparse/SparseEnumeratedBatch.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.SparseEnumeratedBatch.law line 10
2. theorem OAI.MetricKMedian.SparseEnumeratedBatch.length line 18
3. theorem OAI.MetricKMedian.SparseEnumeratedBatch.marginal_error line 23
4. theorem OAI.MetricKMedian.SparseEnumeratedBatch.pair_le line 40
5. theorem OAI.MetricKMedian.SparseEnumeratedBatch.marginal_le line 51
6. def OAI.MetricKMedian.SparseEnumeratedBatch.sortedEnumeration line 61