OAI/Combinatorics/KMedian/Optimization/GradientDenominator.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.RationalGrid.At line 11
2. theorem OAI.MetricKMedian.RationalGrid.zero line 13
3. theorem OAI.MetricKMedian.RationalGrid.integer line 15
4. theorem OAI.MetricKMedian.RationalGrid.sub line 19
5. theorem OAI.MetricKMedian.RationalGrid.neg line 24
6. theorem OAI.MetricKMedian.RationalGrid.max line 28
7. theorem OAI.MetricKMedian.RationalGrid.sum line 33
8. theorem OAI.MetricKMedian.TruncatedLP.truncated_grid line 49
9. theorem OAI.MetricKMedian.TruncatedLP.threshold_grid line 56
10. theorem OAI.MetricKMedian.TruncatedLP.gradient_grid line 67