OAI/Combinatorics/KMedianRecovery/Recovery/BestFallback.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.FiniteSampling.success_of_mean line 9
2. lemma OAI.MetricKMedianRecovery.FiniteSampling.completion_constant_success line 19
3. lemma OAI.MetricKMedianRecovery.FiniteSampling.probability_all_fin line 28
4. def OAI.MetricKMedianRecovery.FiniteSampling.bestWithFallback line 51
5. lemma OAI.MetricKMedianRecovery.FiniteSampling.bestWithFallback_mem line 57
6. lemma OAI.MetricKMedianRecovery.FiniteSampling.bestWithFallback_le line 71
7. lemma OAI.MetricKMedianRecovery.FiniteSampling.bestWithFallback_failure line 82
8. lemma OAI.MetricKMedianRecovery.FiniteSampling.exponential_failure_bound line 101
9. lemma OAI.MetricKMedianRecovery.FiniteSampling.repetition_count_suffices line 108
10. lemma OAI.MetricKMedianRecovery.FiniteSampling.average_le_threshold_add_failure line 118
11. theorem OAI.MetricKMedianRecovery.FiniteSampling.amplified_output line 132