OAI/Combinatorics/KMedianRecovery/Recovery/IncomingSwapBound.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.Anchoring.incoming_swap_bound line 10
2. lemma OAI.MetricKMedianRecovery.Anchoring.cluster_excess_bound line 63
3. lemma OAI.MetricKMedianRecovery.Anchoring.singleton_ball_client_bound line 71
4. lemma OAI.MetricKMedianRecovery.Anchoring.incoming_charge_bound line 85
5. lemma OAI.MetricKMedianRecovery.Anchoring.cluster_weight_identity line 107
6. lemma OAI.MetricKMedianRecovery.Anchoring.all_cluster_weights line 114
7. lemma OAI.MetricKMedianRecovery.Anchoring.disjoint_family_sum_le line 122
8. lemma OAI.MetricKMedianRecovery.Anchoring.singleton_cluster_charge line 133
9. lemma OAI.MetricKMedianRecovery.Anchoring.incoming_fibers_disjoint line 184