OAI/Combinatorics/KMedianRecovery/Recovery/InitialRows.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.PhaseUpperBracket.payment_small line 11
2. lemma OAI.MetricKMedianRecovery.PhaseUpperBracket.small_impossible line 39
3. lemma OAI.MetricKMedianRecovery.PhaseUpperBracket.inactive_impossible line 53
4. lemma OAI.MetricKMedianRecovery.PhaseUpperBracket.prefix_invariant line 87
5. lemma OAI.MetricKMedianRecovery.PhaseUpperBracket.history_invariant line 110
6. theorem OAI.MetricKMedianRecovery.PhaseUpperBracket.attains_high line 125
7. lemma OAI.MetricKMedianRecovery.PhaseInitialBracket.empty_prefix line 142