OAI/Combinatorics/KMedianRecovery/Recovery/NearMass.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.NearClients.sublevel_card line 8
2. lemma OAI.MetricKMedianRecovery.NearClients.exists_le_average line 50
3. def OAI.MetricKMedianRecovery.NearClients.nearMass line 59
4. lemma OAI.MetricKMedianRecovery.NearClients.nearMass_nonneg line 64
5. lemma OAI.MetricKMedianRecovery.NearClients.center_bound line 72
6. lemma OAI.MetricKMedianRecovery.NearClients.main_center_bound line 103
7. lemma OAI.MetricKMedianRecovery.NearClients.main_far_bound line 117
8. lemma OAI.MetricKMedianRecovery.NearClients.main_weight_algebra line 125
9. def OAI.MetricKMedianRecovery.NearClients.progressConstant line 132
10. lemma OAI.MetricKMedianRecovery.NearClients.progressConstant_pos line 134
11. lemma OAI.MetricKMedianRecovery.NearClients.ball_progress line 138
12. lemma OAI.MetricKMedianRecovery.NearClients.removal_progress line 145