OAI/Combinatorics/KMedianRecovery/Strictness/BidPoly.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFinish.bidPoly line 8
2. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFinish.capPoly line 9
3. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFinish.ctx_bound line 10
4. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFinish.first_bid_bound line 22
5. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFinish.finish_invariant line 50
6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFinish.finish_length line 72
7. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFinish.cap line 95
8. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFinish.run line 97
9. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFinish.run_computes line 99
10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFinish.run_pack line 102