OAI/Combinatorics/KMedianRecovery/Recovery/GetRow.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.getRow line 13
  2. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.getRow_computes line 14
  3. lemma OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.getRow_encode line 15
  4. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.entryInput line 20
  5. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.entryInput_computes line 21
  6. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.getEntry line 23
  7. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.getEntry_computes line 24
  8. lemma OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.getEntry_encode line 25
  9. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.diagInput line 30
  10. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.diagInput_computes line 31
  11. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.diagAt line 32
  12. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.diagAt_computes line 33
  13. lemma OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.diagAt_encode line 34
  14. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.contextMatrix line 38
  15. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.contextIndex line 39
  16. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.contextMatrix_computes line 40
  17. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.contextIndex_computes line 41
  18. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.tailDiagInput line 42
  19. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.tailDiagInput_computes line 43
  20. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.tailDiagValue line 44
  21. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.tailDiagValue_computes line 45
  22. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.tailDiagOp line 47
  23. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.tailDiagOp_computes line 49
  24. lemma OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.tailDiagOp_encode line 54
  25. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.tailDiagMapInput line 62
  26. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.tailDiagMapInput_computes line 64
  27. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.tailDiagMap line 66
  28. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.tailDiagMap_computes line 67
  29. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.tailDiag line 69
  30. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.tailDiag_computes line 70
  31. lemma OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.tailDiag_encode line 71
  32. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.negDiag line 84
  33. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.negDiag_computes line 86
  34. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.muEntry line 88
  35. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.muEntry_computes line 92
  36. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.mu line 99
  37. lemma OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.muEntry_encode line 101
  38. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.muRow line 108
  39. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.muRow_computes line 109
  40. lemma OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.muRow_encode line 111
  41. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.muWords line 117
  42. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.muWords_computes line 118
  43. lemma OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.muWords_encode line 119
  44. lemma OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.mu_mul line 125
  45. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.stepInput line 143
  46. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.stepInput_computes line 144
  47. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.stepWords line 146
  48. def OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.stepWords_computes line 147
  49. lemma OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.stepWords_apply line 148
  50. lemma OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.stepInput_pair line 149
  51. lemma OAI.MetricKMedianRecovery.BitMachine.IntegerMatrix.stepWords_encode line 151