OAI/Combinatorics/KMedianRecovery/Encoding/Encode2.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRational.encode_length line 10
  2. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRational.encode_height line 12
  3. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRational.input_height line 19
  4. def OAI.MetricKMedianRecovery.BitMachine.RationalArray.encode line 31
  5. lemma OAI.MetricKMedianRecovery.BitMachine.RationalArray.input_height line 32
  6. def OAI.MetricKMedianRecovery.BitMachine.RationalArray.addOp line 35
  7. def OAI.MetricKMedianRecovery.BitMachine.RationalArray.addOp_computes line 36
  8. lemma OAI.MetricKMedianRecovery.BitMachine.RationalArray.fold_add line 37
  9. def OAI.MetricKMedianRecovery.BitMachine.RationalArray.sumInput line 48
  10. def OAI.MetricKMedianRecovery.BitMachine.RationalArray.sumInput_computes line 50
  11. def OAI.MetricKMedianRecovery.BitMachine.RationalArray.sumWords line 52
  12. def OAI.MetricKMedianRecovery.BitMachine.RationalArray.sumWords_computes line 54
  13. lemma OAI.MetricKMedianRecovery.BitMachine.RationalArray.sumWords_encode line 56
  14. def OAI.MetricKMedianRecovery.BitMachine.RationalArray.sum line 80
  15. def OAI.MetricKMedianRecovery.BitMachine.RationalArray.mulOp line 83
  16. def OAI.MetricKMedianRecovery.BitMachine.RationalArray.mulOp_computes line 84
  17. def OAI.MetricKMedianRecovery.BitMachine.RationalArray.encodePairs line 85
  18. def OAI.MetricKMedianRecovery.BitMachine.RationalArray.dotWords line 87
  19. def OAI.MetricKMedianRecovery.BitMachine.RationalArray.dotWords_computes line 89
  20. lemma OAI.MetricKMedianRecovery.BitMachine.RationalArray.dotWords_encode line 91
  21. def OAI.MetricKMedianRecovery.BitMachine.RationalArray.dotListsWords line 96
  22. def OAI.MetricKMedianRecovery.BitMachine.RationalArray.dotListsWords_computes line 97
  23. lemma OAI.MetricKMedianRecovery.BitMachine.RationalArray.dotListsWords_encode line 98
  24. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.rowEncode line 107
  25. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.encode line 108
  26. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.rowEncode_eq line 110
  27. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.swapWords line 114
  28. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.swapWords_computes line 115
  29. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.columnOp line 117
  30. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.columnMap_computes line 118
  31. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.columnOp_computes line 120
  32. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.columnOp_encode line 122
  33. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.matrixIndices line 127
  34. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.matrixIndices_computes line 128
  35. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.transposeWords line 129
  36. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.transposeMap_computes line 130
  37. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.transposeWords_computes line 131
  38. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.transposeWords_encode line 133
  39. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.rightRowOp line 142
  40. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.rightRowMap_computes line 143
  41. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.rightRowOp_computes line 145
  42. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.dotListsWords_ofFn line 148
  43. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.rightRowOp_encode line 158
  44. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.mulInput line 167
  45. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.mulInput_computes line 169
  46. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.mulWords line 175
  47. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.mulMap_computes line 176
  48. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.mulWords_computes line 177
  49. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.mulWords_encode line 179
  50. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.multiplication line 187