OAI/Combinatorics/KMedianRecovery/Sampling/SamplingRate.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.Sampling.Comparison.samplingRate line 10
2. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.samplingRate_pos line 14
3. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.samplingBound_eq line 18
4. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.sampling_exponential line 24
5. theorem OAI.MetricKMedianRecovery.Sampling.Comparison.rounded_records_success line 42
6. def OAI.MetricKMedianRecovery.Guided.FixedDyadic.kernel line 60
7. def OAI.MetricKMedianRecovery.Guided.FixedDyadic.draw line 65
8. lemma OAI.MetricKMedianRecovery.Guided.FixedDyadic.draw_average line 68
9. def OAI.MetricKMedianRecovery.Guided.FixedDyadic.actions line 75
10. theorem OAI.MetricKMedianRecovery.Guided.FixedDyadic.actions_average line 82
11. lemma OAI.MetricKMedianRecovery.Guided.FixedDyadic.actions_probability line 108
12. def OAI.MetricKMedianRecovery.Guided.FixedDyadic.Precise line 117
13. lemma OAI.MetricKMedianRecovery.Guided.FixedDyadic.precise_mono line 123
14. theorem OAI.MetricKMedianRecovery.Guided.FixedDyadic.exists_precision line 135
15. lemma OAI.MetricKMedianRecovery.Guided.FixedDyadic.weight_lower line 153
16. lemma OAI.MetricKMedianRecovery.Guided.FixedDyadic.path_lower line 159
17. theorem OAI.MetricKMedianRecovery.Guided.FixedDyadic.event_lower line 172
18. theorem OAI.MetricKMedianRecovery.Guided.FixedDyadic.bounded_fair_realization line 184