OAI/Combinatorics/KMedianRecovery/Recovery/ReadUnary.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.RationalMetricInput.readUnary line 8
  2. def OAI.MetricKMedianRecovery.RationalMetricInput.readBlock line 15
  3. def OAI.MetricKMedianRecovery.RationalMetricInput.valueBits line 18
  4. def OAI.MetricKMedianRecovery.RationalMetricInput.readNat line 20
  5. lemma OAI.MetricKMedianRecovery.RationalMetricInput.readUnary_code line 25
  6. lemma OAI.MetricKMedianRecovery.RationalMetricInput.readBlock_code line 31
  7. lemma OAI.MetricKMedianRecovery.RationalMetricInput.valueBits_code line 34
  8. lemma OAI.MetricKMedianRecovery.RationalMetricInput.readNat_code line 39
  9. def OAI.MetricKMedianRecovery.RationalMetricInput.signedNumerator line 49
  10. def OAI.MetricKMedianRecovery.RationalMetricInput.readRational line 51
  11. lemma OAI.MetricKMedianRecovery.RationalMetricInput.signedNumerator_code line 58
  12. lemma OAI.MetricKMedianRecovery.RationalMetricInput.readRational_code line 65
  13. def OAI.MetricKMedianRecovery.RationalMetricInput.readMany line 74
  14. lemma OAI.MetricKMedianRecovery.RationalMetricInput.readMany_code line 82
  15. def OAI.MetricKMedianRecovery.RationalMetricInput.readInput line 93
  16. lemma OAI.MetricKMedianRecovery.RationalMetricInput.readMany_code_on line 104
  17. lemma OAI.MetricKMedianRecovery.RationalMetricInput.readRationalRow_code line 116
  18. lemma OAI.MetricKMedianRecovery.RationalMetricInput.readRationalMatrix_code line 122
  19. lemma OAI.MetricKMedianRecovery.RationalMetricInput.readInput_code line 132