OAI/Combinatorics/KMedianRecovery/Branching/CategoricalRule.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.MetricKMedianRecovery.Categorical.Selected.Rule line 8
2. lemma OAI.MetricKMedianRecovery.Categorical.Selected.Rule.surjective line 11
3. def OAI.MetricKMedianRecovery.Categorical.Selected.greedyStep line 14
4. lemma OAI.MetricKMedianRecovery.Categorical.Selected.greedyStep_clock line 22
5. lemma OAI.MetricKMedianRecovery.Categorical.Selected.greedyStep_invariant line 28
6. lemma OAI.MetricKMedianRecovery.Categorical.Selected.sampled_select_choice line 52
7. lemma OAI.MetricKMedianRecovery.Categorical.Selected.greedyStep_recurrence line 66
8. lemma OAI.MetricKMedianRecovery.Categorical.Selected.greedy_failure_bound line 83
9. def OAI.MetricKMedianRecovery.Categorical.Selected.greedyRun line 101
10. def OAI.MetricKMedianRecovery.Categorical.Selected.greedyOutput line 105
11. lemma OAI.MetricKMedianRecovery.Categorical.Selected.greedyRun_invariant line 110
12. lemma OAI.MetricKMedianRecovery.Categorical.Selected.greedyOutput_feasible line 117
13. lemma OAI.MetricKMedianRecovery.Categorical.Selected.greedyRun_expectation line 123
14. lemma OAI.MetricKMedianRecovery.Categorical.Selected.greedyRun_good line 131
15. lemma OAI.MetricKMedianRecovery.Categorical.Selected.greedyOutput_expected line 169
16. lemma OAI.MetricKMedianRecovery.Categorical.Selected.categorical_expected line 210
17. def OAI.MetricKMedianRecovery.Categorical.Selected.binaryGreedyOutput line 243
18. lemma OAI.MetricKMedianRecovery.Categorical.Selected.binaryGreedyOutput_feasible line 248
19. lemma OAI.MetricKMedianRecovery.Categorical.Selected.binaryGreedyOutput_expected line 254