OAI/Combinatorics/KMedianRecovery/Recovery/Destinations.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.Sampling.Comparison.destinations line 12
2. def OAI.MetricKMedianRecovery.Sampling.Comparison.ownDestination line 18
3. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.ownDestination_mem line 24
4. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.destinations_nonempty line 35
5. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.own_charge_good line 40
6. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.own_charge_covered line 46
7. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.own_charge_uncovered line 56
8. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.convex_capped_le line 64
9. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.interpolated_reference_le line 69
10. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.interpolated_covered_charge line 76
11. def OAI.MetricKMedianRecovery.Sampling.Comparison.endpointCharge line 102
12. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.own_charge_le_endpoint line 110
13. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.interpolation_le_endpoint line 126
14. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.endpoint_charge_sum line 146
15. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.completion_endpoint_success line 178
16. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.surrogate_success line 215