OAI/Combinatorics/KMedianRecovery/Refined/ConditionalRecovery.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.RefinedRecovery.CompanionThresholdInput line 11
2. lemma OAI.MetricKMedianRecovery.RefinedRecovery.quote_eq line 16
3. def OAI.MetricKMedianRecovery.RefinedRecovery.first line 22
4. lemma OAI.MetricKMedianRecovery.RefinedRecovery.first_pair line 25
5. def OAI.MetricKMedianRecovery.RefinedRecovery.totalProgram line 29
6. def OAI.MetricKMedianRecovery.RefinedRecovery.algorithm line 36
7. lemma OAI.MetricKMedianRecovery.RefinedRecovery.algorithm_run line 43
8. theorem OAI.MetricKMedianRecovery.RefinedRecovery.refined_recovery_conditional line 50