OAI/Combinatorics/KMedianRecovery/Algorithms/IntegralPrecision.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.Sampling.Comparison.integralPrecision line 12
2. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.integralPrecision_spec line 16
3. abbrev OAI.MetricKMedianRecovery.Sampling.Comparison.IntegralBits line 24
4. def OAI.MetricKMedianRecovery.Sampling.Comparison.integralActions line 27
5. theorem OAI.MetricKMedianRecovery.Sampling.Comparison.integral_records_success line 32
6. theorem OAI.MetricKMedianRecovery.Sampling.Comparison.integral_prefix_exponential line 52