OAI/Combinatorics/KMedianRecovery/Branching/CategoricalResources.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.Categorical.Explicit.exponent line 10
2. def OAI.MetricKMedianRecovery.Categorical.Explicit.steps line 11
3. def OAI.MetricKMedianRecovery.Categorical.Explicit.samples line 12
4. lemma OAI.MetricKMedianRecovery.Categorical.Explicit.pow_size_bound line 13
5. lemma OAI.MetricKMedianRecovery.Categorical.Explicit.steps_pos line 21
6. lemma OAI.MetricKMedianRecovery.Categorical.Explicit.steps_lower line 22
7. lemma OAI.MetricKMedianRecovery.Categorical.Explicit.steps_upper line 29
8. lemma OAI.MetricKMedianRecovery.Categorical.Explicit.samples_pos line 36
9. lemma OAI.MetricKMedianRecovery.Categorical.Explicit.scale line 37
10. lemma OAI.MetricKMedianRecovery.Categorical.Explicit.count line 42
11. lemma OAI.MetricKMedianRecovery.Categorical.Explicit.sixtyTwo line 58
12. lemma OAI.MetricKMedianRecovery.Completion.Explicit.expected line 84