OAI/Combinatorics/KMedianRecovery/Strictness/BidBound.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseRun.bidBound line 10
2. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseRun.budgetBound line 11
3. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseRun.sizeBound line 12
4. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseRun.context_height line 13
5. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseRun.change_phase_length line 37
6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseRun.reference_length line 44
7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseRun.bid_bound line 51
8. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseRun.finish_bound line 60
9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseRun.clipped_bound line 82
10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseRun.run_bound_invariant line 104
11. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseRun.state_length_bound line 137
12. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseRun.run_length_bound line 160
13. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseRun.cap line 182
14. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseRun.run line 183
15. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseRun.run_computes line 185
16. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseRun.run_pack line 188