OAI/Combinatorics/KMedian/Sparse/SparseStarActivation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.SparseStarActivation.law line 14
2. def OAI.MetricKMedian.SparseStarActivation.upper line 18
3. theorem OAI.MetricKMedian.SparseStarActivation.mean line 20
4. theorem OAI.MetricKMedian.SparseStarActivation.pair line 28
5. theorem OAI.MetricKMedian.SparseStarActivation.columns line 37
6. theorem OAI.MetricKMedian.SparseStarActivation.upper_domination line 49
7. theorem OAI.MetricKMedian.SparseStarActivation.error line 59
8. theorem OAI.MetricKMedian.SparseStarActivation.length line 89