OAI/Combinatorics/KMedianRecovery/Recovery/GetRow2.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.getRow line 11
  2. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.getRow_computes line 12
  3. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.getRow_encode line 13
  4. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.entryInput line 18
  5. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.entryInput_computes line 19
  6. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.getEntry line 21
  7. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.getEntry_computes line 22
  8. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.getEntry_encode line 23
  9. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.diagInput line 28
  10. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.diagInput_computes line 29
  11. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.diagAt line 30
  12. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.diagAt_computes line 31
  13. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.diagAt_encode line 32
  14. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.contextMatrix line 36
  15. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.contextIndex line 37
  16. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.contextMatrix_computes line 38
  17. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.contextIndex_computes line 39
  18. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.tailDiagInput line 40
  19. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.tailDiagInput_computes line 41
  20. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.tailDiagValue line 42
  21. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.tailDiagValue_computes line 43
  22. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.tailDiagOp line 45
  23. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.tailDiagOp_computes line 47
  24. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.tailDiagOp_encode line 52
  25. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.tailDiagMapInput line 60
  26. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.tailDiagMapInput_computes line 62
  27. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.tailDiagMap line 64
  28. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.tailDiagMap_computes line 65
  29. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.tailDiag line 67
  30. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.tailDiag_computes line 68
  31. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.tailDiag_encode line 69
  32. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.negDiag line 82
  33. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.negDiag_computes line 84
  34. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.muEntry line 86
  35. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.muEntry_computes line 90
  36. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.mu line 97
  37. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.muEntry_encode line 99
  38. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.muRow line 106
  39. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.muRow_computes line 107
  40. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.muRow_encode line 109
  41. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.muWords line 115
  42. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.muWords_computes line 116
  43. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.muWords_encode line 117
  44. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.mu_mul line 123
  45. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.stepInput line 141
  46. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.stepInput_computes line 142
  47. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.stepWords line 148
  48. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.stepWords_computes line 149
  49. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.stepWords_apply line 153
  50. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.stepInput_pair line 154
  51. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.stepWords_encode line 156