OAI/Combinatorics/KMedian/Preparation/PreparationStars.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MetricKMedian.Preparation.SupplierStars.Star line 11
2. def OAI.MetricKMedian.Preparation.SupplierStars.outside line 13
3. def OAI.MetricKMedian.Preparation.SupplierStars.targets line 15
4. def OAI.MetricKMedian.Preparation.SupplierStars.flag line 20
5. def OAI.MetricKMedian.Preparation.SupplierStars.weight line 24
6. theorem OAI.MetricKMedian.Preparation.SupplierStars.mass_partition line 31
7. theorem OAI.MetricKMedian.Preparation.SupplierStars.targeted_weight line 49
8. theorem OAI.MetricKMedian.Preparation.SupplierStars.flagged_weight line 67
9. theorem OAI.MetricKMedian.Preparation.SupplierStars.target_card_sum line 72
10. theorem OAI.MetricKMedian.Preparation.SupplierStars.raw_identity line 79
11. theorem OAI.MetricKMedian.Preparation.SupplierStars.weight_nonneg line 96