OAI/Combinatorics/KMedianRecovery/Recovery/GreedyOutputExpected.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.Categorical.greedyOutput_expected line 9
2. def OAI.MetricKMedianRecovery.Categorical.PartitionFeasible line 58
3. lemma OAI.MetricKMedianRecovery.Categorical.diminishing_of_submodular line 62
4. lemma OAI.MetricKMedianRecovery.Categorical.partitionFeasible_singleton line 72
5. lemma OAI.MetricKMedianRecovery.Categorical.partitionFeasible_image line 78
6. lemma OAI.MetricKMedianRecovery.Categorical.exists_filling line 90
7. lemma OAI.MetricKMedianRecovery.Categorical.exists_optimal_assignment line 110
8. lemma OAI.MetricKMedianRecovery.Categorical.zero_of_boundedMarginals_zero line 126