OAI/Combinatorics/KMedianRecovery/Recovery/DirectionChoiceErrors.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.Categorical.direction_le_of_choiceErrors line 10
2. lemma OAI.MetricKMedianRecovery.Categorical.two_estimates_choice line 31
3. theorem OAI.MetricKMedianRecovery.Categorical.estimated_comparison_direction line 39
4. lemma OAI.MetricKMedianRecovery.affine_growth_bound line 51
5. lemma OAI.MetricKMedianRecovery.continuous_greedy_growth line 64