OAI/Combinatorics/KMedianRecovery/Recovery/NumAbs.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidRoot.numAbs line 13
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidRoot.den line 14
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidRoot.precision line 15
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidRoot.numAbs_computes line 16
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidRoot.den_computes line 18
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidRoot.precision_computes line 19
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidRoot.radicand line 21
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidRoot.radicand_computes line 23
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidRoot.upper line 28
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidRoot.upper_computes line 29
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidRoot.denom line 34
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidRoot.denom_computes line 35
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidRoot.rawWords line 36
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidRoot.rawWords_computes line 38
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidRoot.run line 40
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidRoot.run_computes line 41
  17. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidRoot.run_encode line 42
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryEllipsoidRoot.rationalRootUpper line 55
  19. def OAI.MetricKMedianRecovery.BitMachine.WordList.pointwise line 63
  20. def OAI.MetricKMedianRecovery.BitMachine.WordList.pointwise_computes line 65
  21. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.zip_ofFn line 75
  22. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.pointwise_ofFn line 81
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.subInput line 89
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.subInput_computes line 90
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.subWords line 92
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.subWords_computes line 93
  27. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRational.subWords_pair line 94
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.secondInverse line 97
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.secondInverse_computes line 98
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.divInput line 100
  31. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.divInput_computes line 101
  32. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.divWords line 103
  33. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.divWords_computes line 104
  34. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRational.divWords_pair line 105
  35. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.natWords line 108
  36. def OAI.MetricKMedianRecovery.BitMachine.BinaryRational.natWords_computes line 109
  37. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRational.natWords_bits line 111
  38. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.vectorAdd line 116
  39. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.vectorAdd_computes line 117
  40. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.vectorAdd_encode line 118
  41. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.vectorSub line 121
  42. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.vectorSub_computes line 122
  43. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.vectorSub_encode line 123
  44. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.vectorScale line 126
  45. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.vectorScale_computes line 127
  46. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.vectorScale_encode line 128
  47. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.matrixAdd line 131
  48. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.matrixAdd_computes line 132
  49. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.matrixAdd_encode line 133
  50. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.matrixSub line 137
  51. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.matrixSub_computes line 138
  52. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.matrixSub_encode line 139
  53. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.matrixScale line 143
  54. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.matrixScale_computes line 144
  55. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.matrixScale_encode line 145
  56. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.outerRow line 149
  57. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.outerRow_computes line 150
  58. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.outer line 151
  59. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.outer_computes line 152
  60. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.outer_encode line 153
  61. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.dotRow line 160
  62. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.dotRow_computes line 161
  63. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.mulVec line 162
  64. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.mulVec_computes line 163
  65. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.mulVec_encode line 164
  66. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.quadInput line 171
  67. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.quadInput_computes line 172
  68. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.quad line 173
  69. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.quad_computes line 174
  70. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.quad_encode line 175