OAI/Combinatorics/KMedian/Geometry/RationalSplitting.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.Preparation.RationalSplitting.cuts line 12
2. abbrev OAI.MetricKMedian.Preparation.RationalSplitting.Piece line 15
3. def OAI.MetricKMedian.Preparation.RationalSplitting.weight line 17
4. def OAI.MetricKMedian.Preparation.RationalSplitting.assignment line 20
5. theorem OAI.MetricKMedian.Preparation.RationalSplitting.cuts_pos line 24
6. theorem OAI.MetricKMedian.Preparation.RationalSplitting.cuts_le line 28
7. theorem OAI.MetricKMedian.Preparation.RationalSplitting.weight_pos line 37
8. theorem OAI.MetricKMedian.Preparation.RationalSplitting.weight_le line 41
9. theorem OAI.MetricKMedian.Preparation.RationalSplitting.sum_fiber line 46
10. theorem OAI.MetricKMedian.Preparation.RationalSplitting.sum_weight line 52
11. theorem OAI.MetricKMedian.Preparation.RationalSplitting.assigned_fiber line 58
12. theorem OAI.MetricKMedian.Preparation.RationalSplitting.sum_assignment line 69
13. theorem OAI.MetricKMedian.Preparation.RationalSplitting.card_pieces line 74
14. theorem OAI.MetricKMedian.Preparation.RationalSplitting.cost_assignment line 86
15. theorem OAI.MetricKMedian.Preparation.RationalSplitting.nearest_assignment line 104