OAI/Combinatorics/KMedianRecovery/Encoding/RationalBest.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalBest.choose line 10
2. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalBest.choose_computes line 14
3. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRationalBest.choose_pack line 19
4. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalBest.pack line 25
5. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalBest.run line 26
6. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalBest.run_computes line 29
7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRationalBest.run_pack line 32
8. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalBest.fromList line 50
9. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalBest.fromList_computes line 52
10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRationalBest.fromList_pack line 55