OAI/Combinatorics/KMedianRecovery/Recovery/BlindUpdate.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MetricKMedianRecovery.Sampling.Comparison.blindUpdate line 12
2. def OAI.MetricKMedianRecovery.Sampling.Comparison.blindPrecision line 17
3. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.blindPrecision_spec line 22
4. abbrev OAI.MetricKMedianRecovery.Sampling.Comparison.BlindBits line 29
5. def OAI.MetricKMedianRecovery.Sampling.Comparison.blindActions line 32
6. theorem OAI.MetricKMedianRecovery.Sampling.Comparison.fair_records_success line 37
7. theorem OAI.MetricKMedianRecovery.Sampling.Comparison.fair_prefix_exponential line 57
8. def OAI.MetricKMedianRecovery.Sampling.Precision.Good line 75
9. lemma OAI.MetricKMedianRecovery.Sampling.Precision.good_initial line 79
10. lemma OAI.MetricKMedianRecovery.Sampling.Precision.good_retain line 85
11. lemma OAI.MetricKMedianRecovery.Sampling.Precision.good_update line 93
12. lemma OAI.MetricKMedianRecovery.Sampling.Precision.client_lower line 128
13. lemma OAI.MetricKMedianRecovery.Sampling.Precision.total_upper line 152