OAI/Combinatorics/KMedianRecovery/Recovery/Advance.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.Categorical.advance line 10
2. lemma OAI.MetricKMedianRecovery.Categorical.batch_advance line 18
3. lemma OAI.MetricKMedianRecovery.Categorical.batch_room line 28
4. lemma OAI.MetricKMedianRecovery.Categorical.choices_batch line 44
5. lemma OAI.MetricKMedianRecovery.Categorical.sampled_direction line 53
6. lemma OAI.MetricKMedianRecovery.Categorical.derivative_bounds line 73
7. def OAI.MetricKMedianRecovery.Categorical.select line 84
8. lemma OAI.MetricKMedianRecovery.Categorical.select_spec line 93
9. def OAI.MetricKMedianRecovery.FiniteSampling.adaptiveRun line 110
10. lemma OAI.MetricKMedianRecovery.FiniteSampling.adaptiveRun_invariant line 115
11. lemma OAI.MetricKMedianRecovery.FiniteSampling.adaptiveRun_growth line 122