OAI/Combinatorics/KMedianRecovery/Encoding/RowEncode.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.lookup_ofFn line 12
  2. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.mapWith_ofFn line 16
  3. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.indices_ofFn line 20
  4. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.rowEncode line 32
  5. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.encode line 33
  6. lemma OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.rowEncode_eq line 35
  7. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.swapWords line 39
  8. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.swapWords_computes line 40
  9. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.columnOp line 42
  10. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.columnMap_computes line 43
  11. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.columnOp_computes line 45
  12. lemma OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.columnOp_encode line 47
  13. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.matrixIndices line 52
  14. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.matrixIndices_computes line 53
  15. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.transposeWords line 54
  16. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.transposeMap_computes line 55
  17. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.transposeWords_computes line 56
  18. lemma OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.transposeWords_encode line 58
  19. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.rightRowOp line 67
  20. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.rightRowMap_computes line 68
  21. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.rightRowOp_computes line 70
  22. lemma OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.dotListsWords_ofFn line 73
  23. lemma OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.rightRowOp_encode line 83
  24. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.mulInput line 92
  25. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.mulInput_computes line 94
  26. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.mulWords line 96
  27. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.mulMap_computes line 97
  28. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.mulWords_computes line 98
  29. lemma OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.mulWords_encode line 100
  30. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.multiplication line 108