OAI/Combinatorics/KMedianRecovery/Machines/ProjectionMachine.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.BitMachine.BinaryProjection.run line 10
2. def OAI.MetricKMedianRecovery.BitMachine.BinaryProjection.run_computes line 12
3. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryProjection.run_labels line 14
4. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryProjection.run_setBits line 24
5. def OAI.MetricKMedianRecovery.BitMachine.BinaryProjection.originalWord line 28
6. def OAI.MetricKMedianRecovery.BitMachine.BinaryProjection.originalWord_computes line 30
7. def OAI.MetricKMedianRecovery.BitMachine.BinaryProjection.lift line 32
8. def OAI.MetricKMedianRecovery.BitMachine.BinaryProjection.lift_computes line 34
9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryProjection.lift_encode line 36