OAI/Combinatorics/KMedianRecovery/Encoding/BitsInjective.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MetricKMedianRecovery.RationalMetricInput.bits_injective line 8
  2. def OAI.MetricKMedianRecovery.RationalMetricInput.maskSet line 42
  3. def OAI.MetricKMedianRecovery.RationalMetricInput.matrixData line 45
  4. def OAI.MetricKMedianRecovery.RationalMetricInput.validate line 48
  5. def OAI.MetricKMedianRecovery.RationalMetricInput.decodeInput line 60
  6. lemma OAI.MetricKMedianRecovery.RationalMetricInput.maskSet_ofFn line 64
  7. lemma OAI.MetricKMedianRecovery.RationalMetricInput.matrixData_ofFn line 69
  8. lemma OAI.MetricKMedianRecovery.RationalMetricInput.validate_code line 75
  9. lemma OAI.MetricKMedianRecovery.RationalMetricInput.decodeInput_code line 88