OAI/Combinatorics/KMedianRecovery/Encoding/EntryIndex.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.history_ball_before line 13
2. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.covered_of_leaf line 29
3. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.history_ball_count line 33
4. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.history_third_spec line 58
5. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.history_disjoint line 80
6. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.history_population_budget line 107
7. def OAI.MetricKMedianRecovery.Sampling.Comparison.entryIndex line 131
8. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.entryIndex_zero line 136
9. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.history_third_index line 145
10. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.history_index_budget line 165
11. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.action_entry_lower line 194
12. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.actionMenuWeight_of_notBall line 208
13. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.actionMenuWeight_le_one line 216
14. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.progressConstant_le_one line 226
15. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.guideLoss_lower line 229
16. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.history_menu_budget line 239
17. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.history_loss_budget line 261
18. def OAI.MetricKMedianRecovery.Sampling.Comparison.samplingBound line 284
19. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.samplingBound_pos line 288
20. theorem OAI.MetricKMedianRecovery.Sampling.Comparison.actual_records_success line 292