OAI/Combinatorics/KMedianRecovery/Encoding/DuplicateMatrix.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryDuplicateMatrix.forget line 9
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryDuplicateMatrix.duplicate line 10
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryDuplicateMatrix.twice line 12
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryDuplicateMatrix.twice_computes line 13
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryDuplicateMatrix.run line 14
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryDuplicateMatrix.run_computes line 15
  7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDuplicateMatrix.row_double line 16
  8. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDuplicateMatrix.forget_left line 21
  9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDuplicateMatrix.forget_right line 22
  10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDuplicateMatrix.run_encode line 23