OAI/Combinatorics/KMedian/Sparse/SparseCardinalRounding.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.SparseCardinalRounding.round line 13
2. theorem OAI.MetricKMedian.SparseCardinalRounding.integral_of_small_fractional line 16
3. theorem OAI.MetricKMedian.SparseCardinalRounding.round_invariants line 37
4. theorem OAI.MetricKMedian.SparseCardinalRounding.round_mean line 50
5. theorem OAI.MetricKMedian.SparseCardinalRounding.round_pair line 54
6. theorem OAI.MetricKMedian.SparseCardinalRounding.round_length line 58
7. def OAI.MetricKMedian.SparseCardinalRounding.selected line 61
8. theorem OAI.MetricKMedian.SparseCardinalRounding.selected_indicator line 63
9. theorem OAI.MetricKMedian.SparseCardinalRounding.selected_card line 68