OAI/Combinatorics/KMedian/Rounding/WeightedGridInvariant.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MetricKMedian.RationalGrid.add line 12
2. theorem OAI.MetricKMedian.RationalGrid.mul line 17
3. theorem OAI.MetricKMedian.RationalWeightedStep.point_move_self line 28
4. theorem OAI.MetricKMedian.RationalWeightedStep.point_move_other line 31
5. theorem OAI.MetricKMedian.RationalWeightedStep.point_move_rest line 34
6. theorem OAI.MetricKMedian.RationalWeightedStep.move_pair_weighted line 38
7. theorem OAI.MetricKMedian.RationalWeightedStep.up_integral line 46
8. theorem OAI.MetricKMedian.RationalWeightedStep.down_integral line 54
9. theorem OAI.MetricKMedian.RationalWeightedStep.endpoint_grid line 62