OAI/Combinatorics/KMedianRecovery/Encoding/LabelLookup.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabelLookup.item line 9
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabelLookup.item_computes line 10
  3. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLabelLookup.item_pack line 12
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabelLookup.run line 15
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabelLookup.run_computes line 16
  6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLabelLookup.run_pack line 17
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabelLookup.history line 22
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabelLookup.history_computes line 23
  9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLabelLookup.history_pack line 24