OAI/Combinatorics/KMedianRecovery/Encoding/UniformBits.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.Categorical.uniformBits line 9
2. abbrev OAI.MetricKMedianRecovery.Categorical.BinaryOracleIndex line 15
3. instance OAI.MetricKMedianRecovery.Categorical.binaryOracleIndexFintype line 18
4. instance OAI.MetricKMedianRecovery.Categorical.binaryOracleIndexDecidableEq line 22
5. def OAI.MetricKMedianRecovery.Categorical.binarySeedEquiv line 26
6. lemma OAI.MetricKMedianRecovery.Categorical.binaryOracleIndex_card line 45
7. def OAI.MetricKMedianRecovery.Categorical.binaryGreedyOutput line 52
8. lemma OAI.MetricKMedianRecovery.Categorical.binaryGreedyOutput_feasible line 57
9. lemma OAI.MetricKMedianRecovery.Categorical.binaryGreedyOutput_expected line 63