OAI/Combinatorics/KMedianRecovery/Recovery/RemovalReplay.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.MetricKMedianRecovery.RemovalReplay line 9
2. def OAI.MetricKMedianRecovery.RemovalReplay.boundaryBid line 35
3. lemma OAI.MetricKMedianRecovery.RemovalReplay.phase_div_le line 39
4. lemma OAI.MetricKMedianRecovery.RemovalReplay.earlier_bid_dominates line 57
5. lemma OAI.MetricKMedianRecovery.RemovalReplay.selected_no_overbid line 95
6. def OAI.MetricKMedianRecovery.suffixMaximum line 109
7. lemma OAI.MetricKMedianRecovery.le_suffixMaximum line 112
8. lemma OAI.MetricKMedianRecovery.suffixMaximum_le line 116
9. theorem OAI.MetricKMedianRecovery.replay_bounded_price_strictness line 120
10. def OAI.MetricKMedianRecovery.ValidExecution.removalReplay line 193
11. theorem OAI.MetricKMedianRecovery.valid_execution_bounded_price_strictness line 228