OAI/Combinatorics/KMedianRecovery/Recovery/Live.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.HistoryPhaseBound.Live line 10
2. def OAI.MetricKMedianRecovery.HistoryPhaseBound.limit line 15
3. lemma OAI.MetricKMedianRecovery.HistoryPhaseBound.limit_threshold line 17
4. lemma OAI.MetricKMedianRecovery.HistoryPhaseBound.active_bound line 30
5. theorem OAI.MetricKMedianRecovery.HistoryPhaseBound.length_bound line 46
6. theorem OAI.MetricKMedianRecovery.HistoryPhaseBound.free_count line 71
7. theorem OAI.MetricKMedianRecovery.HistoryPhaseBound.uniform_copy_bound line 88
8. lemma OAI.MetricKMedianRecovery.HistoryPhaseBound.limit_upper line 113
9. theorem OAI.MetricKMedianRecovery.HistoryPhaseBound.polynomial_limit_bound line 122