OAI/Combinatorics/KMedianRecovery/Encoding/Encode.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.BitMachine.Signed.encode_length line 9
  2. lemma OAI.MetricKMedianRecovery.BitMachine.Signed.natSize_add line 11
  3. lemma OAI.MetricKMedianRecovery.BitMachine.Signed.encode_add_length line 20
  4. lemma OAI.MetricKMedianRecovery.BitMachine.Signed.encode_sum_length line 25
  5. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.length_encode_take line 35
  6. def OAI.MetricKMedianRecovery.BitMachine.IntegerArray.encode line 43
  7. def OAI.MetricKMedianRecovery.BitMachine.IntegerArray.addOp line 44
  8. def OAI.MetricKMedianRecovery.BitMachine.IntegerArray.addOp_computes line 46
  9. lemma OAI.MetricKMedianRecovery.BitMachine.IntegerArray.fold_add line 47
  10. def OAI.MetricKMedianRecovery.BitMachine.IntegerArray.sumWords line 58
  11. def OAI.MetricKMedianRecovery.BitMachine.IntegerArray.sumWords_computes line 60
  12. lemma OAI.MetricKMedianRecovery.BitMachine.IntegerArray.sumWords_encode line 63
  13. def OAI.MetricKMedianRecovery.BitMachine.IntegerArray.sum line 78
  14. def OAI.MetricKMedianRecovery.BitMachine.IntegerArray.encodePairs line 81
  15. def OAI.MetricKMedianRecovery.BitMachine.IntegerArray.mulOp line 83
  16. def OAI.MetricKMedianRecovery.BitMachine.IntegerArray.mulOp_computes line 85
  17. def OAI.MetricKMedianRecovery.BitMachine.IntegerArray.dotWords line 87
  18. def OAI.MetricKMedianRecovery.BitMachine.IntegerArray.mappedProducts_computes line 89
  19. def OAI.MetricKMedianRecovery.BitMachine.IntegerArray.prefixEmpty_computes line 91
  20. def OAI.MetricKMedianRecovery.BitMachine.IntegerArray.productsWords_computes line 93
  21. def OAI.MetricKMedianRecovery.BitMachine.IntegerArray.dotWords_computes line 97
  22. lemma OAI.MetricKMedianRecovery.BitMachine.IntegerArray.dotWords_encode line 100
  23. def OAI.MetricKMedianRecovery.BitMachine.IntegerArray.dot line 105