OAI/Combinatorics/KMedianRecovery/Branching/CompletionCoefficient.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.Sampling.completionAccuracy_pos line 10
2. def OAI.MetricKMedianRecovery.Sampling.completionCoefficient line 16
3. def OAI.MetricKMedianRecovery.Sampling.precisionCoefficient line 19
4. def OAI.MetricKMedianRecovery.Sampling.recoveryCoefficient line 21
5. lemma OAI.MetricKMedianRecovery.Sampling.completionTapeBound_polynomial line 25
6. lemma OAI.MetricKMedianRecovery.Sampling.integralPrecision_polynomial line 30
7. lemma OAI.MetricKMedianRecovery.Sampling.localTapeBound_polynomial line 46
8. theorem OAI.MetricKMedianRecovery.Sampling.recoveryBitCount_polynomial line 59