OAI/Combinatorics/KMedianRecovery/Refined/Work.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.RefinedRecovery.bits_length_le line 9
2. lemma OAI.MetricKMedianRecovery.RefinedRecovery.natBits_length_le line 14
3. lemma OAI.MetricKMedianRecovery.RefinedRecovery.rationalBits_nat_length line 21
4. def OAI.MetricKMedianRecovery.RefinedRecovery.metricLengthPolynomial line 29
5. lemma OAI.MetricKMedianRecovery.RefinedRecovery.metric_length_bound line 32
6. lemma OAI.MetricKMedianRecovery.RefinedRecovery.polynomial_power_bound line 69
7. lemma OAI.MetricKMedianRecovery.RefinedRecovery.zero_random_polynomialWork line 85