OAI/Combinatorics/KMedianRecovery/Recovery/LeafReplay.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.CanonicalLeafReplay.Runs.swap_free line 14
2. lemma OAI.MetricKMedianRecovery.CanonicalLeafReplay.Runs.insert_far line 43
3. lemma OAI.MetricKMedianRecovery.CanonicalLeafReplay.Runs.replace_paid line 56
4. lemma OAI.MetricKMedianRecovery.RationalLeaves.far_replay line 77
5. lemma OAI.MetricKMedianRecovery.RationalLeaves.zero_free_replay line 109
6. lemma OAI.MetricKMedianRecovery.RationalLeaves.zero_paid_replay line 148
7. lemma OAI.MetricKMedianRecovery.RationalLeaves.append_leaf line 184