OAI/Combinatorics/KMedian/Sparse/SparseOuterCounts.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MetricKMedian.SparseOuterLaw.point_fixed line 16
2. def OAI.MetricKMedian.SparseOuterLaw.outsideCount line 31
3. def OAI.MetricKMedian.SparseOuterLaw.activationCount line 34
4. theorem OAI.MetricKMedian.SparseOuterLaw.outsideCount_cast line 38
5. theorem OAI.MetricKMedian.SparseOuterLaw.activationCount_cast line 43
6. theorem OAI.MetricKMedian.SparseOuterLaw.outsideCount_le line 48
7. theorem OAI.MetricKMedian.SparseOuterLaw.activationCount_support line 70
8. theorem OAI.MetricKMedian.SparseOuterLaw.activationCount_le line 77