OAI/Combinatorics/KMedian/Reduction/NormalizationGuesses.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MetricKMedian.Instance.rationalNearest_nonneg line 13
2. theorem OAI.MetricKMedian.Instance.rationalNearest_attained line 19
3. theorem OAI.MetricKMedian.Instance.maximum_connection line 27
4. theorem OAI.MetricKMedian.Normalization.dyadic_bracket line 64
5. def OAI.MetricKMedian.Normalization.guesses line 81
6. theorem OAI.MetricKMedian.Normalization.guesses_pos line 87
7. theorem OAI.MetricKMedian.Normalization.guesses_card line 94
8. theorem OAI.MetricKMedian.Normalization.good_guess line 108