OAI/Combinatorics/KMedianRecovery/Recovery/LengthSearch.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.CanonicalLengthSearch.chosen line 12
2. def OAI.MetricKMedianRecovery.CanonicalLengthSearch.count line 15
3. inductive OAI.MetricKMedianRecovery.CanonicalLengthSearch.Result line 19
4. def OAI.MetricKMedianRecovery.CanonicalLengthSearch.range line 23
5. lemma OAI.MetricKMedianRecovery.CanonicalLengthSearch.range_spec line 29
6. def OAI.MetricKMedianRecovery.CanonicalLengthSearch.run line 57
7. def OAI.MetricKMedianRecovery.CanonicalLengthSearch.Result.Spec line 65
8. lemma OAI.MetricKMedianRecovery.CanonicalLengthSearch.run_spec line 71
9. def OAI.MetricKMedianRecovery.CanonicalSensitiveEndpoint.EndpointSpec line 106
10. lemma OAI.MetricKMedianRecovery.CanonicalSensitiveEndpoint.endpoints line 120